Zulip Chat Archive

Stream: Lean for teaching

Topic: A zero-config Lean/mathlib development environment


Kevin Sullivan (Aug 24 2021 at 01:05):

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 (Aug 24 2021 at 01:49):

@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 (Aug 24 2021 at 02:19):

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

Scott Morrison (Aug 24 2021 at 02:19):

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

Kevin Sullivan (Aug 24 2021 at 02:25):

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 (Aug 24 2021 at 02:27):

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 (Aug 24 2021 at 02:38):

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 (Aug 24 2021 at 02:39):

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 (Aug 24 2021 at 02:39):

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 (Aug 24 2021 at 02:39):

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

Kevin Sullivan (Aug 24 2021 at 02:46):

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 (Aug 24 2021 at 17:12):

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 (Aug 24 2021 at 23:03):

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 (Aug 25 2021 at 02:15):

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 (Aug 25 2021 at 03:12):

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

Kevin Sullivan (Aug 25 2021 at 18:52):

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 (Aug 25 2021 at 19:43):

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 (Aug 25 2021 at 21:45):

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 (Aug 26 2021 at 00:46):

This conversation might continue in the GENERAL section of Zulip.

Kevin Sullivan (Sep 09 2021 at 04:10):

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 (Sep 09 2021 at 08:46):

Is this mathematicians or computer scientists? What OS?

Huỳnh Trần Khanh (Sep 09 2021 at 09:53):

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 (Oct 14 2021 at 18:26):

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 (Oct 14 2021 at 18:28):

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.


Last updated: Dec 20 2023 at 11:08 UTC