diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 000000000..a9bca17f5 --- /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 new file mode 100644 index 000000000..9f7ab7953 --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,19 @@ +{ + "name": "Lean-MLIR dev container", + + "build": { + "dockerfile": "Dockerfile" + }, + + "onCreateCommand": "lake exe cache get!", + + "hostRequirements": { + "cpus": 4 + }, + + "customizations": { + "vscode" : { + "extensions" : [ "leanprover.lean4" ] + } + } +}