using lean without IDE

Stream: new members

[Hugo van der Sanden]

Hi, is it in principle possible to use lean without using one of the supported editors? My preference would be to create a proof in a text file, then run some commandline process to check if the proof is valid - I have a strong dislike of IDEs.

[Eric Wieser]

You can use lake build Path.To.Your.File to build Path/To/Your/File.lean (after doing lake new to set up a project)

[Eric Wieser]

But there is a lot of information that is crucial to use Lean that is not present outside an IDE

[Mauricio Collares]

If your objection is to using VS Code, both Emacs and neovim are well-supported.

(Edit: To be clear, I just mentioned Emacs and neovim because I think few people classify those as IDEs and maybe Lean documentation doesn't emphasize they're options too. You can certainly build an IDE-like environment on Emacs, but you can also dial it down as much as you like. I don't like IDEs either.)

[Hugo van der Sanden]

Thanks both; I'll have to see how far I get then. (I have never had an experience with any IDE that wasn't a bad one.)

[Arthur Paulino]

You may dislike IDEs, but you may dislike the experience of programming in Lean without synchronous access to the language server even harder

I used to dislike IDEs, but Lean motivated me to adopt VS Code. And now I use VS Code to program in all languages that I use

IMO, the live infoview is a big plus of the whole Lean experience

[Mark Fischer]

Hugo van der Sanden said:

I have never had an experience with any IDE that wasn't a bad one.

1) You can type-check and/or compile Lean code from the command line. Though afaik, you won't see output for commands like #check or #eval without a process interacting with the language protocol. If you just want to check if a proof is valid though, you can do so with a simple text editor and a terminal.

2) I've been finding that even though theorem proving in lean is done with a programming language, it isn't all that much like programming. If you're using Lean to develop proofs, I'd argue live access to proof state and type inference is invaluable in a way it simply isn't when writing programs. I think it has to do with the idea that everything you care about in a proof is statically available while a lot of what you care about in a program is available when the code is running. Theorem-provers can blur that line, sure, but I think you'll be surprised.

3) If you want to read a program in lean, you just read the code. If you want to read a math proof, you often step through the lines while looking at how the proof state changes. A lot of the logic isn't explicit in the text you read, it's in the context being carried forward. If you see a line that says something like "Simplify the goal using these 3 theorems," you're probably considerably less interested in the instruction than what the resulting Goal looks like. In a sense this should change how you think about Lean while writing proofs.

Good luck! :)