Gabriel Ebner

> So if I understood you correctly, you're not necessarily talking about extending the current delaborator (which, as a transformation from `Expr` to `Syntax` can't be readily generalized to other...

> `LEAN_CC` is intended to be "the C compiler used for compiling Lean-produced C files". How is `LEAN_CC` actually intended to be used? I've never been able to make it...

> > Honestly, I really think Lake should just bypass leanc altogether and invoke the compiler directly > > I'm still open to that as I said before The bundled...

> I was just talking about skipping `leanc` in Lake, which isn't in the nixpkgs setup, correct? Whether that works depends on what you call instead of `leanc`. If you...

From my point of view there are still several challenges ahead. The applications I have in mind are mostly mathport / code action related, so this list might a bit...

So resolve to the alias first, and only look it up as a declaration if that fails? That seems good to me.

I'm also seeing this issue in the neovim plugin, so maybe this is a bug in the Lean 4 LSP implementation itself. Does the `Lean 4: Restart Server` command help?

This looks like a bug in the watchdog. Transferring to the Lean 4 repo because this bug is not editor-specific.

I'm going out on a limb here, but this could be due to this line: https://github.com/leanprover/lean4/blob/5896e6f1d6fc69441b476f3457172713e708f835/src/Lean/Server/Watchdog.lean#L308 If writing the exit message to the file worker *blocks*, then the file worker...

> But just to be clear, should "Restart Server" not replace the entire watchdog process? Oh, I confused that with "Refresh File Dependencies". Maybe something different is going on as...