Add 4 suffix to images and add date tags

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

.docker/gitpod-blueprint/Dockerfile

@@ -0,0 +1,47 @@
+# This is the Dockerfile for `leanprovercommunity/gitpod4-blueprint`.
+# As well as elan, we also install leanblueprint and all of its dependencies.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
+
+FROM ubuntu:jammy
+
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex 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
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
+RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
+
+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"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.docker/gitpod/Dockerfile

@@ -1,5 +1,4 @@
-# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
-# As well as elan and mathlib, we also install leanblueprint and all of its dependencies.
+# This is the Dockerfile for `leanprovercommunity/gitpod4`.
 
 # This container does not come with a pre-installed version of mathlib.
 # When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
@@ -10,7 +9,7 @@ FROM ubuntu:jammy
 USER root
 
 ENV DEBIAN_FRONTEND=noninteractive
-RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev python3 python3-pip python3-requests -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git bash-completion 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
@@ -34,9 +33,6 @@ 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

@@ -1,6 +1,10 @@
-# This is the Dockerfile for `leanprovercommunity/lean`.
+# This is the Dockerfile for `leanprovercommunity/lean4`.
 # It is based on the generic `debian` image, and installs `elan` and the current stable version of `lean`.
-# See also the image `leanprovercommunity/mathlib`.
+
+# This container does not come with a pre-installed version of mathlib;
+# you should call `lake exe cache get` which will download the most recent version.
+# The only difference between this Dockerfile and leanprovercommunity/lean4 is that this image
+# bypasses a warning that could occur when trying to connect to github for the first time.
 
 # NOTE: to run this docker image on macos or windows,
 # you will need to increase the allowed memory (in the docker GUI) beyond 2GB
@@ -27,3 +31,6 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -
     . ~/.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
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

scripts/docker_build.sh

@@ -1,8 +1,9 @@
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+DATE=$(date +"%Y-%m-%d")
 
 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 . && \
+docker build -t leanprovercommunity/lean4:$DATE -t leanprovercommunity/lean4:latest . && \
 cd $DIR/../.docker/gitpod && \
-docker build -t leanprovercommunity/mathlib:gitpod .
+docker build -t leanprovercommunity/gitpod4:$DATE -t leanprovercommunity/gitpod4:latest . && \
+cd $DIR/../.docker/gitpod-blueprint && \
+docker build -t leanprovercommunity/gitpod4-blueprint:$DATE -t leanprovercommunity/gitpod4-blueprint:latest .

scripts/docker_push.sh

@@ -3,11 +3,13 @@
 # check with [email protected] for credentials.
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+DATE=$(date +"%Y-%m-%d")
 
 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
+docker push leanprovercommunity/lean4:$DATE && \
+docker push leanprovercommunity/lean4:latest && \
+docker push leanprovercommunity/gitpod4:$DATE && \
+docker push leanprovercommunity/gitpod4:latest && \
+docker push leanprovercommunity/gitpod4-blueprint:$DATE && \
+docker push leanprovercommunity/gitpod4-blueprint:latest