chore(.docker): don't install unnecessary toolchains (#10363)

Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Nov 17, 2021 · f8cbb3e · f8cbb3e
1 parent 5d1363e
commit f8cbb3e
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/.docker/debian/lean/Dockerfile b/.docker/debian/lean/Dockerfile
@@ -49,9 +49,8 @@ ENTRYPOINT ["/bin/bash", "-l"]
 ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
 
 # install elan
-RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y && \
+RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
     . ~/.profile && \
-    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
-    elan toolchain uninstall stable
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
 # install leanproject
 COPY --from=leanproject-builder /home/lean/.local/bin/dist/leanproject /home/lean/.local/bin/
diff --git a/.docker/gitpod/mathlib/Dockerfile b/.docker/gitpod/mathlib/Dockerfile
@@ -14,7 +14,7 @@ WORKDIR /home/gitpod
 SHELL ["/bin/bash", "-c"]
 
 # install elan
-RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y
+RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
 # install whichever toolchain mathlib is currently using
 RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
 # install `leanproject` using `pip`