elan 3.1.0/3.1.1 on Nixpkgs

Stream: lean4

[Mauricio Collares]

Nixpkgs (b8697e57f10292a6165a20f03d2f42920dfaf973) elan 3.1.0/3.1.1 is having problems after elan#121 because the wrapper generated by nix_patch_if_needed points to the temporary location files are now extracted to, not to their final destination. Output of lake exe cache get:

info: downloading component 'lean'
Total: 168.9 MiB Speed:  25.9 MiB/s
info: installing component 'lean'
info: [2/9] Compiling Cache.IO
info: [3/9] Compiling Cache.Hashing
info: [4/9] Compiling Cache.Requests
error: > /home/collares/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/leanc -c -o ./.lake/build/ir/Cache/IO.c.o ./.lake/build/ir/Cache/IO.c -O3 -DNDEBUG
error: stderr:
/home/collares/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/leanc: line 2: /home/collares/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig: No such file or directory
error: external command `/home/collares/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/leanc` exited with code 127

See also:

$ cat ~/.elan/toolchains/leanprover--lean4---v4.7.0-rc1/bin/leanc
#! /nix/store/087167dfxal194pm54cmcbbxsfy3cjgn-bash-5.2p26/bin/bash
LEAN_CC="${LEAN_CC:-/nix/store/ln6zld1ia7rxddmxgbpfhrmb42rbxdw8-gcc-wrapper-13.2.0/bin/cc}" exec -a "$0" /home/collares/.elan/toolchains/leanprover--lean4---v4.7.tmp/bin/leanc.orig "$@" -L /home/collares/.elan/toolchains/leanprover--lean4---v4.7.tmp/lib  # use bundled libraries, but not bundled compiler that doesn't know about NIX_LDFLAGS

[Kim Morrison]

I can't see anything strange about the v4.7.0-rc2 release... the diff from v4.7.0-rc1 is quite small.

[Mauricio Collares]

Sorry, you're right! I thought I had deleted the .lake directory but I didn't. This also affects v4.7.0-rc1, and I didn't notice because I used an older elan to install -rc1. This is fallout from elan#121. Edited my initial post to reflect this.

[Sebastian Ullrich]

Can we use a relative path?

[Joachim Breitner]

I think I just ran into this. Is someone working on this? (Using elan from nixpkgs stable for now.)

[Mauricio Collares]

https://github.com/NixOS/nixpkgs/pull/289941#issuecomment-1981132915 suggested temporarily reverting the temp dir change, while the relative path change is not implemented.

[Joachim Breitner]

Sebastian Ullrich said:

Can we use a relative path?

Probably not trivially, as the leanc will be called from other places, but the usual dance with

parent_path="$(dirname "${BASH_SOURCE[0]}")"

and then using that path below should work.

[Joachim Breitner]

https://github.com/NixOS/nixpkgs/pull/294514

[Johan Commelin]

Joachim Breitner said:

I think I just ran into this. Is someone working on this? (Using elan from nixpkgs stable for now.)

(how) can I do this, while keeping the rest on unstable?

[Mauricio Collares]

This is fixed on unstable now

[Mauricio Collares]

(with the caveat that you have to manually uninstall "bad" toolchains and let the newest version of elan reinstall them)