Lean crashes computer

Stream: new members

[Sayantan Majumdar]

I recently tried running the mathematics_in_lean tutorials. I cloned the repo and tried lake --verbose exe cache get and then lake --verbose build and then started vscode with lean4 extension. The thing stops working and the orange lines appear with the loading message state. I tried to rebuild multiple times and even deleted the .lake folder and rebuilt the project.

Is Lean still so unreliable? What should be done when it gets stuck?

NOTE: both mathlib4 and the project are using the same toolchain leanprover/lean4:v4.6.0-rc1

[Sayantan Majumdar]

what do you guys do when lean4 is stuck? i am running the mathematics_in_lean and it is stuck in the orange lines in lean4

[Sayantan Majumdar]

I am trying to run the mathematics_in_lean tutorials and I first cloned the repo and the tried lake --verbose exe cache get and then lake --verbose build and then opened the folder with vscode and lean4 extension.

It ran properly for a few minutes and then it for stuck at the orange lines and meassege loading state. I rebuild the package and also tried to delete the .lake folder and rebuild the package. I worked for some time but it is again stuck.

what do you do in this situation?

[Kim Morrison]

Can you show us a screenshot? Your qestion is unclear.

[Sayantan Majumdar]

I am trying to run the mathematics_in_lean tutorials and I first cloned the repo and the tried lake --verbose exe cache get and then lake --verbose build and then opened the folder with vscode and lean4 extension.

It ran properly for a few minutes and then it got stuck at the orange lines and message loading state. I rebuilt the package and also tried to delete the .lake folder and rebuild the package. I worked for some time but it is again stuck.

What should I do?

[Sayantan Majumdar]

I am trying to run the mathematics_in_lean tutorials and I first cloned the repo and the tried lake --verbose exe cache get and then lake --verbose build and then opened the folder with vscode and lean4 extension.

It ran properly for a few minutes and then it got stuck at the orange lines and message loading state. I rebuilt the package and also tried to delete the .lake folder and rebuild the package. I worked for some time but it is again stuck.

both the MIL and mathlib4 are using the same lean-toolchain leanprover/lean4:v4.6.0-rc1

[Frédéric Dupuis]

You've posted the same question in four streams by now. Please don't do this.

[Sayantan Majumdar]

which lean-toolchain are you using? I am not sure but I have rebuilt my library many times and suddenly it will start working fast! and then get very slow

[Notification Bot]

Kim Morrison has marked this topic as unresolved.

[Notification Bot]

A message was moved here from #lean4 > ✔ Lean running very slowly by Kim Morrison.

[Notification Bot]

A message was moved here from #lean4 > Lean is stuck! by Kim Morrison.

[Notification Bot]

A message was moved here from #general > What to do when Lean is stuck? by Kim Morrison.

[Notification Bot]

4 messages were moved here from #mathlib4 > lean4 is stuck by Kim Morrison.

[Sayantan Majumdar]

Frédéric Dupuis said:

You've posted the same question in four streams by now. Please don't do this.

sorry, was was building the library while posting and everything crashed. did not realise all the other messages were actually posted.

[Sayantan Majumdar]

Kim Morrison said:

Can you show us a screenshot? Your qestion is unclear.

Here is a screenshot.
Screenshot-from-2024-04-22-17-12-13.png

[Rémy Degenne]

If you click on the first line (the first import line with a blue squiggle), what do you see on the right?

[Sayantan Majumdar]

Rémy Degenne said:

If you click on the first line (the first import line with a blue squiggle), what do you see on the right?

"busily processing..." and in the next line "Loading..."

[Sayantan Majumdar]

I thought I already built the library before opening vscode and did not change any file yet

[Sayantan Majumdar]

I will clean or delete the .lake folder and try building again. Or shift to Coq

[Rémy Degenne]

I don't know what is happening then. I expected something like "building X", which would mean that the dependencies were not fully built, but that's apparently not the issue here.
One other thing that happened to me once is that there was a lock file that prevented the build and it got stuck like that, but I don't remember where that lock file was located or whether that is an issue that still happens with newer versions.