Minimal Lean+Mathlib setup in Docker

Stream: new members

[Isak Colboubrani]

I am currently following these steps to set up new Lean+Mathlib projects:

docker run -it --rm ubuntu
apt update && apt upgrade -y && apt install -y curl git
curl -sS -o elan-init.sh https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
sh elan-init.sh -y
source $HOME/.elan/env
lake new project_name math
cd project_name
lake exe cache get
echo 'import Mathlib' > ProjectName/Basic.lean
echo 'example : 1 + 1 != 3 := by aesop' >> ProjectName/Basic.lean
lake build

I have a few questions:

1. Is this the recommended method for setting up Lean+Mathlib in Docker?
2. Any suggestions on improvements? Are there ways to enhance compile time?
3. Are there any plans towards including elan, lake, or lean as official Debian packages?

[Kevin Buzzard]

I don't know anything about docker, but I am pretty sure that the answer to 3 is that lake and lean are both very fast-moving right now and contributing them as official Debian packages will cause a lot of problems. The whole point of elan is that it will download the version of Lean which is right for the project you're running, and 9 times out of 10 this will not be the version that a package manager offers.

[Isak Colboubrani]

@Kevin Buzzard That's completely understandable for lake and lean (and what I assumed), but is elan sufficiently stable to be considered for inclusion?

[Isak Colboubrani]

This would eliminate the need for the "piping curl to shell" process, which is often unpopular among users (example: https://0x46.net/thoughts/2019/04/27/piping-curl-to-shell/).

[Michael Rothgang]

To me, packaging elan for Debian doesn't sound out of the question. (The rustup tool (for the Rust programming language) is packaged now - and elan is basically a fork of rustup.)
I guess the key question is whether the Lean FRO has sufficient resources and interest to make that happen. :-)

[Sebastian Ullrich]

https://packages.debian.org/sid/elan

[Isak Colboubrani]

@Sebastian Ullrich Thanks! I wasn't aware of that Debian package. I'm happy to move away from the "curl to shell" approach.

Here's my revised minimal Lean+Mathlib setup in Docker:

docker run -it --rm debian:unstable
apt update && apt upgrade -y && apt install -y elan curl git
elan toolchain install nightly
elan default nightly
lake new project_name math
cd project_name/
lake exe cache get
echo 'import Mathlib' > ProjectName/Basic.lean
echo 'example : 1 + 1 != 3 := by aesop' >> ProjectName/Basic.lean
lake build

Any suggestions on improvements?

@Christopher Hoskin Thanks for packaging elan for Debian! Would it be sensible to add curl and git as dependencies (or "recommended dependencies") for elan in Debian? I believe that lake new <project_name> math and lake exe cache get might fail with somewhat cryptic error messages without curl and git installed.

[Eric Wieser]

I think that's somewhat tricky, because it's not elan that depends on curl, or even lake; it's Mathlib

[Eric Wieser]

Maybe it's worth noting that there is already a docker setup for mathlib at https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile

[Eric Wieser]

This also comes with python and requests, which are needed by the polyrith tactic

[Sebastian Ullrich]

Current Lake does depend on curl

[Christopher Hoskin]

Sebastian Ullrich said:

Current Lake does depend on curl

The Debian elan package depends on libcurl3-gnutls. Is that sufficient, or are you saying that it needs the curl command line tool too?

I looked at packaging lean3 - technically looked easy enough, but I'm not sure that a lean package would be particularly useful, at least from a mathlib point of view. Instead I opted for symlinking /usr/bin/lean and friends to elan, which downloads toolchains to ~/.elan/toolchains/.