lean4 in Docker - download file; Mathlib missing

Stream: new members

[Ben]

I'm new to Lean and want to use Lean on the command line to evaluate the correctness of statements in a text file. My question is about a large file being downloaded everytime I run the Docker image.

I have a Docker image with Lean4 and I am using that to run the command

$ docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean4onubuntu lean --run hello.v4.lean

The result of that command is successful execution but also a large download everytime the command is executed.

info: downloading https://releases.lean-lang.org/lean4/v4.25.1/lean-4.25.0-linux_aarch64.tar.zst
473.1 MiB / 473.1 MiB (100 %)  56.8 MiB/s ETA:   0 s
info: installing /root/.elan/toolchains/leanprover--lean4---v4.25.1
Hello, world!
Hello, world!

What should I be doing differently with the Dockerfile to prevent this download?

The Dockerfile contains

# https://hub.docker.com/r/phusion/baseimage/tags
FROM phusion/baseimage:noble-1.0.2
WORKDIR /opt/
# https://leanprover-community.github.io/install/debian_details.html
RUN apt -y update && apt -y upgrade
RUN apt install -y curl git
# `git` is needed by `lake`

# as per https://stackoverflow.com/a/53605439/1164295
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf |\
       bash -s -- --default-toolchain leanprover/lean4:stable -y

ENV PATH="/root/.elan/bin:$PATH"

# as per https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
RUN mkdir /opt/new_project
WORKDIR /opt/new_project
RUN lake +leanprover-community/mathlib4:lean-toolchain new project_name math
# The purpose of lake new is to generate the initial project files based on a template
# inclusion of `math` omits `Main.lean` and declares Mathlib as a dependency in your lakefile.toml

WORKDIR /opt/new_project/project_name

# Next, read `lakefile.toml` in the current directory (/opt/new_project/project_name).
# Then identify the declared dependencies (in this case, Mathlib) and
# download and install these dependencies into your project.
RUN lake exe cache get

# cache the build of Mathlib
RUN echo "import Mathlib.Data.Real.Basic" > ProjectName/mathlib_test.v4.lean
RUN lake lean ProjectName/mathlib_test.v4.lean

For completeness, the contents of the hello.lean file are

def main : IO Unit := IO.println "Hello, world!"
#eval main

Thank you for your help!

[Ben]

Gemini 3 Pro (LLM) found a fix for the downloaded file

# https://hub.docker.com/r/phusion/baseimage/tags
FROM phusion/baseimage:noble-1.0.2
WORKDIR /opt/

RUN apt -y update && apt -y upgrade
RUN apt install -y curl git

RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf |\
       bash -s -- --default-toolchain leanprover/lean4:stable -y

ENV PATH="/root/.elan/bin:$PATH"

RUN mkdir /opt/new_project
WORKDIR /opt/new_project
RUN lake +leanprover-community/mathlib4:lean-toolchain new project_name math
# The purpose of lake new is to generate the initial project files based on a template
# inclusion of `math` omits `Main.lean` and declares Mathlib as a dependency in your lakefile.toml

# Download the version file directly from Mathlib repository first.
RUN curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

# Set the container's default toolchain to match the project
# This reads the version Mathlib wants and makes it the global default
RUN elan default "$(cat lean-toolchain)"

WORKDIR /opt/new_project/project_name

# Next, read `lakefile.toml` in the current directory (/opt/new_project/project_name).
# Then identify the declared dependencies (in this case, Mathlib) and download and install these dependencies into your project.
RUN lake exe cache get

# cache the build of Mathlib
RUN echo "import Mathlib.Data.Real.Basic" > ProjectName/mathlib_test.v4.lean
RUN lake lean ProjectName/mathlib_test.v4.lean

which works for

cat hello.v4.lean
def main : IO Unit := IO.println "Hello, world!"
#eval main

and the command

docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean4onubuntu lean hello.v4.lean
Hello, world!

[Notification Bot]

This topic was moved here from #new members > lean4 in Docker downloads 473 MB file by Ben.