Can't run lean 3 project

Stream: general

[Kevin Buzzard]

I have a student working on some model theory and they have a problem which was solved in Lean 3 in the flypitch project. I wanted to take a look at what was done there but I can no longer get it to work (I cloned it fine):

buzzard@buster:~/lean-projects/flypitch$ leanproject get-mathlib-cache
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `3.4.2`
info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/v3.4.2' to '/home/buzzard/.elan/tmp/aru_sptirnlkmcf0_file'
info: caused by: http request returned an unsuccessful status code: 404
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

I see it's trying to download lean 3.4.2 from the lean 4 releases. Is there a fix for this? leanproject build gives me the same error.

[Shreyas Srinivas]

Are you able to open the repository on gitpod?

[Kevin Buzzard]

Sorry, I have no idea how to do that if there's not a gitpod button in the README. The repo is this https://github.com/flypitch/flypitch

[Shreyas Srinivas]

easy way: Install the gitpod extension on your browser

[Shreyas Srinivas]

Here's a direct URL : gitpod.io/#https://github.com/flypitch/flypitch

[Yaël Dillies]

Kevin Buzzard said:

Sorry, I have no idea how to do that if there's not a gitpod button in the README. The repo is this https://github.com/flypitch/flypitch

All you need to do is add gitpod.io/# before the repo name

[Shreyas Srinivas]

@Yaël Dillies : different subject : why is the gitpod image installing the lean4 extension and which is in tunr asking me to install lean4?

[Shreyas Srinivas]

Fwiw, I am getting the same error as Kevin on gitpod

[Yaël Dillies]

Extensions are not managed by the image but by the .gitpod.yml

[Shreyas Srinivas]

Yes, but the flypitch repo doesn't have a gitpod.yml config file

[Shreyas Srinivas]

Given that the same error occurs inside and outside the docker container, I think elan just isn't able to fetch lean3 images and picks a default lean4 toolchain instead. @Kevin Buzzard : if making a PR to flypitch is okay, I can add a .gitpod.yml file that might just use an existing lean3 image and work. (CC: @Floris van Doorn )

[Shreyas Srinivas]

I can confirm that my solution will work since I just opened mathlib3 successfully on gitpod

[Sebastian Ullrich]

Try

-lean_version = "3.4.2"
+lean_version = "leanprover-community/lean:v3.4.2"

[Kevin Buzzard]

In leanpkg.toml? Now I get

buzzard@buster:~/lean-projects/flypitch$ leanproject build
Building project flypitch
info: downloading component 'lean'
error: binary package was not provided for 'linux'
Command '['leanpkg', 'configure']' returned non-zero exit status 1.
buzzard@buster:~/lean-projects/flypitch$

[Floris van Doorn]

It works locally for me, presumably because I have the correct Lean version already installed (although actually when I run Lean locally I seem to have some LEAN_PATH issues later).
PRs to Flypitch improving the situation (Gitpod/leanpkg.toml fixes) are welcome.

[Julian Berman]

Sebastian Ullrich said:

Try

-lean_version = "3.4.2"
+lean_version = "leanprover-community/lean:v3.4.2"

Don't you mean leanprover/lean:v3.4.2? EDIT: no, that similarly seems to say "no binary package provided".

[Julian Berman]

Ah the issue is something (elan?) doesn't know how to follow github redirects. PR incoming.

[Julian Berman]

https://github.com/flypitch/flypitch/pull/41

[Shreyas Srinivas]

PR for gitpod incoming

[Shreyas Srinivas]

https://github.com/flypitch/flypitch/pull/40

[Shreyas Srinivas]

@Julian Berman I ended up also having to change leanpkg.toml

[Julian Berman]

I'm happy to close mine if unneeded, but does what you changed in the leanpkg.toml work for you? For me in Gitpod Sebastian's change didn't work and I needed what I did.

[Shreyas Srinivas]

It didn't. May I borrow your change?

[Shreyas Srinivas]

Mine also adds the gitpod stuff

[Julian Berman]

Sure, go for it.

[Shreyas Srinivas]

Now gitpod works, but leanproject cache can't find oleans

[Shreyas Srinivas]

Looking for flypitch oleans for 95fad36 locally...

[Shreyas Srinivas]

Oh wait that's just for flypitch files. Probably doesn't matter

[Shreyas Srinivas]

so the gitpod setup appears to work, but takes a while to setup. Let me see if I can get it working on the docker images that Yael maintains

[Shreyas Srinivas]

So the PR "works" although it seems to take forever for the yellow bar to disappear when opening a file in the project. I conjecture that this is because the flypitch project itself needs to be build. PR 40 is ready for review @Floris van Doorn

[Shreyas Srinivas]

I am getting a warning : WARNING: Lean version mismatch: installed version is 3.4.2, but package requires leanprover/lean3:3.4.2

[Notification Bot]

2 messages were moved here from #general > Dockerhub by Shreyas Srinivas.

[Eric Wieser]

Shreyas Srinivas said:

Julian Berman I ended up also having to change leanpkg.toml

This doesn't sound great, as it doesn't scale to every other abandoned lean3 project. Was the config wrong, or did something change with elan?

[Shreyas Srinivas]

I tested it again. Apparently the warning is a serious issue. leanproject does not get the cache at all. So the build command builds all of mathlib3

[Shreyas Srinivas]

Shreyas Srinivas said:

I am getting a warning : WARNING: Lean version mismatch: installed version is 3.4.2, but package requires leanprover/lean3:3.4.2

this warning