From 30298f17c8c63c3a91bcf26f67180973244a9d8e Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Mon, 19 Aug 2024 10:32:46 +0100 Subject: [PATCH] Add 4 suffix to images and add date tags Signed-off-by: zeramorphic --- .docker/gitpod-blueprint/Dockerfile | 47 +++++++++++++++++++++++++++++ .docker/gitpod/Dockerfile | 8 ++--- .docker/lean/Dockerfile | 11 +++++-- .docker/mathlib/Dockerfile | 12 -------- scripts/docker_build.sh | 9 +++--- scripts/docker_push.sh | 12 +++++--- 6 files changed, 70 insertions(+), 29 deletions(-) create mode 100644 .docker/gitpod-blueprint/Dockerfile delete mode 100644 .docker/mathlib/Dockerfile diff --git a/.docker/gitpod-blueprint/Dockerfile b/.docker/gitpod-blueprint/Dockerfile new file mode 100644 index 0000000000000..882d902a65baa --- /dev/null +++ b/.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 diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile index 5db682b5831ef..5b3061fb54390 100644 --- a/.docker/gitpod/Dockerfile +++ b/.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" diff --git a/.docker/lean/Dockerfile b/.docker/lean/Dockerfile index 8f7c98ea37c05..1ada0a31f3d81 100644 --- a/.docker/lean/Dockerfile +++ b/.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 diff --git a/.docker/mathlib/Dockerfile b/.docker/mathlib/Dockerfile deleted file mode 100644 index 9c04caa2491cc..0000000000000 --- a/.docker/mathlib/Dockerfile +++ /dev/null @@ -1,12 +0,0 @@ -# This is the Dockerfile for `leanprovercommunity/mathlib`. -# It is based on the `leanprovercommunity/lean` image. - -# 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/lean is that this image -# bypasses a warning that could occur when trying to connect to github for the first time. - -FROM leanprovercommunity/lean:debian - -# ssh to github once to bypass the unknown fingerprint warning -RUN ssh -o StrictHostKeyChecking=no github.com || true diff --git a/scripts/docker_build.sh b/scripts/docker_build.sh index fa76a1ae5f262..822e71bb67fd2 100644 --- a/scripts/docker_build.sh +++ b/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 . diff --git a/scripts/docker_push.sh b/scripts/docker_push.sh index 9a5af01d8584a..793cf793b3bf2 100644 --- a/scripts/docker_push.sh +++ b/scripts/docker_push.sh @@ -3,11 +3,13 @@ # check with scott.morrison@gmail.com 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