A "wait for lean compilation" language model tool

[mik-jozef]

This tool enables an agent to wait for compilation to finish after a file is edited, and optionaly refresh file imports. This is because Lean's compilation can take seconds and vscode's diagnostics is non-blocking. Without this, an agent can receive a false negative "0 problems found message".

I thought I would ask for this as a feature request, but since I tried vibe-coding it and it works locally, I thought I would attach my code as well. If the impl does not meet quality standards let me know if you'd prefer me to create a feature request issue instead.

The alternative solution of letting an agent run lake build using terminal has two disadvantages, as far as I know:

• requires using terminal, which requires either manual approval each time, or auto-approve that "provides best effort protections and assumes the agent is not acting maliciously".
• may include unrelated errors, not just those that the agent asks for for specific files using vscode diagnostics

[mhuisi]

Are you aware of lean-beam?

[mhuisi]

Regarding "agent gets confused about diagnostics", in core we have a single line in our CLAUDE.md that seems to prevent these issues:
https://github.com/leanprover/lean4/blob/master/.claude/CLAUDE.md#lsp-and-ide-diagnostics

[mik-jozef]

in core we have a single line in our CLAUDE.md that seems to prevent these issues:

If you're referring to "Trust command-line test results over IDE diagnostics.", I was hoping for a solution that avoids the command line.

Thanks for mentioning lean-beam, I have not yet had a chance to give it a proper look, but if the Lean 4 extension is not a proper place for this kind of functionality (though I think it would be cool if good agent tooling came with installing the extension out of the box!) then I'm happy to close this.