My CoCalc Lean stuck at v3.5.1

Stream: general

[Vaibhav Karve]

I need help upgrading the Lean version on CoCalc to the latest Lean + Mathlib. I have the latest version in my leanpkg.toml file. Runningleanproject up in a terminal window on CoCalc gives me a warning:

WARNING: Lean version mismatch: installed version is 3.5.1, but package requires leanprover-community/lean:3.15.0

mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 55, done.
remote: Counting objects: 100% (55/55), done.
remote: Compressing objects: 100% (49/49), done.
remote: Total 52062 (delta 21), reused 14 (delta 6), pack-reused 52007
Receiving objects: 100% (52062/52062), 22.35 MiB | 15.75 MiB/s, done.
Resolving deltas: 100% (40220/40220), done.
> git checkout --detach 8535132345bc8c4f48b56ebf89e0db5bcad8b456    # in directory _target/deps/mathlib
HEAD is now at 85351323 refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring (#2084)

WARNING: Lean version mismatch: installed version is 3.5.1, but package requires leanprover-community/lean:3.15.0

configuring leanteach 0.1
mathlib: trying to update _target/deps/mathlib to revision 8535132345bc8c4f48b56ebf89e0db5bcad8b456
> git checkout --detach 8535132345bc8c4f48b56ebf89e0db5bcad8b456    # in directory _target/deps/mathlib
HEAD is now at 85351323 refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring (#2084)
Looking for local mathlib oleans
Found local mathlib oleans

I understand that there is a version mismatch. But how do I fix said mismatch?

[Alex J. Best]

I'm not sure if you can at the moment, but @Harald Schilly and @William Stein are the ones who can say with certainty.

[William Stein]

Hi, you basically need to change your PATH and then have your own complete separate install of lean. Moreover, you need to ensure that when cocalc starts a lean server it starts the one in your PATH (rather than the systemwide one). Unfortunately this "Moreover" step is possibly not possible /easy right now. Fortunately, @Harald Schilly @Harald Schilly did a bunch of work today on exactly making customizing the environment possible (here: https://github.com/sagemathinc/cocalc/pull/4649).

[Vaibhav Karve]

Thank you. I'll give this a try and see how it goes.

[Harald Schilly]

@Vaibhav Karve sorry, I don't know anything about leanproject. If you bring your own lean executables and put them into or link to them from ~/bin/ in a cocalc project, they're in said PATH. I don't know if leanproject will recognize them, or if it even works inside a cocalc project. If you're lucky, it would be nice to know the steps you took.