From 5c2ef51b44169355a92adcf1e9855d32a1572f7d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 15 Dec 2024 13:38:13 -0800
Subject: [PATCH] chore: add gitpod configuration (#6382)

This PR adds a dockerfile for use with Gitpod.

This provides all the dependencies, and kicks off a build once the
editor is opened for the first time.

It can be tested by going to
https://gitpod.io/#https://github.com/leanprover/lean4/pull/6382

This should make it less painful for users hoping to contribute small
lemmas to `Init/` and `Std/`; they can open gitpod and wait, rather than
having to read the docs to run a series of commands.
---
 .gitpod.Dockerfile | 14 ++++++++++++++
 .gitpod.yml        | 11 +++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 .gitpod.Dockerfile
 create mode 100644 .gitpod.yml

diff --git a/.gitpod.Dockerfile b/.gitpod.Dockerfile
new file mode 100644
index 0000000000..7472f7741d
--- /dev/null
+++ b/.gitpod.Dockerfile
@@ -0,0 +1,14 @@
+# You can find the new timestamped tags here: https://hub.docker.com/r/gitpod/workspace-full/tags
+FROM gitpod/workspace-full
+
+USER root
+RUN apt-get update && apt-get install git libgmp-dev libuv1-dev cmake ccache clang -y && apt-get clean
+
+USER gitpod
+
+# Install and configure elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+ENV PATH="/home/gitpod/.elan/bin:${PATH}"
+# Create a dummy toolchain so that we can pre-register it with elan
+RUN mkdir -p /workspace/lean4/build/release/stage1/bin && touch /workspace/lean4/build/release/stage1/bin/lean && elan toolchain link lean4 /workspace/lean4/build/release/stage1
+RUN mkdir -p /workspace/lean4/build/release/stage0/bin && touch /workspace/lean4/build/release/stage0/bin/lean && elan toolchain link lean4-stage0 /workspace/lean4/build/release/stage0
diff --git a/.gitpod.yml b/.gitpod.yml
new file mode 100644
index 0000000000..600c1a8c8a
--- /dev/null
+++ b/.gitpod.yml
@@ -0,0 +1,11 @@
+image:
+    file: .gitpod.Dockerfile
+
+vscode:
+  extensions:
+    - leanprover.lean4
+
+tasks:
+  - name: Release build
+    init: cmake --preset release
+    command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)