Eric Wieser

feat(library/init/core): allow lists of proofs

4

With upstream changes to mathlib, this would allow `fintype some_prop`, which would in turn allow proofs to be used to index finite things like matrices or summations.

feat(*): Log progress messages to stderr even when using `json` output on stdout

2

I haven't actually tested this, but it seems plausible that it would work. Motivated by https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Showing.20progress.20of.20mathlib.20builds/near/214955317

fix(init/meta/converter/interactive): Do not allow rw to create ⊢ goals in conv mode

4

This is an attempt at the approach described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212702071 A contrived example where this applies: ```lean import algebra.ring variables {α : Type*} [ring α] {a b c : α}...

### 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). *...

Consider: ``` python a = Session() b = Session() add_images_to(a) add_images_to(b) a.commit() b.rollback() ``` `a.commit` will commit `b`s images as well, because `_stored_images` is global state! It should be session-specific...

Fixes gh-8938 Previously, for all but the pretty printer, method hooks in base classes took precedence over explicit `for_type` hooks registered for subclasses. This changes makes all the printers match...

feat(analysis/inner_product_space/spectrum): add a decomposition instance

1

This proof felt a bit painful - I suspect most of the results I needed already exist somewhere else. This `decomposition` instances inherits the noncomputability of `orthogonal_projection`, but it is...

Correct link to galgebra

13

The link here is dead. xref https://github.com/pygae/galgebra/issues/28 I have no idea whether it makes sense to accept corrections here, but I thought I may as well file the PR.