A "configuration-free" Lean environment builder

Stream: general

[Kevin Sullivan]

9:05 PM

To easy my own group's use of Lean (including onboarding of new students), I've put together a Lean in a Box environment so that no one will need to configure their own computers (beyond installing Docker and VSCode) to have a fully working Lean Development Environment. Simply create a fork of my repo, open that clone of yours in VSCode (in the right way), and all the rest builds itself. You'll be booted into Ubuntu 20.04 LTS running in a container with Lean and mathlib (among other things), delivered to you through a VSCode Window open and ready for development. I'd love to have a few people give it a go and send reports from the field. Detailed instructions are in the README: https://github.com/kevinsullivan/TMDE. (TMDE stands unostentatiously for The (coolest) Mathematical Development Environment (ever). Humor for my students.) Also, I I would not be surprised if others have done this before. I just wouldn't know about that, and so offer this as (another) opportunity to Get Lean Easy (TM) :-)

[We are beta testing one issue here, so please be advised: If nothing really happens when you clone your repo into a container, please load the Remote-Containers extension for VSCode on your local machine, reload the VSCode Window, try again, and let us know. What should happen is that a Docker build process kicks off. You can open a window to monitor it at the lower right of the screen There's also a status bar that remains active while the build does. We might need to add "Install the Remote-Containers extension in VSCode" to our instructions.]

[Yakov Pechersky]

Installing Docker Desktop might not be so simple, iirc it requires admin privileges, and has also sorts of questions during installation about WSL and other things that might be confusing. Additionally, unless configured to start at boot, the docker desktop daemon needs to be started before VSCode is launched.

[Yakov Pechersky]

These are great instructions otherwise!

[Kevin Sullivan]

Yakov Pechersky said:

Installing Docker Desktop might not be so simple, iirc it requires admin privileges, and has also sorts of questions during installation about WSL and other things that might be confusing. Additionally, unless configured to start at boot, the docker desktop daemon needs to be started before VSCode is launched.

Thank you, Yakov. It is a distinct advantage of our design that one need not deal with WSL. The details are in the README. In our experience, Docker Desktop runs adequately on Windows 10 Professional, Enterprise, and Education machines, but not on Windows 10 Home (which is what most home PC users will have). But inexpensive upgrade keys are available. They're free to my students through UVa.

And yes, the docker daemon does need to be running (typically through Docker Desktop) for some functions to work. So "zero-configuration" is really a slight marketing exaggeration. But give it a try, I think you'll be surprise how quickly you have your own GitHub-backed Lean project up and running with a first class configuration in all respects. Not free, but not bad!

[Kevin Sullivan]

Yakov Pechersky said:

Installing Docker Desktop might not be so simple, iirc it requires admin privileges, and has also sorts of questions during installation about WSL and other things that might be confusing. Additionally, unless configured to start at boot, the docker desktop daemon needs to be started before VSCode is launched.

Thank you, again, Yakov. We've added the clarifying instruction to ensure that Docker Desktop is running when VSCode is launched. We also fixed a small issue where VSCode would report a Lean Path not defined error. We fixed it by adding the automatic running of "leanpkg configure" to the set-up script. It all seems to be working now without a hitch.

[Eric Wieser]

I'm also surprised that installing docker is easier than installing elan. I suppose the extra difficulty comes from git and mathlibtools?

[Patrick Massot]

I guess Kevin's students are already meant to install Docker for other courses (otherwise I don't see how this solution could make any sense at all).

[Scott Morrison]

I can see some value even if you're having to install Docker just for this. Installing Docker doesn't involve touching the command line, which realistically is a hurdle for many.

[Gabriel Ebner]

I just wanted to try this out.

1. Apparently you need to install the separate "Remote - Containers" extension for vscode first (this is not in the readme).
2. The container build hangs at the following prompt (there is no way to press enter):

STEP 1: FROM alpine:3.13.2
? Please select an image:
  ▸ docker.io/library/alpine:3.13.2
    quay.io/alpine:3.13.2

[Gabriel Ebner]

After changing the registry configuration it still doesn't work. Apparently podman is not supported for the clone command.
However cloning the repository manually and then opening as a container seems to work fine.

[Kevin Sullivan]

Gabriel Ebner said:

After changing the registry configuration it still doesn't work. Apparently podman is not supported for the clone command.
However cloning the repository manually and then opening as a container seems to work fine.

I will respond to these feedbacks later this evening.

[Kevin Sullivan]

Eric Wieser said:

I'm also surprised that installing docker is easier than installing elan. I suppose the extra difficulty comes from git and mathlibtools?

Unix, terminal, shell, path, git, git bash, python3, ... For students who've never used a command line interface, and who come to us with all manner of laptop configurations, it's a lot of incidental complexity. For example, one sometimes has to remove/reconfigure a Python install that isn't the one recommended in the setup for Windows instructions. I myself would much rather no pollute my personal laptop with a bunch of software needed for this class.

