mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
5c2ef51b44
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.
12 lines
220 B
YAML
12 lines
220 B
YAML
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)
|