Gabriel Ebner

Note that for the docs we could just create a file containing `import all #help options` and parse the output. If somebody wants to implement this, it would also be...

I'm pretty sure this is a unification problem and not a transparency issue. During type class search we need to unify the instance with the goal, this is much harder...

bors try

If you can, building with release type Debug is certainly helpful. This will also enable extra assertions (and hopefully point to the actual source of the error). Maybe you could...

Yes!

No the change was supposed to make Lean crash *faster*. Can you try again with the Release build type?

> lean(89652,0x16d653000) malloc: Heap corruption detected, free list is damaged at 0x600055857120 Oooh, this is not good. This means that the error happens somewhere else, and we're just noticing at...

Thanks for asking! I wasn't sure if "leaving the buffer" means "leaving the parent buffer" or "leaving the buffer for the floating window".

~~This looks like your Lean installation is messed up a bit. When you start lean from nvim, it runs `lean --server`, which in turns runs one `lean --worker` process per...

> We could emulate this before by pausing the current pin, but this seems much more intentional, and also gives you an extmark and interactive info. I don't think we...