[Kevin Sullivan]

Patrick Massot said:

I guess Kevin's students are already meant to install Docker for other courses (otherwise I don't see how this solution could make any sense at all).

To install Docker Desktop on Windows or OSX, you download and run the typical installer. https://www.docker.com/products/docker-desktop. Students don't interact with Docker again after that. It's dead simple. Give it a try.

[Kevin Sullivan]

Scott Morrison said:

I can see some value even if you're having to install Docker just for this. Installing Docker doesn't involve touching the command line, which realistically is a hurdle for many.

Exactly. I've had many students do the typical set-up. Most have never seen a Unix-like terminal/shell. They learn to use it, but it's a workout for them, and frustrating for enough of them (even if only 1/10) that it's an issue; and, in any case, it's not the workout I want or need them to have.

[Kevin Sullivan]

Gabriel Ebner said:

I just wanted to try this out.

1. Apparently you need to install the separate "Remote - Containers" extension for vscode first (this is not in the readme).
2. The container build hangs at the following prompt (there is no way to press enter):

STEP 1: FROM alpine:3.13.2
? Please select an image:
  ▸ docker.io/library/alpine:3.13.2
    quay.io/alpine:3.13.2

Gabriel, I'm speculating. My group hasn't seen the Docker error you report. I'm speculating, perhaps your Docker Desktop installation needs updating. If you're willing, update to the current Version, and give it another go?

[Kevin Sullivan]

Gabriel Ebner said:

1. Apparently you need to install the separate "Remote - Containers" extension for vscode first (this is not in the readme).

Yes, that's true, and was missing from our docs. It's there now. That was an oversight. All our testers already had it installed.

[Gabriel Ebner]

Perhaps your Docker Desktop installation needs updating.

