Warning in project version

Stream: general

[Filippo A. E. Nuccio]

I have updated my LocalClassFieldTheory project and now I see

Opened project is using a Lean 4 version (4.0.0-nightly-2023-02-04) from before the first Lean 4 stable release (4.0.0).
Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.

I would certainly want to update to a new Lean 4 version, but my toolchain says

leanprover/lean4:v4.8.0-rc2

so I am not sure what I am supposed to do.

[Filippo A. E. Nuccio]

Also, since updating to 4..8.0-rc2 my lean server crashes very often, without noticeable trouble (I simply relaunch it) but it seems a bad sign...

[Patrick Massot]

Are there any error messages when it crashes?

[Filippo A. E. Nuccio]

Yes, let me reopen it and copy-paste

[Filippo A. E. Nuccio]

OK, now I have launched it and can work well... Let's wait 3 mins

[Filippo A. E. Nuccio]

(as usual, you're never as fit as when you enter the doctor's room... :fever: )

[Filippo A. E. Nuccio]

OK, now I got the

Opened project is using a Lean 4 version (4.0.0-nightly-2023-02-04) from before the first Lean 4 stable release (4.0.0). Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.

[Filippo A. E. Nuccio]

But no crash "yet"

[Marc Huisinga]

Filippo A. E. Nuccio said:

OK, now I got the

Opened project is using a Lean 4 version (4.0.0-nightly-2023-02-04) from before the first Lean 4 stable release (4.0.0). Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.

What's the setup information output in the file you are looking at? (Forall menu > Show setup information)

[Filippo A. E. Nuccio]

Operating system: Windows_NT (release: 10.0.22631)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1185G7 @ 3.00GHz
Available RAM: 34.19 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.8.0-rc2)
Project: Valid Lean project (path: c:\Users\nf51454h\Desktop\Lean\LocalClassFieldTheory)

---

Elan toolchains:

installed toolchains
--------------------

