messed up updating mathlib

Stream: new members

[Hannah Fechtner]

Hi all -- I tried to update mathlib and seem to have broken things.

What I did : lake update (that was supposed to be lake update mathlib, I believe. oops)

That gave me some kind of error, so I pasted the new version info into lean-toolchain

and ran "lake update" again

Now everything in VSCode is in red, and I'm getting the following errors:

[Hannah Fechtner]

in terminal:

/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> curl --version
curl 8.6.0 (x86_64-apple-darwin23.0) libcurl/8.6.0 (SecureTransport) LibreSSL/3.3.6 zlib/1.2.12 nghttp2/1.61.0
Release-Date: 2024-01-31
Protocols: dict file ftp ftps gopher gophers http https imap imaps ipfs ipns ldap ldaps mqtt pop3 pop3s rtsp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS GSS-API HSTS HTTP2 HTTPS-proxy IPv6 Kerberos Largefile libz MultiSSL NTLM NTLM_WB SPNEGO SSL threadsafe UnixSockets

/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> git --version
git version 2.15.0

/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lean --version
Lean (version 4.8.0-rc1, x86_64-apple-darwin22.6.0, commit dcccfb73cb24, Release)
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> elan --version
elan 3.1.1 (71ddc6633 2024-02-22)


/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lean --version
Lean (version 4.8.0-rc1, x86_64-apple-darwin22.6.0, commit dcccfb73cb24, Release)
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lake --version
Lake version 5.0.0-dcccfb7 (Lean version 4.8.0-rc1)
/Users/hannahfechtner/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/src/lean> lean --version
Lean (version 4.8.0-rc1, x86_64-apple-darwin22.6.0, commit dcccfb73cb24, Release)
[Error - 12:37:23 PM] Request textDocument/codeAction failed.
  Message: elaboration interrupted
  Code: -32603
[Error - 6:02:26 PM] Request textDocument/completion failed.
  Message: elaboration interrupted
  Code: -32603
[Error - 7:30:51 PM] Request textDocument/codeAction failed.
  Message: elaboration interrupted
  Code: -32603
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lean --version
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.9.0-rc1, x86_64-apple-darwin22.6.0, commit be6c4894e0a6, Release)
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lake --version
Lake version 5.0.0-be6c489 (Lean version 4.9.0-rc1)
warning: ././lakefile.lean:79:2: warning: @[test_runner] has been deprecated, use @[test_driver] instead
warning: ././.lake/packages/batteries/lakefile.lean:24:2: warning: @[test_runner] has been deprecated, use @[test_driver] instead
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lean --version
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.8.0-rc2, x86_64-apple-darwin22.6.0, commit 873ef2d894af, Release)
/Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4> lake --version
Lake version 5.0.0-873ef2d (Lean version 4.8.0-rc2)
Watchdog error: Got `shutdown` request, expected an `exit` notification

[Hannah Fechtner]

and when I hit "restart file" I get the following in the infoview:

[Eric Wieser]

If you are working on mathlib itself, then you should not use lake update

[Eric Wieser]

You should be able to use git to revert the changes you made to the lake-manifest.json, to get back to where you were

[Hannah Fechtner]

thank you! took me a bit to fight github, but looks like it's working again!

[Hannah Fechtner]

... not quite.

as I understand it, I'm working in one big lean project. this contains a .lake, which has the "original" mathlib.

I'm working on a PR, so I have a copy of mathlib, also in that same big lean project.

However, it's not exactly the same: the "original", for whatever reason, does not contain, say Mathlib.Algebra.Group.Subsemigroup.Basic . My copy does (I did not create this file).

When I try to compile anything which depends on this file, I get :

/Users/hannahfechtner/.elan/toolchains/leanprover--lean4---v4.6.0-rc1/bin/lake setup-file /Users/hannahfechtner/Desktop/knotthings/knot_project/mathlib4/Mathlib/Algebra/Group/Subsemigroup/Membership.lean Init Mathlib.Algebra.Group.Subsemigroup.Basic` failed:

stderr:
error: 'Mathlib.Algebra.Group.Subsemigroup.Basic': no such file or directory (error code: 2)
  file: ./.lake/packages/mathlib/././Mathlib/Algebra/Group/Subsemigroup/Basic.lean

All Messages (1)

Restart File

This file has an error which prevented it from compiling, which I corrected (in mem_iInf, line 254, Set.forall_mem_range needed to be Set.forall_range_iff for the simp to work)

I'm still getting that same error

Why is it looking in .lake for that file? shouldn't it be looking in my own copy of mathlib4?

[Bolton Bailey]

Why is it looking in .lake for that file? shouldn't it be looking in my own copy of mathlib4?

Lake works by having a copy of mathlib4 in the .lake subdirectory of your project rather than referencing some other central copy of mathlib on your computer because if you have multiple projects that depend on different versions of mathlib, then these projects need to reference different mathlib folders.

You could try deleting .lake and recompiling. That sometimes works.

You could also try checking your lakefile.lean/lake-manifest.json to make sure that it is not referencing some old mathlib revision from before that file was first created back in May. If it is referencing a commit that old, your update probably failed. (In which case my advice is again to delete .lake folder and maybe also the manifest and try recompiling.)

[Ruben Van de Velde]

I'm not sure what your mean by "one big lean project" - I think that may be the source of your confusion. If you have a project outside mathlib, it will have a lakefile that defines that you depend on mathlib. This file will say you want to use the master branch of mathlib by default. If you instead want to use a version of mathlib that has results you put in a PR that is not merged yet, you can replace the "master" in the lakefile by the name of your branch