Gabriel Ebner

I've added the mathlib commit info to both the log as well as the predata tarball. I'm not sure if the timing is helpful. But at least we can now...

Hooked up a profiler to `order.filer.basic`: ``` # Children Self Command Shared Object Symbol 99.93% 2.40% mathport mathport [.] lean::csimp_fn::is_recursive_fn::visit ``` I guess we accidentally (?) made some function computable...

Hmm, now it hangs at ζ-reduction in `number_theory.bertrand` (`bertrand.real_main_inequality` to be specific). ``` 100.00% 0.00% mathport mathport [.] l_Lean_Meta_transform_visit___at_Lean_Meta_zetaReduce___spec__2___lambda__1 ```

No, without. Maybe 1512 fixes this issue.

This happens because only the second `tt` has a resolved constant in the AST. Not sure why there is a difference between theorem statement and proof here.

That's a good suggestion, but I'm not sure it's the best idea. 1. In my experience, putting mathport configuration in mathlib4 is a bit of a maintenance headache. For example...

Looking at the mathlib PR, I can see two situations where the TypeMax workaround leaks: 1. `Type max u v` is a category, and that's the expected type of types,...

If you forget a `pure` on an assertion, Pulse says that it cannot prove the assertion (instead of complaining about the type error). ````fstar ```pulse fn foo (n: nat) requires...

I did not expect a complete grammar---the lean.nvim readme was pretty clear that this is experimental. Errors are fine as well; the grammar in the vscode extension also has lots...

This is indeed super ambiguous, the following is a valid three-line long open statement: ```lean namespace something end something -- we need to define the namespace first open Lean something...