Gabriel Ebner
Gabriel Ebner
https://leanprover-community.github.io/mathlib_docs/tactic/delta_instance.html#tactic.delta_instance_handler
Put the following in a lakefile: ```lean require std4 from git "https://github.com/leanprover-community/std4" @ "main" ``` Note that I made a mistake: this repo does not exist since `std4` is in...
Addresses #130. Reduces the runtime of the benchmark in #130 from 8.4s to 1.7s on my laptop.
Mathlib contains around 3k files. I have made a [small stress test](https://github.com/gebner/inundation) to see how long it takes to open a file in the editor with that project size (I...
This caused the IDE server to crash on some files in pulse.
The `lookup` request is the only one which does not return any response if the request failed. This makes it hard to support it in a generic API for IDE...
Consider the following four files: ```fstar // A.fsti module A val t: Type0 val s0: Type0 // We wrap the type in a match to trigger automatic coercion. inline_for_extraction let...
Before Lean 3.27, it was impossible to spawn more than a few thousand tasks via `task.delay`, because storing the log messages was quadratic in the number of tasks. ---