stable
leanprover/lean4:nightly-2023-02-04 (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------


leanprover/lean4:v4.8.0-rc2 (overridden by '\\?\C:\Users\nf51454h\Desktop\Lean\LocalClassFieldTheory\lean-toolchain')

Lean (version 4.8.0-rc2, x86_64-w64-windows-gnu, commit 873ef2d894af, Release)

[Filippo A. E. Nuccio]

Yes, now it goes:

Lean Server has stopped unexpectedly

[Filippo A. E. Nuccio]

The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

[Filippo A. E. Nuccio]

And if I look at the output

[Filippo A. E. Nuccio]

Watchdog error: cannot find open document 'file:///c%3A/Users/nf51454h/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/src/lean/Lean/Elab/Declaration.lean'

[Error - 2:39:22 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

[Filippo A. E. Nuccio]

(Beside the trouble per se the fact that it crashes after 9 minutes is beyond my paygrade. I thought the idea of getting tired while jogging was a human feature...)

[Marc Huisinga]

Did you open that file at some point (e.g. by using go-to-definition)?

[Filippo A. E. Nuccio]

I opened another file (inside Mathlib) but almost immediately, certainly not after 9 minutes.

[Marc Huisinga]

One thing you can try is to set elan default leanprover/lean4:v4.8.0-rc2

[Filippo A. E. Nuccio]

Let me try; and the probably close-reopen VSCode?

[Marc Huisinga]

Yes

[Filippo A. E. Nuccio]

OK, done. Now I fear I have to wait 9 more minutes for the next crash... :hourglass_done:

[Marc Huisinga]

Unfortunately, when opening core files, Lean uses the default toolchain because the core source files don't have a lean-toolchain file themselves (cc @Sebastian Ullrich). This means that go to definition into core can break things.

[Filippo A. E. Nuccio]

But I went to a declaration in Mathlib.DedekindDomain.Ideal...

[Filippo A. E. Nuccio]

OK, I still get the warning

Opened project is using a Lean 4 version (4.0.0-nightly-2023-02-04) from before the first Lean 4 stable release (4.0.0).
Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.

[Filippo A. E. Nuccio]

and beyond having a (seemingly) updated toolchain I do not know what to do

[Marc Huisinga]

Does elan show now designate the correct toolchain as default?

[Filippo A. E. Nuccio]

Ah no

[Filippo A. E. Nuccio]

It still gives the old one

[Filippo A. E. Nuccio]

Yes, now it is ok

[Filippo A. E. Nuccio]

$ elan show
installed toolchains

---

stable
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:v4.8.0-rc2 (default)

active toolchain

---

leanprover/lean4:v4.8.0-rc2 (overridden by '\\?\C:\Users\nf51454h\Desktop\Lean\LocalClassFieldTheory\lean-toolchain')
Lean (version 4.8.0-rc2, x86_64-w64-windows-gnu, commit 873ef2d894af, Release)

[Filippo A. E. Nuccio]

Let's try again with the project

[Filippo A. E. Nuccio]

OK, while it launches: I would be very happy to uninstall the old one, but I have the feeling that each time I will create a new project I would re-install it due to the instructions here. Am I wrong?

[Marc Huisinga]

The instructions at that documentation page now seem to refer to a more recent nightly

[Filippo A. E. Nuccio]

Oh, you're right.

[Filippo A. E. Nuccio]

OK, so I will happily uninstall that old toolchain.

[Filippo A. E. Nuccio]

OK, now I am not getting the warning any more, let's see if it crashed in a while.

[Filippo A. E. Nuccio]

Yep, crashed again!

Watchdog error: cannot find open document 'file:///c%3A/Users/nf51454h/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/src/lean/Lean/Elab/Declaration.lean'

[Error - 2:54:03 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

[Filippo A. E. Nuccio]

And again, I was just fighting with a rw inside my file and had the Mathlib.DedekindDomain.Ideal open, where the declaration I was fighting against is.

[Filippo A. E. Nuccio]

And once more, if I simply ignore this "crash" I can keep working.

[Marc Huisinga]

Ah, I have an idea for one more thing to narrow down the source of this issue. Could you try downgrading your Lean 4 extension version to 0.0.155? (Extensions > Right click on Lean 4 extension > Install another version)

[Filippo A. E. Nuccio]

Sure, let me try.

[Filippo A. E. Nuccio]

OK, done and restarted; I have also disabled the auto-update

[Marc Huisinga]

(VS Code sometimes opens ghost documents in the background for various features. I had to touch our logic for filtering these documents in fixing https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/VSCODE.20outline.20mode.20not.20working.20in.20imports/near/442000461, so there's a chance that I overlooked something)

[Filippo A. E. Nuccio]

Well, we're ready for another trial. I will keep fighting my rw and if in 5/7 minutes nothing happens is seems like a good sign.

[Filippo A. E. Nuccio]

... still good :silence:

[Filippo A. E. Nuccio]

I am inclined to believe that you found the problem! :tada:

[Marc Huisinga]

Well, it's still not really clear what the cause is and unfortunately I can't reproduce it myself. I have a suspicion though, so let's see if I can fix this regardless without a reproducer.

[Filippo A. E. Nuccio]

Of course if you need/want to discuss by zoom to see/play with my PC, that's fine.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Marc Huisinga]

I made an attempt at fixing this and the attempted fix is in a pre-release version (0.0.158) of the VS Code extension. You can install it by selecting the extension and then clicking "Switch to pre-release" in the page that opens.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Filippo A. E. Nuccio]

OK, let me check.

[Filippo A. E. Nuccio]

I still do not have it

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Marc Huisinga]

If the issue you encountered didn't come up with 0.0.158 anymore, I'll release it tomorrow.

[Filippo A. E. Nuccio]

Well, as a matter of fact I have not been able to download 0.0.158, I still only have 0.0.157 in the top of my list and no "pre-release" button in the extension page.... :sad:

[Marc Huisinga]

Filippo A. E. Nuccio said:

Well, as a matter of fact I have not been able to download 0.0.158, I still only have 0.0.157 in the top of my list and no "pre-release" button in the extension page.... :sad:

This is what it looks like for me:
image.png

[Marc Huisinga]

Perhaps you need to update to 0.0.157 first for the button to show up?

[Filippo A. E. Nuccio]

Let me try

[Filippo A. E. Nuccio]

Yes indeed, good point.

[Filippo A. E. Nuccio]

I have just installed 0.0.158 then, I will work on it half an hour, say, and will report back if I have problems.

[Filippo A. E. Nuccio]

Well, for the time being everything still OK. I will soon need to leave, but I have not seen any problem as those before. Thanks!