A zero-config Lean/mathlib development environment

Stream: Lean for teaching

[Kevin Sullivan]

To get students started with Lean with really minimal system configuration, I've put together a Lean in a Box environment. Open a fork of my repo, and the rest builds itself. You'll be booted into Ubuntu 20.04 LTS running in a container with the full Lean stack installed, all delivered by VSCode ready for development. I would love to have a few people give it a go and send reports from the field. All the details are in the GitHub README, at https://github.com/kevinsullivan/TMDE. (TMDE stands unostentatiously for The (coolest) Mathematical Development Environment (ever). Humor for my students.) [If nothing happens when you connect to your repo following the instructions, please load the Remote-Containers extension to VSCode on your local machine and reload the VSCode Window to try again. Let me know in this case, please, if you could.]

[Mac]

@Kevin Sullivan Cool! It is also neat to see project in security and teaching utilizing Lean being funded (at least in part) by the NSF! As a Computer Security Ph.D. student coding in Lean as hobby. that gives me courage that I may one day be able to transition some of that work into my profession.

[Scott Morrison]

@Kevin Sullivan, this failed for me with the following error:
Screen-Shot-2021-08-24-at-12.18.14-pm.png

[Scott Morrison]

Not sure what is going on. Of course from outside the container that URL is fine.

[Kevin Sullivan]

Scott Morrison said:

Kevin Sullivan, this failed for me with the following error:
Screen-Shot-2021-08-24-at-12.18.14-pm.png

Ok, thanks for this. We haven't seen that. Looks like a problem setting up container-host networking, but I'd only be guessing. We'll keep our eye out. I'll also poke around to see if I can find other reports. Will get back.

[Kevin Sullivan]

Getting back. Maybe something here will help? https://stackoverflow.com/questions/20370294/git-could-not-resolve-host-github-com-error-while-cloning-remote-repository-in. I've so little access to your context. Happy to look some more if needed.

[Scott Morrison]

It seems I had an old version of docker on this machine. After allowing docker to update itself, it seems to have worked.

I did need to hit enter at a prompt at some point during the build, however!

[Scott Morrison]

It also didn't give an indication that it was done building... eventually there was no more output for a while (about the 7 minute mark)

[Scott Morrison]

While things seem to work, the first time I opened a lean file I got a pop-up error about leanpkg.path does not exist.

[Scott Morrison]

I'm going to stop playing with this now, but good luck. :-) I like the idea.

[Kevin Sullivan]

It's working well for my group internally. The more we hear the faster we can figure out what to fix. So thanks!

Update: I've updated the instructions to remind folks to update any older Docker install already in place.

[Kevin Sullivan]

Scott Morrison said:

It seems I had an old version of docker on this machine. After allowing docker to update itself, it seems to have worked.

I did need to hit enter at a prompt at some point during the build, however!

Scott,

Thanks again. The leanpkg.path issue has been fixed by automatically running "leanpkg configure" as part of the set-up script. It all seems to be working without warnings now.

[Scott Morrison]

No --- the prompt (unfortunately I got enter before thinking I should note it down) was more of a "hit enter to dispose of this terminal" type prompt.

[Kevin Sullivan]

Scott Morrison said:

No --- the prompt (unfortunately I got enter before thinking I should note it down) was more of a "hit enter to dispose of this terminal" type prompt.

Ah, that was likely the signal that a key part of build processes finished. I'll program in a welcome message if I can so that it's clear that the build is done and the environment is ready to use.

[Scott Morrison]

Lots more happened afterwards! Sorry I can't give you the exact message.

[Kevin Sullivan]

Thanks. Just ran again on a clean box and did get asked about the name of a container volume in which to store the cloned repo. Will add that to documentation.

[Patrick Massot]

Could you explain again what you gain compared to the bundles we have where you unzip one file and click on an icon to launch VScode+Lean, as in https://oleanstorage.azureedge.net/releases/bundles/trylean_windows.zip?

[Kevin Sullivan]

Patrick Massot said:

Could you explain again what you gain compared to the bundles we have where you unzip one file and click on an icon to launch VScode+Lean, as in https://oleanstorage.azureedge.net/releases/bundles/trylean_windows.zip?

Patrick, Thanks for the pointer. I've just been going from the installation instructions for Windows and OSX from the community web site, here: https://leanprover-community.github.io/. I haven't tried the one-click installers. Some possible advantages, per your question, include:

(1) No potential conflicts with local configurations (we've had to ask Windows users to remove old Python installations that don't work with the installation instructions for Windows, for example).
(2) The same, fully configured Ubuntu 20.04 LTS operating system environment for everyone, so that we don't have to document variants across OSX and Windows.
(3) A project that is already backed by a GitHub repository.
(4) Ease of evolution of the development environment. E.g., we can push an update to the OS layer, then all one needs to do is "Rebuild Container" in VSCode to get the updated environment.

Thanks, again, for pointing me to the one-click installer. Where are those documented? I don't see that information on the Lean Community documentation page.

Kind regards,
Kevin

[Kevin Sullivan]

This conversation might continue in the GENERAL section of Zulip.

[Kevin Sullivan]

Kind regards. A short experience report: I teach a class of about 85 first- and second-year undergraduates this semester. Within a day of being pointed to our instructions,, about 85% had this environment configuration running and tested successfully, without having needed any help. The remaining ~15% had various issues. Most were easily resolved. Relevant fixes have been applied where applicable. One problem required some exploration to come up with a plausible solution: there seems to be an ongoing conflict between Docker Desktop and VirtualBox on Windows. This poses problems to students who are required to use both. Only one student was at issue here, but the severity of this issue elsewhere would depend on local conditions: the extent to which co-location of these tools on your OS is a requirement. Take this for what it's worth: I'd rate it as a very smooth adoption processes for most of the students, and the residual issues were mostly resolved in just a few minutes each. My students don't have any problem with it, and seem to like it.

[Kevin Buzzard]

Is this mathematicians or computer scientists? What OS?

[Huỳnh Trần Khanh]

Wow, this thing is incredibly cool! It's very similar to the setup that I have on my local machine, but VS Code is also inside the container too! Well, code-server to be exact. My setup is also very easy to use: just run docker-compose up and everything is up and running!

[Kevin Sullivan]

Hi Kevin B, sorry for delay getting back to you. The environment is for either computer scientists or mathematicians. I'd encourage you to give it a try and let me know what you think. It has been a real problem-saver for my class of 85 second year undergraduates.

[Kevin Sullivan]

Huỳnh Trần Khanh said:

Wow, this thing is incredibly cool! It's very similar to the setup that I have on my local machine, but VS Code is also inside the container too! Well, code-server to be exact. My setup is also very easy to use: just run docker-compose up and everything is up and running!

Thank you! Yes, if you're running on Windows or OSX it really works like a charm.