Comment by fooker
19 hours ago
This has also been my experience with lean4.
I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool
19 hours ago
This has also been my experience with lean4.
I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool
To be fair, Coq has ProofGeneral and Agda has its emacs mode. Once you go outside these established channels, oftentimes using the tool becomes incredibly difficult. I guess for interactive theorem proving in general you may need some sort of editor at some point.
Yeah, I'm not a fan of the encouragement to use vscode; that said it was pretty easy for me to get neovim set up with Lean tooling, and that's what I use generally.