That's right, I don't have a docker installation (and I'm not sure if "Docker Desktop" is even a thing on Linux). These days, it's all the rage to replace docker by podman (which provides a (mostly compatible) docker executable, but doesn't require a daemon or root access). Some distributions, like Fedora, even come with podman by default.

Most of the time, it's a drop-in replacement for docker. Unfortunately the vscode container extension is closed source, so this incompatibility is hard to fix.

[Patrick Massot]

Kevin Sullivan said:

Patrick Massot said:

I guess Kevin's students are already meant to install Docker for other courses (otherwise I don't see how this solution could make any sense at all).

To install Docker Desktop on Windows or OSX, you download and run the typical installer. https://www.docker.com/products/docker-desktop. Students don't interact with Docker again after that. It's dead simple.

Obviously you do whatever you want with your students, but all this thread clearly demonstrates your setup is dead not-simple. Also you commented on Docker vs a full regular install of our tools (including python tools), but that's not the alternative. The alternative is the zip bundles. On Windows (and Linux) they seem to work flawlessly. They are painful only on Mac because users need gmp first.

[Kevin Sullivan]

Gabriel Ebner said:

Perhaps your Docker Desktop installation needs updating.

That's right, I don't have a docker installation (and I'm not sure if "Docker Desktop" is even a thing on Linux). These days, it's all the rage to replace docker by podman (which provides a (mostly compatible) docker executable, but doesn't require a daemon or root access). Some distributions, like Fedora, even come with podman by default.

Most of the time, it's a drop-in replacement for docker. Unfortunately the vscode container extension is closed source, so this incompatibility is hard to fix.

Yeah, Docker Desktop isn't a thing on Linux. This solution works on Windows and OSX, because Docker Desktop does. That at least is documented in the instructions.

[Kevin Sullivan]

Patrick Massot said:

Kevin Sullivan said:

Patrick Massot said:

I guess Kevin's students are already meant to install Docker for other courses (otherwise I don't see how this solution could make any sense at all).

To install Docker Desktop on Windows or OSX, you download and run the typical installer. https://www.docker.com/products/docker-desktop. Students don't interact with Docker again after that. It's dead simple.

Obviously you do whatever you want with your students, but all this thread clearly demonstrates your setup is dead not-simple. Also you commented on Docker vs a full regular install of our tools (including python tools), but that's not the alternative. The alternative is the zip bundles. On Windows (and Linux) they seem to work flawlessly. They are painful only on Mac because users need gmp first.

As I read this thread, what I conclude is that (1) we needed to make some small fixes to the instructions, probably to include a more prominent warning that this won't work directly on Linux; (2) the dependency on a closed source VSCode extention is problematical for some. I've fixed (1). Can't fix (2), but for most it's not a show-stopper.

As for your Zip bundles. I don't know about them but would like to, as I said. They don't seem to be documented on the main project documentation pages, under Installation.

Also, the larger use case for the approach I describe is in my grad student group, where this packaging method lets us deliver a development platform with Lean, the ROS robotics package (which can be a bear to install), a custom-configured version of LLVM/Clang (that takes hours to compile), etc. To be able to have that environment up and running in five minutes has been a real boon to our group.

[Gabriel Ebner]

we needed to make some small fixes to the instructions, probably to include a more prominent warning that this won't work directly on Linux;

It should work just fine if you have the docker docker installed (and not the podman docker). It also works fine if you use "Open Folder in Container" instead of "Clone Repository in Container Volume". I'm probably not the only who uses podman and runs into these issues though.

[Patrick Massot]

Kevin Sullivan said:

As for your Zip bundles. I don't know about them but would like to, as I said. They don't seem to be documented on the main project documentation pages, under Installation.

They are. It's the last section of that page.

[Kevin Sullivan]

Gabriel Ebner said:

we needed to make some small fixes to the instructions, probably to include a more prominent warning that this won't work directly on Linux;

It should work just fine if you have the docker docker installed (and not the podman docker). It also works fine if you use "Open Folder in Container" instead of "Clone Repository in Container Volume". I'm probably not the only who uses podman and runs into these issues though.

Thank you, Gabriel.

[Kevin Sullivan]

Patrick Massot said:

Kevin Sullivan said:

As for your Zip bundles. I don't know about them but would like to, as I said. They don't seem to be documented on the main project documentation pages, under Installation.

They are. It's the last section of that page.

Here? https://leanprover-community.github.io/index.html.

[Bryan Gin-ge Chen]

There isn't a direct link from the front page, but the section Patrick is referring to is here.

[Kevin Sullivan]

Bryan Gin-ge Chen said:

There isn't a direct link from the front page, but the section Patrick is referring to is here.

Thank you. I wasn't aware of that. Looks like a great way to dip ones toes in Lean water.

I did, however, notice at the very bottom of the page that it says, "The downside is you won't be able to create your own projects or easily upgrade Lean and mathlib. You'll need a regular install for this."

Our containers build on the standard Ubuntu 20.04 LTS OS container with a full install of Lean. One ends up with a one-test-file project booted up through leanpkg build. One can use leanpkg, leanproject, and all the other Lean infrastructure through a terminal to the container OS to manage, reconfigure, or update Lean, mathlib, etc. And (once you configure your git username and email in the container) you can push to and pull from your own GitHub repo as well as from the upstream one (this one!) to take advantage of improvements we might make.

My aim was/is to provide a comprehensive, professional quality, but early-student-ready (as close to dead simple as possible) development environment and infrastructure. It's maybe a little comparing apples and oranges in relation to the ZIP installers. Different problems different tools!

Here's another use case: Our research software development environment "inherits" from this one but extends it with the Robot Operating System (ROS), a custom build of LLVM/Clang, VSCode extensions for that environment (e.g., lots for C++) and a bunch more stuff. It's no more complicated to get that environment up and running than the simple "Lean" one here, on the other hand.

[Kevin Sullivan]

Gabriel Ebner said:

we needed to make some small fixes to the instructions, probably to include a more prominent warning that this won't work directly on Linux;

It should work just fine if you have the docker docker installed (and not the podman docker). It also works fine if you use "Open Folder in Container" instead of "Clone Repository in Container Volume". I'm probably not the only who uses podman and runs into these issues though.

I looked at Podman. Thanks for that. I'd use it if I were building a containerized stack to run on Linux. It runs there and Docker Desktop doesn't. The problem for us is that it doesn't run on Windows or OSX.

[Kevin Sullivan]

"Circling back", I now have some data. A few weeks ago, I required my class of ~85 first and second year discrete math students in CS to obtain their Lean development environments for the semester using the approach we've discussed here. I compared my observations of the student experience "getting Lean" this year with experiences of prior years, when I had them follow the (evolving) standard installation instructions for MacOS and Windows.

About 85% needed no help and had the system running quickly and without apparent complications. The remainder had various mostly minor issues. I have systematiclly documented each instance as a GitHub Issue in our class repo (just in case you're interested, haha). Most issues were fixable in just a few minutes each. Since then, for at least the last few weeks, everything has been working without incidents, with the students working in the environment at least three times a week in class.

Bottom line from my perspective? I've required students in large classes to use Lean and mathlib something like half a dozen times. For beginners in computing, with diverse laptop-based hardware and OS configurations, and variations in ability to follow instructions, and the need for prior knowledge of things like command line interfaces, the standard instructions are too often too much. All I can tell you is that in my estimation, this approach reduced the overhead of getting students up and running by at least 80% versus the baseline. It was much easier for them, and consequently on me.

A few of the issues that we fixed early on were raised by people here, so I'd like to thank each person who took the time to have a look and comment here.

(And if you haven't tried it and are interested, if you're like my students, you've got at least an 80% chance to see the fun part without any annoying glitches in the installation process. Would love to hear about your experiences, if any, positive or not, with responses here or issues in our GitHub repo.

Kevin