Skip to content

Commit

Permalink
chore: add gitpod configuration (#6382)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
eric-wieser authored Dec 15, 2024
1 parent a8656c5 commit 5c2ef51
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 0 deletions.
14 changes: 14 additions & 0 deletions .gitpod.Dockerfile
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions .gitpod.yml
Original file line number Diff line number Diff line change
@@ -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)

0 comments on commit 5c2ef51

Please sign in to comment.