Bad paths with elan v3.1.1

[sbp]

Using Alpine Linux we can run elan-init version 3.1.1 to give us a stable LEAN4 toolchain:

# apk add -U gcompat git
# wget -O- https://github.com/leanprover/elan/releases/download/v3.1.1/elan-aarch64-unknown-linux-gnu.tar.gz | tar -C /usr/bin -zxf-
# elan-init -vy

This, in the output of elan-init, says that it's installing v4.9.1/lean-4.9.0-linux_aarch64.tar.zst. It appears to work, and we can source ~/.profile and use lake.

# source ~/.profile
# cd /tmp
# lake new example
error: could not detect the configuration of the Lake installation

But this results in an error. From some browsing around, it appeared that setting LAKE_HOME would fix the problem even though elan is documented to handle this sort of thing for the user. Anyway, setting an appropriate value of LAKE_HOME works for creating a new LEAN4 codebase.

# LAKE_HOME="$HOME/.elan/toolchains/stable" lake new example
# cd /tmp/example

Then we get another error if we try to run lake build:

# LAKE_HOME="$HOME/.elan/toolchains/stable" lake build
error: ././lakefile.lean:1:0: error: unknown package 'Init'
error: ././lakefile.lean:2:5: error: unknown namespace 'Lake'
error: ././lakefile.lean:4:0: error: unexpected identifier; expected command
error: ././lakefile.lean:10:17: error: unexpected identifier; expected 'abbrev', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
error: ././lakefile.lean: package configuration has errors

Again from more reading it appeared that setting LEAN_SYSROOT would fix it, but it just changes the error:

# LAKE_HOME="$HOME/.elan/toolchains/stable" LEAN_SYSROOT="$HOME/.elan/toolchains/stable" lake build
✖ [1/7] Building Example.Basic
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib /root/.elan/toolchains/stable/bin/lean ././././Example/Basic.lean -R ./././. -o ././.lake/build/lib/Example/Basic.olean -i ././.lake/build/lib/Example/Basic.ilean -c ././.lake/build/ir/Example/Basic.c --json
error: ././././Example/Basic.lean:1:0: unknown package 'Init'
error: ././././Example/Basic.lean:1:13: unknown constant 'String'
error: Lean exited with code 1
Some builds logged failures:
- Example.Basic
error: build failed

Logically, from the output, it seems that LEAN_PATH also has to be set, but its value is simply ignored:

# LAKE_HOME="$HOME/.elan/toolchains/stable" LEAN_SYSROOT="$HOME/.elan/toolchains/stable" LEAN_PATH="$HOME/.elan/toolchains/stable/lib" lake build
✖ [1/7] Building Example.Basic
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib /root/.elan/toolchains/stable/bin/lean ././././Example/Basic.lean -R ./././. -o ././.lake/build/lib/Example/Basic.olean -i ././.lake/build/lib/Example/Basic.ilean -c ././.lake/build/ir/Example/Basic.c --json
error: ././././Example/Basic.lean:1:0: unknown package 'Init'
error: ././././Example/Basic.lean:1:13: unknown constant 'String'
error: Lean exited with code 1
Some builds logged failures:
- Example.Basic
error: build failed

At this point it was unclear how to proceed any further, hence this issue.

[foxyseta]

Same here!