JovanGerb
JovanGerb
@semorrison Yes, I've run `!bench` on mathlib, and many files in `Batteries`, and `Mathlib.Tactic` have sped up. For example Batteries.Tactic.NoMatch | 2,467 mld. | -118,849 mln. | -4,818 % Batteries.Tactic.Case...
In type class synthesis, this code gets the result from the discrimination tree: ``` let result ← globalInstances.getUnify type tcDtConfig -- Using insertion sort because it is stable and the...
In my `RefinedDiscrTree`, I output a natural number score that indicates how good the match is, and I sort the result based on the scores of the entries. This a...
changelog-language
Yeah, I wasn't sure about backticks vs single quotes. I went for normal quotes because they seem to be used more than backticks. I don't know of any difference in...
Here both quotes are even used in the same error: https://github.com/leanprover/lean4/blob/0448e3f4ea1b2c476fc79aeee5d407971a1cd9e2/src/lake/Lake/Load/Package.lean#L31
Hmmm, the Mathlib CI isn't happening automatically?
That's okay, I was hoping for a more significant speedup as well. But I think 0.1% is above the noise threshold for instuctions for Mathlib as a whole (from what...
Yes, @PatrickMassot suggested to me after my presentation to change some settings. I think the changes include - turn off pop-up suggestions when typing. - turn off hovers in the...
In fact, I was trying to turn off the typing pop-up suggestions before the talk, but couldn't figure out on time how to do it.