Reid Barton

build Setup.hs with local compiler when cross-compiling

41

I have a script that invokes cabal with `--with-ghc=...`, `--with-ghc-pkg=...`, `--with-gcc=...`, etc. for cross-compiling to Android. It works great for most packages, but fails for a package with Build-type: Custom,...

simp sometimes gives an obscure error for nonexistent lemma

1

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

segfault on inductive type with binder starting with `_`

2

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

don't use "standalone" .olean files by default

6

It's fairly common to end up with accidentally end up with .olean files whose corresponding .lean file is gone (because it has been renamed, for example) and it can cause...

prove_goal_async fails when there are instances in the context

2

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

If the Lean 3 input has the form ```lean def add_foo := ... @[to_additive] def mul_foo := ... ``` then the mathport output now contains one `#align add_foo addFoo` resulting...

When I run `make port-mathbin` locally, there are 5 panics. It's not clear to me what files are being processed at the time. The failure is not propagated to the...

Expand the surreals library

3

We currently have a definition of the [surreal numbers](https://en.wikipedia.org/wiki/Surreal_number) in [surreal.lean](https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/surreal.lean), but there is still more to be done here. The next steps would be to show that the arithmetic...

More on quotients of categories

2

In `category_theory.quotient` we currently have a construction of the quotient of a category by an arbitrary relation on the Hom-sets, and half of its universal property (we could also prove...