leanmake choosing nix store over elan

Stream: lean4

[ohhaimark]

I'm trying to build a package with a Dockerfile. I would rather just use nix, but that is not an option.

I have the following Dockerfile:

FROM ubuntu:21.04

RUN apt-get update
RUN apt-get install build-essential bash curl -y

# Use a login shell so that the '~/.profile' modified by elan is sourced.
SHELL ["/bin/sh", "-lc"]

# Install elan and lean4
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none  -y
RUN elan default leanprover/lean4:4.0.0-m2

WORKDIR /app
COPY . .

RUN leanpkg configure
RUN leanpkg build bin

# ENTRYPOINT [ "bash", "-li" ]

And get the following output

Step 9/10 : RUN leanpkg configure
 ---> Running in 7341750684f6

WARNING: Lean version mismatch: installed version is leanprover/lean4:4.0.0, but package requires leanprover/lean4:4.0.0-m2

configuring PrimeLean4 0.1
Removing intermediate container 7341750684f6
 ---> a032a68066b7
Step 10/10 : RUN leanpkg build bin
 ---> Running in e7f3d21d955c

WARNING: Lean version mismatch: installed version is leanprover/lean4:4.0.0, but package requires leanprover/lean4:4.0.0-m2

configuring PrimeLean4 0.1

WARNING: Lean version mismatch: installed version is leanprover/lean4:4.0.0, but package requires leanprover/lean4:4.0.0-m2

> sh -c "/root/.elan/toolchains/leanprover--lean4---4.0.0-m2/bin/leanmake" LEAN_OPTS="" LEAN_PATH="././build" bin >&2    # in directory .
make: *** No rule to make target '/nix/store/prmyjkfnl47my9yvf3g3c4m77jv9r2zy-lean-stage1/lib/lean/Init.olean', needed by 'build/PrimeLean4.olean'.  Stop.
uncaught exception: external command exited with status 2
The command '/bin/sh -lc leanpkg build bin' returned a non-zero code: 1

So for some reason, leanpkg doesn't use the lean installed by elan even through running which lean gives me /root/.elan/bin/lean

What gives?

[ohhaimark]

I have gotten it to use the elan toolchain, but leanmake doesn't seem to pick on an olean that is there.

FROM ubuntu:21.04

RUN apt-get update
RUN apt-get install build-essential bash curl -y

# Install elan and lean4
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none  -y

# Set shell to login shell so that ~/.profile is loaded
SHELL ["/bin/sh", "-lc"]
# Manually add elan to path as further shells aren't login shells and don't load ~/.profile
ENV PATH="$HOME/.elan/bin:${PATH}"

# Install lean toolchain early so that changes in source code don't
# trigger a redownload of lean
RUN elan toolchain install leanprover/lean4:4.0.0-m2

WORKDIR /app
COPY . .

RUN leanpkg configure
RUN leanpkg build bin

# ENTRYPOINT [ "bash", "-li" ]

> sh -c "/root/.elan/toolchains/leanprover--lean4---4.0.0-m2/bin/leanmake" LEAN_OPTS="" LEAN_PATH="././build" bin >&2    # in directory .
make: *** No rule to make target '/home/reuben/.elan/toolchains/leanprover--lean4---4.0.0-m2/bin/../lib/lean/Init.olean', needed by 'build/PrimeLean4.olean'.  Stop.
uncaught exception: external command exited with status 2

[ohhaimark]

Ah, I see now it's trying my $HOME '/home/reuben' instead of the docker $HOME '/root'.

[ohhaimark]

Ah, It's because the generated depend files were being included from the source of the Docker build, rather then being build in the container.

[ohhaimark]

Finally running with .dockerignore and:

FROM ubuntu:21.04

RUN apt-get update

# Install elan and lean4
RUN apt-get install curl -y
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none  -y

# Set shell to login shell so that ~/.profile is loaded
SHELL ["/bin/sh", "-lc"]

# Install lean toolchain early so that changes in source code don't
# trigger a redownload of lean
RUN elan toolchain install leanprover/lean4:4.0.0-m2
RUN apt-get install build-essential libgmp-dev -y

WORKDIR /app
COPY . .

RUN leanpkg configure
RUN leanpkg build bin
ENTRYPOINT [ ./build/bin/PrimeLean4 ]