Cannot determine lean version in lean4 repo

Stream: lean4

[Thomas Murrills]

When opening the lean4 repo in VS code, I'm hit with the error "Cannot determine lean version". The output is this:

[rootfolder]/lean4> lean +lean4 --version
info: downloading component 'lean'

Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })

error: could not download nonexistent lean version `lean4`
info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/lean4' to '/Users/thomas/.elan/tmp/6735_xeuan5d47e0_file'
info: caused by: http request returned an unsuccessful status code: 404

=> Operation failed. Exit code: 1.

Does anyone know why this is happening? I can work on the mathlib4 and std4 repos just fine.

[Mac Malone]

Lean is meant to be built with itself. Thus, you should build a copy from the source by following the Development Setup instructionsin the Lean Manual and linking the custom toolchain as lean4 (as the aforementioned documentation suggests).

[Thomas Murrills]

This has never been a problem before, though.

[Thomas Murrills]

Further, having to build lean each time I want to modify the lean4 repo would be prohibitive on my machine (and relinking the toolchain as lean4 each time I want to mess around on different branches would be inconvenient). Did something change which now stops it from just grabbing an appropriate toolchain?

[Sebastian Ullrich]

It didn't grab an appropriate toolchain before, it just defaulted to your elan toolchain default. You could use elan override on the lean4 directories to restore that behavior.

[Thomas Murrills]

Ah, I see. Thanks! :)

[Thomas Murrills]

(I suppose in an ideal world it would pull the most recent toolchain available (or a PR release toolchain), but I imagine there are far bigger fish to fry.)

[Yuxi Liu]

I was hit by this as well.

Just a reminder, if you use nix-shell to set up the build environment, the nix flake lock version's CCache is at 4.8.1 (at least for aarch64-darwin/macOS), which fails to compile due to a test script error. It's fixed by this patch and the patch was released in 4.8.2. I got it working on my local branch with a nix flake update, which bumps CCache to 4.8.3. If there are no other problems, I think the flake lock should be bumped? I can submit a PR if needed.

[Sebastian Ullrich]

@Yuxi Liu Yes, please do

[Yuxi Liu]

Sebastian Ullrich said:

Yuxi Liu Yes, please do

Done. Issue: #3048, PR: #3050.