Lean fail to start for an unknown reason

Stream: lean4

[Ruize Chen]

image.png
I cloned a repository formalising-mathematics-2024, and I have the lean4 extension in my vscode, but when I tried to edit one of the files, lean was not working. normally It would show no goal or something like that, but no response. I tried to do the instructions for installing the lean4 (Actually it was just about installing git, vscode, and extension ). I even reinstalled the vscode, what can I do to fix this?

[Mac Malone]

Does the server still fail to start if you restart it via the Lean 4: Server: Restart Server command? You can access this command by opening the Command Palette in VSCode via Ctrl+Shift+P or Cmd+Shift+P )on MacOS), typing said command, and pressing enter.

[Ruben Van de Velde]

The red bar counts as a response of sorts. Does anything interesting show up if you click on "all messages" in the infoview?

[Ruize Chen]

Ruben Van de Velde said:

The red bar counts as a response of sorts. Does anything interesting show up if you click on "all messages" in the infoview?

the only message says:
Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.
I suppose I need to update something:face_with_monocle:

[Mario Carneiro]

that's the expected behavior, you are supposed to press the button

[Ruize Chen]

Mac Malone said:

Does the server still fail to start if you restart it via the Lean 4: Server: Restart Server command? You can access this command by opening the Command Palette in VSCode via Ctrl+Shift+P or Cmd+Shift+P )on MacOS), typing said command, and pressing enter.

It was still not working, I think it's about the import thing cause the message said that

[Mario Carneiro]

the fact that this message also fills the screen with a red highlight is something we plan to fix

[Ruize Chen]

Mario Carneiro said:

that's the expected behavior, you are supposed to press the button

but simply pressing the button"restart file" will give me the same response, I suppose I have something to update?

[Mario Carneiro]

if a popup did not appear, you can also manually trigger it using Lean 4: Server: Restart File from the Ctrl+Shift+P menu

[Mario Carneiro]

no you do not have to update anything, or at least the feedback so far does not indicate this

[Mario Carneiro]

another thing you can try is lake build from the terminal

[Ruize Chen]

Mario Carneiro said:

another thing you can try is lake build from the terminal

I will try this

[Mario Carneiro]

note that "Restart File" and "Restart Server" are different commands. Usually when you get in this state "Restart Server" will not fix it but "Restart File" will

[Ruize Chen]

I suppose there is somthing about lake cause when I tried for the first time I saw the message "lake file configuration changed" but only for once, I am trying the lake build. I believe the both restart commands cannot fix it cause I tried them both for a few times.

[Mario Carneiro]

cc: @Mac Malone do you know why the server would misinterpret "lake configuration changed" as "files are not up to date"?

[Ruize Chen]

It's working, thank you. after lake build and restarting the file

[Marc Huisinga]

Looks like I'll perhaps have to re-add the stale dependency notifications for older versions of Lean 4 where the fullRange span of the diagnostic doesn't cover the full file and the "Restart File" error doesn't show up under "Messages", only "All Messages".

[Marc Huisinga]

Mario Carneiro said:

cc: Mac Malone do you know why the server would misinterpret "lake configuration changed" as "files are not up to date"?

The "lake configuration changed" message is from the extension. We register file watchers for lakefile.lean and lean-toolchain and issue a notification to restart the server when these files change.
I'm not sure yet why this message triggers when opening this repo.

[Mario Carneiro]

oh, my interpretation was that lake was complaining that it needed a lake update

[Mario Carneiro]

when lake is in this state, will the server "Restart File" button work as intended?

[Marc Huisinga]

iz said:

Mario Carneiro said:

that's the expected behavior, you are supposed to press the button

but simply pressing the button"restart file" will give me the same response, I suppose I have something to update?

I cloned the repo, opened Sheet1.lean and clicked the "Restart File" button in the bottom right of the InfoView when the message showed up and it started building just fine, though lake exe get cache should have been run beforehand.

[Marc Huisinga]

Mario Carneiro said:

oh, my interpretation was that lake was complaining that it needed a lake update

I don't think Lake has the power to issue notifications with buttons that run VS Code commands :-)

Mario Carneiro said:

when lake is in this state, will the server "Restart File" button work as intended?

Yes.

[Mario Carneiro]

I'm not sure where lake's complaint goes when the server is calling lake (probably nowhere?)

[Mario Carneiro]

the situation that seems bad here that I'd like to get to the bottom of is where pressing "Restart File" causes it to fail and produce an error saying to try "Restart File" again

[Mario Carneiro]

I'm sure it's the result of bad local configuration but it's still not something that should happen

[Marc Huisinga]

I tested it and it seems to work fine. I suspect that @iz may have pressed the "Restart Server" button, not the "Restart File" button?

[Ruize Chen]

Marc Huisinga said:

iz said:

Mario Carneiro said:

that's the expected behavior, you are supposed to press the button

but simply pressing the button"restart file" will give me the same response, I suppose I have something to update?

