Zulip Chat Archive
Stream: lean4
Topic: elan toolchain link: three hyphens becomes colon?
Siddharth Bhat (Mar 31 2024 at 05:13):
I've observed some curious behaviour:
$ elan toolchain link xxx---yyy stage2/
$ elan toolchain list
error: invalid toolchain name: 'run-2024-03-30:15-19:tcg40'
My list of toolchains seem to be in order, including the xxx---yyy
toolchain:
ls -al $HOME/.elan/toolchains/
total 0
drwxr-xr-x 13 sid staff 416 31 Mar 06:09 .
drwxr-xr-x 8 sid staff 256 13 Mar 13:53 ..
lrwxr-xr-x 1 sid staff 51 22 Mar 15:29 lean4 -> /Users/sid/24/refcount/.lean4/build/current/stage1/
lrwxr-xr-x 1 sid staff 50 22 Mar 15:30 lean4-stage0 -> /Users/sid/24/refcount/.lean4/build/current/stage0
...
lrwxr-xr-x 1 sid staff 48 31 Mar 06:09 xxx---yyy -> /Users/sid/24/refcount/clean/build/reuse/stage2/
I'm totally unsure what's causing this behaviour. Is this some kind of known (expected) behaviour, or a bug?
Mac Malone (Mar 31 2024 at 05:30):
This sounds like a unintentional side effect of the fact that :
in a toolchain name is encoded as ---
in the directory name of standard Elan toolchains (e.g., leanprover/lean4:v4.0.0
is stored in the directory leanprover--lean4---v4.0.0
).
Last updated: May 02 2025 at 03:31 UTC