Using lean through the CLI/Docker?

Stream: new members

[Alex Altair]

Hey all, potential new user poking my head in here to ask a question; how doable would it be to use Lean by manually interacting with the CLI instead of things like the VS Code plugin? Whenever I can, I like to install software on my computer through Docker containers, and it's more of a pain to use a GUI from inside a docker container (plus I use sublime, never used VS Code)

[Ruben Van de Velde]

You could use lake build, but this will be very painful

[Matthew Ballard]

How do you feel about nvim or emacs?

[Eric Wieser]

Vscode has an interface for connecting to a remote system (such as your docker container)

[Alex Altair]

@Ruben Van de Velde Not sure what you mean by that; I was thinking I would install lean the "normal" way, just inside a container

[Eric Wieser]

Ruben's point is that using Lean via the command line alone will be a completely miserable experience

[Alex Altair]

Matthew Ballard said:

How do you feel about nvim or emacs?

If I do end up learning a new editor, then I'd go with VS Code

[Alex Altair]

Eric Wieser said:

Vscode has an interface for connecting to a remote system (such as your docker container)

That's good to know, might be a worthwhile intermediate

[Eric Wieser]

I think that's going to be your final (not just intermediate) destination unless you plan to write a sublime text extension

[Alex Altair]

Gotcha

[Eric Wieser]

I think there was a thread by another user asking for a sublime extension, so there is _some_ interest; but I imagine you can find more interesting things to do with Lean when you get started, and the nvim/emacs crowd probably outnumbers sublime users.

[Scott Morrison]

VSCode works great, and no one but diehard emacs/nvim people who were using these before I was born should consider anything else. :-)

VSCode happily interacts with a Lean server over an ssh connection, and this would work fine if you want to keep the server inside a container.