Trying to revive a broken Lean project

Stream: new members

[Terence Tao]

Hi everyone, this is my first time on this Zulip.

A few days ago I started a Lean4 project to formalize a mathematical proof I had recently written. The github repository is at https://github.com/teorth/symmetric_project . Unfortunately, I had recently tried to update my local copy of Mathlib (and simultaneously accepted a pull request from another user who had also updated) and this managed to break my local copy in a weird way. I then tried to create a fresh local copy using the instructions from https://leanprover-community.github.io/install/project.html ; this did indeed create a new copy, but now lean cannot recognize Mathlib or any other packages and so the copy is functionally useless. Here is a screenshot of the current status:

image.png

I can't tell whether the problem is because the master github repository is itself broken, or something additional needs to be done locally. Any suggestions would be greatly appreciated. Worst case I could start a completely new project and manually port over the small number of files I have, but I'm hoping there is a quicker fix.

[Matthew Ballard]

I cloned a copy and opened that file. I seem to be building the dependencies fine on my machine.

[Matthew Ballard]

How did you update your local copy of mathlib?

[Yaël Dillies]

Hey! Nice seeing you here. Can you screenshot the working tree? I just want to make sure you opened the folder containing lakefile.lean, and not a parent folder.

[Terence Tao]

By following the instructions in https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 . On my Windows machine there was the issue that it did not recognize the -L option in curl but I found a workaround.

[Terence Tao]

By working tree do you mean this:
image.png

[Terence Tao]

After updating the library, the git control panel stopped being responsive, the lean infoview reported all sorts of external errors, and the git output produced messages like this:
image.png
at this point I decided to abandon my old local copy and create a new one. Currently git seems to work fine and lean seems to be running, it just can't find any packages.

[Yaël Dillies]

Yes that's what I meant. You have opened the current folder. So it's not that.

[Yaël Dillies]

Terence Tao said:

After updating the library, the git control panel stopped being responsive

Ahah. What do you mean by "updating" exactly? running lake update? and what library? mathlib? Std?

[Ruben Van de Velde]

Odd. I cloned your project, ran lake exe cache get, and everything seems to work smoothly

[Terence Tao]

I opened a shell and entered in these commands as suggested on the lean community documents:

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

[though actually I used "Invoke-WebRequest -Uri https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -OutFile lean-toolchain" for the first line as I had an -L option that it was rejecting.]

[Yaël Dillies]

If a fresh copy has the same problem, we can rule out cache issues. Given that Matthew can't reproduce, it's probably an issue with your PATH.

[Terence Tao]

The fresh copy is broken in a different way from the original copy. The original copy is stuck doing some sort of git synchronization. The fresh copy has no git issues, but the only problem is the inability of lean to detect packages.

[Yaël Dillies]

lake update is currently discouraged. It's broken in subtle ways when working on a project downstream of mathlib. Where did you read that?

[Terence Tao]

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

[Anatole Dedecker]

lake update should be fine after getting the right toolchains, right? EDIT: no (because toolchain != manifest) but that shouldn't be a problem here anyways

[Terence Tao]

I'll try to see if I can at least start a completely new project (unrelated to this one) with my current setup to see if I have managed to break my local Lean installation and not just an individual project instance.

[Yaël Dillies]

Sorry, I am currently out of ideas. If you wish to continue working on your project, you can use Gitpod. Here's a link which should open your project in a new workspace: gitpod.io/#https://github.com/teorth/symmetric_project

[Henrik Böving]

Terence Tao said:

I opened a shell and entered in these commands as suggested on the lean community documents:

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

[though actually I used "Invoke-WebRequest -Uri https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -OutFile lean-toolchain" for the first line as I had an -L option that it was rejecting.]

can you try to build your project from the command line using just lake build? That way we can figure out if the issue is related to the way you are using vscode or if something is inherently broken with the way the project exists on your machine right now

[Mario Carneiro]

Yaël Dillies said:

Yes that's what I meant. You have opened the current folder. So it's not that.

Are you sure about that? It appears @Terence Tao did indeed open the parent of the folder, since there is an extra symmetric_project entry in the list. When you open the folder itself you will see the folder name in bold caps at the top, and then the files in the folder directly under that.

[Terence Tao]

OK, trying that now. By the way I was able to create a completely new project and everything seems to be functional there, so at least I don't seem to have completely broken my lean installation.

[Yaël Dillies]

Mario Carneiro said:

Yaël Dillies said:

Yes that's what I meant. You have opened the current folder. So it's not that.

Are you sure about that? It appears Terence Tao did indeed open the parent of the folder, since there is an extra symmetric_project entry in the list. When you open the folder itself you will see the folder name in bold caps at the top, and then the files in the folder directly under that.

Argh, that fine line of indentation is really hard to see.

[Terence Tao]

I ran lake build which ran fine, but when I opened the project again I encountered the same inability to locate packages.

image.png

image.png

[Yaël Dillies]

Following what Mario just said, could you try opening the symmetric_project folder in vscode rather than its parent?

[Terence Tao]

Was just trying that now actually. It's doing something slightly different, I'm getting the "waiting for lean server to start..." message

[Ruben Van de Velde]

Progress!

[Terence Tao]

Ooh! It works!

[Arend Mellendijk]

I feel like there really should be a clearer error message if you try to open file that imports mathlib and VS code can't find a lakefile, I remember being bitten by this same mistake a couple times when I started out

[Terence Tao]

OK that does seem to have been the issue, I managed to create the local copy one level deeper than necessary. Would it break things if I just moved the symmetric_project folder (which is the one that actually contains all the useful files) up one level so that I don't accidentally open the wrong folder again?

[Mario Carneiro]

no, that sounds like a good idea, the extra folder won't do anything but cause confusion

[Mario Carneiro]

you will have to close and reopen the VSCode instance after moving the folder though

[Terence Tao]

OK I moved the project out of the redundant folder and things still work, so looks like everything is resolved. Thanks for all the help!