Add Dockerfiles for lean and mathlib

Signed-off-by: zeramorphic <[email protected]>

.docker/gitpod/Dockerfile

@@ -1,12 +1,11 @@
 # This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+# As well as elan and mathlib, we also install leanblueprint and all of its dependencies.
 
-# 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 ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive latexmk graphviz graphviz-dev python3 python3-pip python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group
@@ -30,6 +29,9 @@ RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-li
 
 ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
 
+# install leanblueprint
+RUN python3 -m pip install leanblueprint invoke
+
 # fix the infoview when the container is used on gitpod:
 ENV VSCODE_API_VERSION="1.50.0"
 

.docker/lean/Dockerfile

@@ -0,0 +1,29 @@
+# This is the Dockerfile for `leanprovercommunity/lean`.
+# It is based on the generic `debian` image, and installs `elan` and the current stable version of `lean`.
+# See also the image `leanprovercommunity/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
+
+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/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan default stable

.docker/mathlib/Dockerfile

@@ -0,0 +1,9 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib`.
+# It is based on the `leanprovercommunity/lean` image.
+# This Dockerfile doesn't contain a copy of mathlib;
+# you should call `lake exe cache get` which will download the most recent version.
+
+FROM leanprovercommunity/lean:debian
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

scripts/docker_build.sh

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

scripts/docker_push.sh

@@ -0,0 +1,13 @@
+# 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/mathlib:latest && \
+docker push leanprovercommunity/mathlib:debian && \
+docker push leanprovercommunity/mathlib:gitpod