Gabriel Ebner

Closed as completed. AFAICT we've already ported the relevant files from core.

> I am curious what benefit, if any, the update has on performance. Could you run your benchmark against the new update? The benchmark is literally running `lake print-paths` on...

So apparently the `lookup` query is used internally by `full-buffer`.

> So apparently the `lookup` query is used internally by `full-buffer`. I've added a new internal query type to ignore errors. The `full-buffer` command now uses this to suppress error...

The vscode extension now avoids the awkward version of the lookup query, and no longer uses the internal lookup queries either. The right choice is probably to just remove the...

What is `factorize`? An inverse to `expand`?

Personally, I think that a mathematica/sage interface is only useful for hard computations that have intelligible certificates. E.g. computing antiderivatives is probably a good example. For `cancel` the best certificate...

This PR is blocked by what I can only assume to be a miscompilation. Running stage1 immediately segfaults in the `Syntax.identComponents` function where we call `lean_inc` on a freed object...

Rebasing onto #2060 seemed to fix the compilation errors. !bench

> Before this patch `unique_lock` refers to `lean::unique_lock` under certain conditions ( -DLEAN_MULTI_THREAD=OFF). That's the intended behavior. The `LEAN_MULTI_THREAD` flag should disable all multi-threading. That flag will also enable optimizations...