elan, leanpkg and lake... I am lost

Stream: lean4

[Alexandre Rademaker]

OK, after one day fighting with Haskell tools (no solutions yet BTW, https://github.com/emacs-lsp/lsp-haskell/issues/154). I planned to have some peaceful time with Lean... but...

Elan supports both Lean4 and Lean3, right? But the repo says nothing about Lake, anyway, ignoring that below...

% elan show
installed toolchains
--------------------

stable
nightly
leanprover-community/lean:3.23.0
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-07-29
leanprover/lean4:nightly-2022-08-10
leanprover/lean4:stable (default)

active toolchain
----------------

leanprover/lean4:stable (default)
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

I thought, let me try to update Lean4 to the last version

% elan update leanprover/lean4:nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-08-19
info: downloading component 'lean'
Total: 132.1 MiB Speed:  11.1 MiB/s
info: installing component 'lean'

  leanprover/lean4:nightly updated - (lean does not exist)

Wow! What the 'lean does not exist' means? Let us see what happen.. nothing:

ar@tenis ~ % elan show
installed toolchains
--------------------

stable
nightly
leanprover-community/lean:3.23.0
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-07-29
leanprover/lean4:nightly-2022-08-10
leanprover/lean4:stable (default)

active toolchain
----------------

leanprover/lean4:stable (default)
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
``

I prefer Emacs, but I watch the video pointed by the docs to learn something. The video talks about the https://github.com/leanprover/lean4-samples/blob/main/HelloWorld/lean-toolchain example. Note that only `leanprover/lean4:nightly` was defined and VS Code seems to work well with that. But not Emacs.. I changed my project to that and  I got error in the `lean4-lsp:stderr` buffer:

error: toolchain 'leanprover/lean4:nightly' does not have the binary /Users/ar/.elan/toolchains/leanprover--lean4---nightly/bin/lean

I finally tried to install the version given the complete date

% elan toolchain install leanprover/lean4:nightly-2022-08-15
info: downloading component 'lean'
Total: 132.1 MiB Speed: 3.9 MiB/s
info: installing component 'lean'

leanprover/lean4:nightly-2022-08-15 installed - (lean does not exist)

So what is going on here? How can I have only the nightly and maybe lean3-community toolchains and let elan update them for me whenever I run `elan update`?

[Juan Pablo Romero]

I've noticed that some of the daily builds are broken, as in, the artifact is missing some binaries.
A working build should look like this:

$  ls -l ~/.elan/toolchains/leanprover--lean4---nightly-2022-08-09/bin
-rwxr-xr-x  1 jpablo  staff   167K Aug  9 00:19 clang
-rwxr-xr-x  1 jpablo  staff   2.5M Aug  9 00:28 lake
-rwxr-xr-x  1 jpablo  staff   4.2M Aug  9 00:19 ld64.lld
-rwxr-xr-x  1 jpablo  staff    49K Aug  9 00:27 lean
-rwxr-xr-x  1 jpablo  staff    70K Aug  9 00:27 leanc
-rwxr-xr-x  1 jpablo  staff   839B Aug  9 00:18 leanmake
-rwxr-xr-x  1 jpablo  staff   101K Aug  9 00:19 llvm-ar

If it's missing something you'll get the error you mentioned.

[Juan Pablo Romero]

the workaround is to delete the broken build and try another from a different date

[Chris Lovett]

Ok, I think I know what's going on. We recently changed the lean4-samples to use leanprover/lean4:nightly so that our nightly schedules builds would pick up any new build breaks from the latest lean bits that it installs. When you don't specify a date, elan installs the latest. BUT, here's the catch. If you already have a very old version of leanprover/lean4:nightly installed, elan does not update it. It's kind of operating as a cache. So this is what I've been doing to fix that:

elan toolchain uninstall leanprover/lean4:nightly
elan toolchain install leanprover/lean4:nightly

If you do that, now the lean4-samples should behave like you see in the CI build.

[Sebastian Ullrich]

You can use elan update for that, like in the first post

[Alexandre Rademaker]

but @Sebastian Ullrich and @Chris Lovett , see the outputs

% elan show
no active toolchain

ar@tenis ~ % elan -v toolchain install leanprover/lean4:nightly
verbose: updating existing install for 'leanprover/lean4:nightly'
verbose: toolchain directory: '/Users/ar/.elan/toolchains/leanprover--lean4---nightly'
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-08-20
info: downloading component 'lean'
verbose: creating temp file: /Users/ar/.elan/tmp/6jp35185in2g9hjy_file
verbose: downloading file from: 'https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-08-20'
verbose: downloading with curl
verbose: creating temp file: /Users/ar/.elan/tmp/89s8utnt9hv_b2g9_file
verbose: downloading file from: 'https://github.com//leanprover/lean4-nightly/releases/download/nightly-2022-08-20/lean-4.0.0-nightly-2022-08-20-darwin.tar.zst'
verbose: downloading with curl
Total: 132.4 MiB Speed:  11.2 MiB/s
info: installing component 'lean'
verbose: removing toolchain directory directory: '/Users/ar/.elan/toolchains/leanprover--lean4---nightly'
verbose: creating toolchain directory directory: '/Users/ar/.elan/toolchains/leanprover--lean4---nightly'
verbose: deleted temp file: /Users/ar/.elan/tmp/89s8utnt9hv_b2g9_file
verbose: deleted temp file: /Users/ar/.elan/tmp/6jp35185in2g9hjy_file
verbose: toolchain 'leanprover/lean4:nightly' installed

  leanprover/lean4:nightly updated - (lean does not exist)

So after the install, note the message lean does not exist. Moreover, no lean binary in the expected place and no active toolchain:

ar@tenis ~ % ls .elan/toolchains/leanprover--lean4---nightly/bin/
GNUSparseFile.0 clang       lake        ld64.lld    leanmake    llvm-ar

ar@tenis ~ % elan show
no active toolchain

If I try another installation:

ar@tenis ~ % elan -v toolchain install leanprover/lean4:nightly
verbose: updating existing install for 'leanprover/lean4:nightly'
verbose: toolchain directory: '/Users/ar/.elan/toolchains/leanprover--lean4---nightly'
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-08-20
verbose: toolchain is already up to date

  leanprover/lean4:nightly unchanged - (lean does not exist)

If I uninstall it and install again, same problem!

[Alexandre Rademaker]

I'm starting to be suspicious of the latest MacOS update. Now running MacOS Monterey 12.5.1.

[Sebastian Ullrich]

Hmm, there definitely is a bin/lean in https://github.com//leanprover/lean4-nightly/releases/download/nightly-2022-08-20/lean-4.0.0-nightly-2022-08-20-darwin.tar.zst

lean-4.0.0-nightly-2022-08-20-darwin/bin/lean: Mach-O 64-bit x86_64 executable, flags:<NOUNDEFS|DYLDLINK|TWOLEVEL|PIE>

[Mauricio Collares]

(deleted)

[Mauricio Collares]

This GNUSparseFile.0 directory is really suspicious

[Sebastian Ullrich]

That sounds like https://github.com/leanprover/elan/issues/78

[Mauricio Collares]

But I assume a (corrupted) lean binary is inside the GNUSparseFile.0 directory

[Mauricio Collares]

I don't know what generates the tarballs, but perhaps passing --format=v7 to tar could help until tar-rs supports untarring sparse files.

[Sebastian Ullrich]

Let's give that a try https://github.com/leanprover/lean4/pull/1498

[Alexandre Rademaker]

Oh nice, but I installed elan from brew. So better uninstall it and install it directly ? Will that work now?

[Alexandre Rademaker]

Oh , I see now you changed the lean compressing approach , so I can try my current elan installation with the next lean nightly release , right ?

[Alexandre Rademaker]

BTW, yes, if I download the tar.zst file manually, I can expand it with tar --use-compress-program=unzstd -xvf lean-4.0.0-nightly-2022-08-19-darwin.tar.zst. But I don't want to mess with my elan installation, so I will wait the proper solution.

[Josh Clune]

Hi, I'm another Mac/brew user currently experiencing issues very similar to what @Alexandre Rademaker described. Was there a final verdict on what I should do?

Using brew to remove and reinstall elan, and using elan to uninstall and reinstall the nightly toolchain still yields the lean does not exist message for me, even though I believe that https://github.com/leanprover/lean4/pull/1498 has been merged. Should I sit tight for now, or is there something else I should try? I totally understand if the answer is just, wait, it should be fixed soon, I'm just looking to confirm whether there was a step that I overlooked/missed.

[Mauricio Collares]

A nightly (2022-08-22) with https://github.com/leanprover/lean4/pull/1499 should be available in about 8 hours

[Josh Clune]

Great, thanks!

[Alexandre Rademaker]

Indeed, after running the elan -v toolchain install leanprover/lean4:nightly I got Lean installed, but it is strange the output of the show command

% elan show
no active toolchain

[Sebastian Ullrich]

Is that in a project with a lean-toolchain file?

[Alexandre Rademaker]

no, outside a project, in my home folder

[Alexandre Rademaker]

Inside a project folder, I got

% elan show
leanprover/lean4:nightly (overridden by '/Users/ar/hpsg/mrs-lean/lean-toolchain')
Lean (version 4.0.0-nightly-2022-08-22, commit f8c7de5a64fc, Release)

[Julian Berman]

(FWIW my CI was broken yesterday with nightly for 08-20 on macOS, but appears to work now on 08-22, which I think means at least here something has been fixed.)

[Alexandre Rademaker]

sorry @Sebastian Ullrich , just rewrote my last message to make it clear.

[Mauricio Collares]

Use elan default leanprover/lean4:nightly to configure your default toolchain (the one that's used when you're not inside a project directory)

[Chris Lovett]

I added a CI nightly test of elan on macOS to the lean4-samples repo.