diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 0000000000000..a9bca17f5908f --- /dev/null +++ b/.devcontainer/Dockerfile @@ -0,0 +1,8 @@ +FROM mcr.microsoft.com/devcontainers/base:jammy + +USER vscode +WORKDIR /home/vscode + +RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none + +ENV PATH="/home/vscode/.elan/bin:${PATH}" diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 658bff66fd6a5..9d19495f1ab40 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,10 +1,12 @@ { - "name": "Ubuntu", - "image": "mcr.microsoft.com/devcontainers/base:jammy", - "features": { - "ghcr.io/adamtopaz/elan-feature/elan:0" : { "version" : "0.1.1" } + "name": "Mathlib4 dev container", + + "build": { + "dockerfile": "Dockerfile" }, - "postCreateCommand": "lake exe cache get!", + + "onCreateCommand": "lake exe cache get!", + "customizations": { "vscode" : { "extensions" : [ "leanprover.lean4" ]