Acme editor

Stream: Emacs

[Maksym Radziwill]

Lean4 is now supported in the Acme editor (of plan9 fame).

I forked the acme-lsp repo to provide LSP support for Lean4 in acme, https://github.com/maksym-radziwill/acme-lsp-lean . The LSP supports hover (L hov), go-to definition (L def), an info view (L assist goal), finding all references (L refs) and code completion (L comp). The info view with "L assist goal" works just as in vscode, that is clicking on code updates the info view. Performance is top notch.

I wrote another program to get unicode working in the same way as it does in the vscode lean4 extension i.e same key combinations and characters, https://github.com/maksym-radziwill/acme-unicode .

To test these out I wrote some 200 lines of lean4 using acme, specifically I added a proof of Borel-Caratheodory to the StrongPNT project. After this experience, I conclude that Acme is now a viable way of writing lean4 code.

It is also possible to provide integration with loogle, either a local or remote instance, but I didn't upload a relevant repo yet. There is no syntax highlighting, because syntax highlighting is impossible in acme by design.

This is Acme-specific, but I thought some here might find it useful to know about another editor option for Lean4.