Containerizing Lean 4 files using Docker

Stream: general

[Arnav Sabharwal]

I'm experimenting with containerizing Lean 4, and am using the Dockerfile provided in .docker/gitpod/Dockerfile. I'm just trying to get something to print when I run docker run. However, I receive no response, and since I haven't done this before I don't know what the reason could be. Here is the one (and only) Lean file in the project I'm using for basic experimentation, so some assistance would really help!

def main : IO Unit := {
IO.println "Hello!"
}

[Eric Wieser]

That's unfortunately not valid lean code!

[Eric Wieser]

You are going to have a very bad time writing lean code if your only mechanism to test it is with docker run; Lean is designed to be edited inside an editor like VSCode / emacs / vim, with suitable extensions installed.

[Eric Wieser]

It wouldn't surprised me if VSCode outside the container knows how to start and connect to a server inside it

[Jason Rute]

Eric Wieser said:

It wouldn't surprised me if VSCode outside the container knows how to start and connect to a server inside it

If I recall, you install vs code outside the server if you haven’t. Then there is a Docker plugin which lets you remotely start a session inside the container. In that vs code session you install the lean plugin and it should go smoothly. (It’s been a while since I did this sort of thing with Docker, but I’ve done it a lot with remote servers.)

[Jason Rute]

Also see here for a valid hello world program: https://lean-lang.org/functional_programming_in_lean/hello-world/running-a-program.html