Development setup

Stream: lean4 dev

[Tom]

I've been looking at setting up a development version of Lean against my fork of the compiler but while I'm used to building large C++/mixed language programs, I can't quite understand what the second part of this page is telling me: https://leanprover.github.io/lean4/doc/dev/index.html

Specifically, starting about halfway down, " then use elan override set to associate such ...". Are the command lines below a "fire and forget" kind of thing I shouldn't worry about right now? I think I get the gist of what it's saying (I think it's pointing "lean4" to be a link to the stage1 version of Lean, i.e. the version written in itself - correct?) but I'm barely getting to grips with the language and the rest of the ecosystem is still very much opaque to me - so want to make sure I can undo any damage I may cause.

Any clarifications/real-world recommendations on setting up a good dev env would be appreciated!

[Henrik Böving]

The way you are setting up elan here will make the Lean plugins for common editors use the compiler source and binaries that you have just built as an LSP server so you can get go to definition in your own compiler sources and observe functionality you've just implemented right away.

Note that if you have a file open and recompile the compiler you have to restart the lean server for that file, in emacs this is done by C-c C-d for a single file and M-x lsp-workspace-restart for all your open files in that LSP workspace.

[Mac]

Tom said:

so want to make sure I can undo any damage I may cause.

These commands are elan commands and elan is something that can be easily wiped and replaced, so there should be no worries about irreparable damage to your system with them.

[Tom]

Thanks! I appreciate the help.