From 651c06ca1e61520f812f4395a797c7d9091468a5 Mon Sep 17 00:00:00 2001
From: Adam Topaz <github@adamtopaz.com>
Date: Mon, 20 Mar 2023 22:37:42 +0000
Subject: [PATCH] feat: Update devcontainer.json + add Dockerfile (#2998)

This PR removes the external dependency for `devcontainer.json` by using a dockerfile to install elan.

Another feature is that `lake exe cache get!` is now done using `onCreateCommand` instead of `postCreateCommand`, so the oleans should be available as soon as the container is created, whereas before the user had to wait a little while, which was potentially confusing.
---
 .devcontainer/Dockerfile        |  8 ++++++++
 .devcontainer/devcontainer.json | 12 +++++++-----
 2 files changed, 15 insertions(+), 5 deletions(-)
 create mode 100644 .devcontainer/Dockerfile

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" ]