I cloned the repo, opened Sheet1.lean and clicked the "Restart File" button in the bottom right of the InfoView when the message showed up and it started building just fine, though lake exe get cache should have been run beforehand.

I think my computer took too long after I clicked restart button and nothing other than the message appeared, what I did was basically trying restart file repeatedly, and somehow after I run the “lake build” and few more trials of restarting, the lean4 started to work properly(my computer might be a bit slow)

[Ruize Chen]

Marc Huisinga said:

I tested it and it seems to work fine. I suspect that iz may have pressed the "Restart Server" button, not the "Restart File" button?

I was only actually clicking restart file button

[Mario Carneiro]

I don't think there is even a restart server button

[Mario Carneiro]

well, maybe in the lean menu

[Marc Huisinga]

Mario Carneiro said:

I don't think there is even a restart server button

There is, in the "Lake configuration changed" notification. It even covers the "Restart File" button :(

[Mario Carneiro]

I just noticed there is a new always-present restart file button in the infoview

[Marc Huisinga]

Yes, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/import.20must.20be.20rebuilt/near/429907606

[Mario Carneiro]

what signals that a restart is necessary?

[Marc Huisinga]

At least in the next Lean 4 RC, these kinds of errors will show up under "Messages" in the whole file, so as long as you have the InfoView open, it will be visible

[Marc Huisinga]

But older Lean 4 versions don't do that, so I may need to re-add the notifications for compatibility with older Lean 4 versions (only for the older versions, though)

[Mario Carneiro]

ah, okay just tried it and I see we still have the wall of red message

[Ruize Chen]

I doubted that my computer might be too slow when loading, it took sometime to give the correct response. I found it working fine after going back from using the online editor gitpod for a while.

[Marc Huisinga]

iz said:

I doubted that my computer might be too slow when loading, it took sometime to give the correct response. I found it working fine after going back from using the online editor gitpod for a while.

By the way, the Lean language client startup should be much quicker in newer Lean versions.

[Mario Carneiro]

Marc Huisinga said:

At least in the next Lean 4 RC, these kinds of errors will show up under "Messages" in the whole file, so as long as you have the InfoView open, it will be visible

I actually don't get the message immediately. I see a massive red gutter and an error highlight on the first line, and a closed "All Messages (1)" in the infoview and "No info found." for the main view. I expect this a side effect of the mechanism to avoid too-long error highlights, the message is not actually shown unless the cursor is on the first line or you have all messages open

[Mario Carneiro]

I'm not testing this on the latest lean though, only the latest version of the extension

[Mario Carneiro]

maybe that's what you were saying about backcompat

[Marc Huisinga]

Mario Carneiro said:

ah, okay just tried it and I see we still have the wall of red message

By the way, the language server stops processing the file when this kind of import error is returned, so "error for the whole file" like all other header errors is the right severity here.

[Mario Carneiro]

I think "error" is the wrong severity, because it's not a problem in the user's code

[Mario Carneiro]

it's also confusing for red files to show up in the explorer view just because something was open but not checked

[Mario Carneiro]

e.g. if I make a change in file A and files B and C depend on it, and file B is open in another tab, I will see only B turn red in the explorer

[Mario Carneiro]

I would opt for something like no highlights in the code at all (and no messages), and a big banner over the infoview saying that the checker is not running and you should use the big green "Start" button to start it

[Mario Carneiro]

possibly also a gutter indication of some kind for those who don't use the infoview or don't have it open. But gray not red

[Marc Huisinga]

Mario Carneiro said:

I think "error" is the wrong severity, because it's not a problem in the user's code

There is no other severity that communicates an issue that cannot be recovered from until further action is taken but wasn't caused by "user code". "Information", "hint" and "warning" all do not accurately signal that the language server will literally not process the file.

Mario Carneiro said:

it's also confusing for red files to show up in the explorer view just because something was open but not checked

I don't understand what "open but not checked" means.

Mario Carneiro said:

e.g. if I make a change in file A and files B and C depend on it, and file B is open in another tab, I will see only B turn red in the explorer

If B is open in another tab, it will not turn red at all. This only happens when you first open the file. lean4#393 (in the next RC) will instead issue an "info" diagnostic because the language server can keep processing the file in this case.

Mario Carneiro said:

I would opt for something like no highlights in the code at all (and no messages), and a big banner over the infoview saying that the checker is not running and you should use the big green "Start" button to start it

Programming users sometimes use Lean 4 without the InfoView (instead using the problems pane in VS Code), so these errors also need to show up somewhere else.

[Mario Carneiro]

making it show up on hovers is also a possibility, although it sounds a bit obnoxious

[Marc Huisinga]

To be clear, we are limited by LSP here in terms of the diagnostic severities we have available

[Mario Carneiro]

I don't think this should be an LSP "diagnostic" at all

[Mario Carneiro]

we have nothing to say about the user's code

[Mario Carneiro]

we have something to say about the system state

[Mario Carneiro]

it should be indicated by an icon in the status bar, a banner in the infoview, a gutter indicator, something like that. Not messages, which are for problems in the code

[Mario Carneiro]

it would be good to see how other LSP extensions handle this kind of thing. Most of the cases I can think of are done via status indicators or notifications

[Mario Carneiro]

and as you say, I don't think LSP directly helps here

[Marc Huisinga]

Mario Carneiro said:

it would be good to see how other LSP extensions handle this kind of thing. Most of the cases I can think of are done via status indicators or notifications

Status indicators are way too hidden, notifications are way too noisy. I think that of the tools that VS Code gives us, diagnostics are the best fit, even if they are not optimal by nature of also highlighting a part of the code (though I don't think highlighting a part of the header is really all that confusing, since to me it communicates that there's probably something wrong with the context of the file).

One thing also worth pointing out is that we added the fullRange field to diagnostics long ago to make diagnostics better fit this kind of use-case, but it was unfortunately disabled shortly afterwards by accident and I've only re-enabled it again very recently.

[Mario Carneiro]

Status indicators are way too hidden

My experience with the rust-analyzer status indicator is that it's quite noticeable, but it does this by being full red highlight over the text in the status bar. It is used when reading Cargo.toml fails for example

[Mario Carneiro]

though I don't think highlighting a part of the header is really all that confusing

It is very confusing that it highlights only the first import. It gives the impression that the error is with that import

[Mario Carneiro]

it's also usually very far from the part of the file I'm looking at at the moment

[Marc Huisinga]

Mario Carneiro said:

though I don't think highlighting a part of the header is really all that confusing

It is very confusing that it highlights only the first import. It gives the impression that the error is with that import

I agree, we could probably improve this.

Mario Carneiro said:

it's also usually very far from the part of the file I'm looking at at the moment

That's why it always shows up under "Messages" now on the next RC :-)

[Mario Carneiro]

and there is no point in drawing my attention to the beginning of the file to fix something over there and take me away from the current context

[Mario Carneiro]

To me "wall of red" very strongly suggests "you fool, you've broken everything" which is hard for newcomers to deal with

[Kevin Buzzard]

Would this all become far less relevant if instead of the instructions in my README telling people to clone the repo and then type some gobble-de-gook about cache get, we could just tell people to "install" the repo via some VS Code interface, which does (a) cloning (the part which everyone seems to be able to do) (b) getting cache (a part which trips people up) (c) opening the right folder (another part which trips people up)? Or is this somehow not possible?

[Marc Huisinga]

Kevin Buzzard said:

Would this all become far less relevant if instead of the instructions in my README telling people to clone the repo and then type some gobble-de-gook about cache get, we could just tell people to "install" the repo via some VS Code interface, which does (a) cloning (the part which everyone seems to be able to do) (b) getting cache (a part which trips people up) (c) opening the right folder (another part which trips people up)? Or is this somehow not possible?

The VS Code extension should already do this with the "Download Project" command, let me check.

[Marc Huisinga]

Yes, it works just fine with the formalizing mathematics repository.

[Marc Huisinga]

(Forall menu > Open project > Download project)

[Kevin Buzzard]

I should change the README then!

[Damiano Testa]

Kevin, feel free to use the test here.

[Marc Huisinga]

Damiano Testa said:

Kevin, feel free to use the test here.

To be clear, you shouldn't need to:

• Manually navigate to the folder you want to open. At the end, the extension will show a popup that asks you whether you want to re-open VS Code in that folder.
• Manually download the cache. The VS Code extension tries to call lake exe get cache when it makes sense in case we are in a Mathlib context. All the project-level commands in the VS Code extension (Creating projects, downloading projects, building projects, cleaning projects, updating a dependency) try to call lake exe get cache at a point where it makes sense.

[Damiano Testa]

---

Installing mathlib4

1. Open VSCode, open the lean4 extension and click on the ∀ symbol at the top-right.

2. Choose Open project ... --> Project: Download project ...
   This should automatically suggests mathlib4, so just type Enter.

3. Choose a folder where you want to download mathlib4.
   Wait for the download -- this may take a while, since mathlib4 and its cache occupy ~5GB.

4. You are good to go!

This should produce a project with a working cache.

If, at some point, you want to download the remote cache (assuming that it is available, since you pushed your project and CI built it for you), then in the ∀ menu, you can find Project Actions... --> Project: Fetch Mathlib build cache that will save you from having to compile locally mathlib4 (a process that can take somewhere in the region of 1 hour to complete).

---

[Damiano Testa]

I removed one of the steps: does this look alright now?

[Marc Huisinga]

You don't need to run Fetch Mathlib Build Cache directly after Download Project because the latter will already do that for you.

[Damiano Testa]

I added a clarification: I think that mentioning that you can download the cache (later on) is useful advice!

[Marc Huisinga]

Yes, if you are working with Git, then you may still need to run the command occasionally :-)

[Filippo A. E. Nuccio]

(deleted)