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