ctb

Hi bwa users,

The bwa-mem manuscript has been rejected. Interestingly, the first
reviewer only raised a couple of minor concerns and then accepted the
manuscript in the second round of the review. The second reviewer made
quite a few mistakes on some basic concepts and was hostile from the
beginning. The third reviewer gave fair and good review in the first
round, all of which have been addressed, but he then tried hard to
argue one particular mapper to be the best in accuracy that on the
contrary is inferior to most others in my view. I admit that my

rxaviers

People

:bowtie:	😄 :smile:	😆 :laughing:
😊 :blush:	😃 :smiley:	☺️ :relaxed:
😏 :smirk:	😍 :heart_eyes:	😘 :kissing_heart:
😚 :kissing_closed_eyes:	😳 :flushed:	😌 :relieved:
😆 :satisfied:	😁 :grin:	😉 :wink:
😜 :stuck_out_tongue_winking_eye:	😝 :stuck_out_tongue_closed_eyes:	😀 :grinning:
😗 :kissing:	😙 :kissing_smiling_eyes:	😛 :stuck_out_tongue:

vasanthk

System Design Cheatsheet

Picking the right architecture = Picking the right battles + Managing trade-offs

Basic Steps

1. Clarify and agree on the scope of the system

• User cases (description of sequences of events that, taken together, lead to a system doing something useful)
  • Who is going to use it?
  • How are they going to use it?

sleepygarden

function canvasApp() {

    if (!canvasSupport()) {
        return;
    }

    var canvas = document.getElementById('canvasOne');

    var ctx = canvas.getContext('2d');
    setup();

shagunsodhani

Deep Math: Deep Sequence Models for Premise Selection

Introduction

• Automated Theorem Proving (ATP) - Attempting to prove mathematical theorems automatically.
• Bottlenecks in ATP:
  • Autoformalization - Semantic or formal parsing of informal proofs.
  • Automated Reasoning - Reasoning about already formalised proofs.
• Paper evaluates the effectiveness of neural sequence models for premise selection (related to automated reasoning) without using hand engineered features.
• Link to the paper

bit-hack

// non-recursive version of algorythm presented here:
// http://ruslanledesma.com/2016/06/17/why-does-heap-work.html

#include <algorithm>
#include <array>
#include <stddef.h>
#include <stdio.h>
#include <vector>

template <typename type_t>

yizhang82

    class rw_spin_lock
    {
    public:
        rw_spin_lock()
        {
            _readers = 0;
        }

    public:
        void acquire_reader()

kbuzzard

-- this was compiling with mathlib in June 2020
import tactic

theorem imo2019Q1 (f : ℤ → ℤ) :
(∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔
(∀ x, f x = 0) ∨ ∃ c, ∀ x, f x = 2 * x + c :=
begin
  split, swap,
  { -- easy way: f(x)=0 and f(x)=2x+c work.
    intro h,

jessejanderson

New site:

Schools affected by COVID-19

Please visit the link above for up-to-date content.

The rest of the page is left here for legacy reasons but will no longer be updated.

alreadydone

import tactic data.setoid.basic
universes u v

def em (p) := p ∨ ¬p
def lem := ∀p, em p

def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β