From da397c9742dab3e6060d0a6a8411d7c7f49ff61e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 1 Jun 2024 13:46:49 +0000
Subject: [PATCH] Reuse mathlib's docker image Even though it's ancient and
 installs the Lean 3 extension, it works for our purposes if we run `elan self
 update` afterwards.

---
 .docker/gitpod/Dockerfile | 40 ---------------------------------------
 .gitpod.yml               |  3 +--
 2 files changed, 1 insertion(+), 42 deletions(-)
 delete mode 100644 .docker/gitpod/Dockerfile

diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile
deleted file mode 100644
index e157390ec9..0000000000
--- a/.docker/gitpod/Dockerfile
+++ /dev/null
@@ -1,40 +0,0 @@
-# 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 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 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}"
-
-# 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/.gitpod.yml b/.gitpod.yml
index 82b6e0430d..e812af8e6c 100644
--- a/.gitpod.yml
+++ b/.gitpod.yml
@@ -1,5 +1,4 @@
-image:
-  file: .docker/gitpod/Dockerfile
+image: leanprovercommunity/mathlib:gitpod
 
 vscode:
   extensions: