[danilafe]

I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.

[fooker]

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

[danilafe]

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.

[JuniperMesos]

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.