feat(.docker): Docker containers for debian, alpine, and gitpod (#6515)

# Docker containers

The `.docker` directory contains instructions for building Docker containers
with Lean and mathlib.

## Build

You can build these containers using `scripts/docker_build.sh`.
This will result in the creation of two containers:

* `leanprovercommunity/lean` - contains elan, lean, and leanproject
* `leanprovercommunity/mathlib` - additionally contains a copy of mathlib, with oleans

In fact, for each container you'll get three different tags, `:debian`, `:alpine` and `:latest`.
`:debian` and `:alpine` use those respective distributions, and `:latest` just points at `:debian`.
Finally, there is also a `leanprovercommunity/mathlib:gitpod` for use at
[https://gitpod.io/](https://gitpod.io/).

## Usage

### gitpod.io

There is a container based on `gitpod/workspace-base`
enabling [https://gitpod.io/](https://gitpod.io/) to create in-browser VSCode sessions
with elan/lean/leanproject/mathlib already set up.

Either prepend `https://gitpod.io/#` to basically any URL at github, e.g.
[https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker](https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker),
or install a [gitpod browser extension](https://www.gitpod.io/docs/browser-extension/)
which will add buttons directly on github.

### Command line

You can use these containers as virtual machines:

```sh
docker run -it leanprovercommunity/mathlib
```

### Docker registry

These containers are deployed to the Docker registry, so anyone can just
`docker run -it leanprovercommunity/mathlib` to get a local lean+mathlib environment.

There is a local script in `scripts/docker_push.sh` for deployment,
but I have also set up `hub.docker.com` to watch the `docker` branch for updates
and automatically rebuild.

If this PR is merged to master we should change that to watch `master`.

### Remote containers for VSCode

Installing the `Remote - Containers` VSCode extension
will allow you to open a project inside the `leanprovercommunity/mathlib` container
(meaning you don't even need a local copy of lean installed).

The file `/.devcontainer/devcontainer.json` sets this up:
if you have the extension installed, you'll be prompted to ask if you'd like to run inside the
container, no configuration necessary.


Co-authored-by: Alex J. Best <[email protected]>



Co-authored-by: Scott Morrison <[email protected]>

.devcontainer/README.md

@@ -0,0 +1,11 @@
+# Remote containers for VSCode
+
+Installing the `Remote - Containers` VSCode extension
+will allow you to open a project inside the `leanprovercommunity/mathlib` container
+(meaning you don't even need a local copy of lean installed).
+
+The file `/.devcontainer/devcontainer.json` sets this up:
+if you have the extension installed, you'll be prompted to ask if you'd like to run inside the
+container, no configuration necessary.
+
+See `/.docker/README.md` for a description of the `leanprovercommunity/mathlib` container.

.devcontainer/devcontainer.json

@@ -0,0 +1,21 @@
+{
+	"name": "mathlib",
+	// "image": "leanprovercommunity/mathlib", // it's faster to build the container than download it
+	"build": {
+		"dockerfile": "../.docker/debian/mathlib/Dockerfile",
+	},
+
+	// Set *default* container specific settings.json values on container create.
+	"settings": {
+		"terminal.integrated.shell.linux": "/bin/bash"
+	},
+
+	// Add the IDs of extensions you want installed when the container is created.
+	"extensions": ["jroesch.lean"],
+
+	// Use 'postCreateCommand' to run commands after the container is created.
+	// "postCreateCommand": "uname -a",
+
+	// Comment out connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root.
+	"remoteUser": "lean"
+}

.docker/README.md

@@ -0,0 +1,67 @@
+# Docker containers
+
+The `.docker` directory contains instructions for building Docker containers
+with Lean and mathlib.
+
+## Build
+
+You can build these containers using `scripts/docker_build.sh`.
+This will result in the creation of two containers:
+
+* `leanprovercommunity/lean` - contains elan, lean, and leanproject
+* `leanprovercommunity/mathlib` - additionally contains a copy of mathlib, with oleans
+
+In fact, for each container you'll get three different tags, `:debian`, `:alpine` and `:latest`.
+`:debian` and `:alpine` use those respective distributions, and `:latest` just points at `:debian`.
+Finally, there is also a `leanprovercommunity/mathlib:gitpod` for use at
+[https://gitpod.io/](https://gitpod.io/).
+
+## Usage
+
+### gitpod.io
+
+There is a container based on `gitpod/workspace-base`
+enabling [https://gitpod.io/](https://gitpod.io/) to create in-browser VSCode sessions
+with elan/lean/leanproject/mathlib already set up.
+
+Either prepend `https://gitpod.io/#` to basically any URL at github, e.g.
+[https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker](https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker),
+or install a [gitpod browser extension](https://www.gitpod.io/docs/browser-extension/)
+which will add buttons directly on github.
+
+You can enable gitpod for repositories importing mathlib as a dependency simply by creating
+the file `/.gitpod.yml` containing:
+
+```yml
+image: leanprovercommunity/mathlib:gitpod
+
+vscode:
+  extensions:
+    - jroesch.lean
+
+tasks:
+  - command: . /home/gitpod/.profile && leanproject get-mathlib-cache
+```
+
+### Command line
+
+You can use these containers as virtual machines:
+
+```sh
+docker run -it leanprovercommunity/mathlib
+```
+
+### Docker registry
+
+These containers are deployed to the Docker registry, so anyone can just
+`docker run -it leanprovercommunity/mathlib` to get a local lean+mathlib environment.
+
+There is a local script in `scripts/docker_push.sh` for deployment,
+but I have also set up `hub.docker.com` to watch the `docker` branch for updates
+and automatically rebuild.
+
+If this PR is merged to master we should change that to watch `master`.
+
+### Remote containers for VSCode
+
+See `/.devcontainer/README.md`.

.docker/alpine/lean/.profile

@@ -0,0 +1,6 @@
+# set PATH so it includes user's private bin if it exists
+if [ -d "$HOME/.local/bin" ] ; then
+    PATH="$HOME/.local/bin:$PATH"
+fi
+
+PATH="$HOME/.elan/bin:$PATH"

.docker/alpine/lean/Dockerfile

@@ -0,0 +1,79 @@
+# This is an alternative Dockerfile, for `leanprovercommunity/lean:alpine`,
+# based on `alpine`, and installs `elan` and `leanproject`.
+# See also the image `leanprovercommunity/mathlib` which contains a copy of mathlib.
+
+# `elan` doesn't include a release for `x86_64-unknown-linux-musl`,
+# so we roll our own
+FROM clux/muslrust as elan-builder
+
+RUN git clone https://github.com/Kha/elan.git .
+RUN cargo build --release
+
+# To save some space, we make another intermediate container in which we install
+# elan and whichever toolchain mathlib currently needs.
+# We later COPY out just the ~/.elan directory into our final container.
+FROM alpine as elan-install
+
+RUN apk update && apk add --no-cache curl
+
+RUN adduser -D lean
+USER lean
+WORKDIR /home/lean
+COPY --from=elan-builder /volume/target/x86_64-unknown-linux-musl/release/elan-init .
+RUN ./elan-init -y && rm elan-init && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan toolchain uninstall stable
+
+# We make another temporary `builder` container, from https://github.com/six8/pyinstaller-alpine
+# in which we install `python` and prepare a standalone version of `leanproject`.
+# This saves including a huge layer containing a python environment.
+FROM six8/pyinstaller-alpine:alpine-3.6-pyinstaller-v3.4 as leanproject-builder
+
+USER root
+# install prerequisites
+RUN apk update && apk add --no-cache python3 py3-pip py3-virtualenv
+# create a non-root user
+RUN adduser -D lean
+
+USER lean
+WORKDIR /home/lean
+
+ENV PATH="/home/lean/.local/bin:$PATH"
+
+# install `leanproject` using `pip`
+RUN python3 -m pip install --user mathlibtools
+
+# run `pyinstaller` on the installed copy of `leanproject`
+WORKDIR /home/lean/.local/bin
+RUN /pyinstaller/pyinstaller.sh --onefile --noconfirm leanproject
+# this has created `/home/lean/.local/bin/dist/leanproject`,
+# which we'll now copy to a fresh container
+
+# Now we start the `alpine` build.
+FROM alpine
+
+USER root
+# install prerequisites
+# (leanpkg assumes bash)
+RUN apk update && apk add --no-cache bash curl git openssh
+# create a non-root user
+RUN adduser -D lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/ash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/ash", "-l"]
+
+# install elan
+COPY --from=elan-install /home/lean/.elan /home/lean/.elan
+
+COPY .profile .
+
+# install leanproject
+COPY --from=leanproject-builder /home/lean/.local/bin/dist/leanproject /home/lean/.local/bin/
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"

.docker/alpine/mathlib/Dockerfile

@@ -0,0 +1,11 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:alpine`.
+# It is based on the `leanprovercommunity/lean:alpine` image,
+# and contains a cloned copy of the `mathlib` github repository,
+# along with precompiled oleans.
+
+FROM leanprovercommunity/lean:alpine
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+# clone a copy of mathlib, and download precompiled oleans
+RUN leanproject get mathlib

.docker/debian/lean/Dockerfile

@@ -0,0 +1,57 @@
+# This is the Dockerfile for `leanprovercommunity/lean`.
+# It is based on the generic `debian` image, and installs `elan` and `leanproject`.
+# See also the image `leanprovercommunity/mathlib` which contains a copy of mathlib.
+
+# NOTE: to run this docker image on macos or windows,
+# you will need to increase the allowed memory (in the docker GUI) beyond 2GB
+
+# We start with a temporary `builder` container,
+# in which we install `python` and prepare a standalone version of `leanproject`.
+FROM debian as leanproject-builder
+
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git python3 python3-pip python3-venv -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+ENV PATH="/home/lean/.local/bin:$PATH"
+
+# install `leanproject` using `pip`
+RUN python3 -m pip install --user mathlibtools
+
+# now install `pyinstaller`, and run it on the installed copy of `leanproject`
+RUN python3 -m pip install --user pyinstaller
+WORKDIR /home/lean/.local/bin
+RUN pyinstaller --onefile --noconfirm leanproject
+# this has created `/home/lean/.local/bin/dist/leanproject`,
+# which we'll now copy to a fresh container
+
+# We now build the final container.
+FROM debian
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+# install elan
+RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan toolchain uninstall stable
+# install leanproject
+COPY --from=leanproject-builder /home/lean/.local/bin/dist/leanproject /home/lean/.local/bin/

.docker/debian/mathlib/Dockerfile

@@ -0,0 +1,11 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib`.
+# It is based on the `leanprovercommunity/lean` image,
+# and contains a cloned copy of the `mathlib` github repository,
+# along with precompiled oleans.
+
+FROM leanprovercommunity/lean:debian
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+# clone a copy of mathlib, and download precompiled oleans
+RUN leanproject get mathlib

.docker/gitpod/mathlib/Dockerfile

@@ -0,0 +1,30 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM gitpod/workspace-base
+
+USER root
+
+RUN apt-get update && apt-get install curl git python3 python3-pip python3-venv -y
+
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# install elan
+RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
+# install `leanproject` using `pip`
+# RUN python3 -m pip install --user mathlibtools
+RUN python3 -m pip install --user pipx && python3 -m pipx ensurepath && source ~/.profile && pipx install mathlibtools
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

.github/PULL_REQUEST_TEMPLATE.md

@@ -14,3 +14,5 @@ using the following format:
 - [ ] depends on: #abc [optional extra text]
 - [ ] depends on: #xyz [optional extra text]
 -->
+
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

.gitpod.yml

@@ -0,0 +1,9 @@
+image:
+  file: .docker/gitpod/mathlib/Dockerfile
+
+vscode:
+  extensions:
+    - jroesch.lean
+
+tasks:
+  - command: . /home/gitpod/.profile && leanproject get-mathlib-cache

README.md

@@ -3,6 +3,7 @@
 ![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
 [![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
 [![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
+[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
 
 [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
 It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter.

scripts/docker_build.sh

@@ -0,0 +1,12 @@
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+
+cd $DIR/../.docker/debian/lean && \
+docker build -t leanprovercommunity/lean:debian -t leanprovercommunity/lean:latest . && \
+cd $DIR/../.docker/alpine/lean && \
+docker build -t leanprovercommunity/lean:alpine . && \
+cd $DIR/../.docker/debian/mathlib && \
+docker build -t leanprovercommunity/mathlib:debian -t leanprovercommunity/mathlib:latest .
+cd $DIR/../.docker/alpine/mathlib && \
+docker build -t leanprovercommunity/mathlib:alpine .
+cd $DIR/../.docker/gitpod/mathlib && \
+docker build -t leanprovercommunity/mathlib:gitpod .

scripts/docker_push.sh

@@ -0,0 +1,15 @@
+# This script attempts to build all the docker images, and then push then to the repository.
+# You'll need to have run `docker login` already;
+# check with [email protected] for credentials.
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+
+cd $DIR
+./docker_build.sh
+docker push leanprovercommunity/lean:latest
+docker push leanprovercommunity/lean:debian
+docker push leanprovercommunity/lean:alpine
+docker push leanprovercommunity/mathlib:latest
+docker push leanprovercommunity/mathlib:debian
+docker push leanprovercommunity/mathlib:alpine
+docker push leanprovercommunity/mathlib:gitpod