Skip to content

Commit

Permalink
Add explanation
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Aug 18, 2024
1 parent afd3b17 commit d84e425
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 1 deletion.
4 changes: 4 additions & 0 deletions .docker/gitpod/Dockerfile
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
# As well as elan and mathlib, we also install leanblueprint and all of its dependencies.

# This container does not come with a pre-installed version of mathlib.
# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
# see the .gitpod.yml file for more information.

FROM ubuntu:jammy

USER root
Expand Down
5 changes: 4 additions & 1 deletion .docker/mathlib/Dockerfile
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
# This is the Dockerfile for `leanprovercommunity/mathlib`.
# It is based on the `leanprovercommunity/lean` image.
# This Dockerfile doesn't contain a copy of mathlib;

# This container does not come with a pre-installed version of mathlib;
# you should call `lake exe cache get` which will download the most recent version.
# The only difference between this Dockerfile and leanprovercommunity/lean is that this image
# bypasses a warning that could occur when trying to connect to github for the first time.

FROM leanprovercommunity/lean:debian

Expand Down

0 comments on commit d84e425

Please sign in to comment.