From 57ff473c54d90785225d932afb4d146ca50f5bb8 Mon Sep 17 00:00:00 2001
From: Austin Letson <waustinletson@gmail.com>
Date: Thu, 11 Apr 2024 13:45:13 +0000
Subject: [PATCH 1/2] chore: add .gitpod.yml and .docker/gitpod/Dockerfile

---
 .docker/gitpod/Dockerfile | 41 +++++++++++++++++++++++++++++++++++++++
 .gitpod.yml               |  6 ++++++
 2 files changed, 47 insertions(+)
 create mode 100644 .docker/gitpod/Dockerfile
 create mode 100644 .gitpod.yml

diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile
new file mode 100644
index 0000000000..38dec79ecf
--- /dev/null
+++ b/.docker/gitpod/Dockerfile
@@ -0,0 +1,41 @@
+# This is the Dockerfile for leanprover/std4
+# This file is mostly copied from [mathlib4](https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile)
+
+# 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 gcc make -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 std4 is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover/std4/main/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
new file mode 100644
index 0000000000..5170403ac3
--- /dev/null
+++ b/.gitpod.yml
@@ -0,0 +1,6 @@
+image:
+  file: .docker/gitpod/Dockerfile
+
+vscode:
+  extensions:
+    - leanprover.lean4

From bb1fa8c348ef316ace763dc38b08aa765dee46a8 Mon Sep 17 00:00:00 2001
From: Austin Letson <waustinletson@gmail.com>
Date: Wed, 17 Apr 2024 22:26:13 +0000
Subject: [PATCH 2/2] chore: remove duplicate git and python3 from docker
 installs

---
 .docker/gitpod/Dockerfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile
index 38dec79ecf..ededb0b68a 100644
--- a/.docker/gitpod/Dockerfile
+++ b/.docker/gitpod/Dockerfile
@@ -7,7 +7,7 @@ FROM ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests gcc make -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl bash-completion python3-requests gcc make -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