reliable file desync on Linux Mint

Stream: lean4

[Floris van Doorn]

I have a student that is using Lean on Linux Mint 20, and they have an issue when typing in a Lean file (Lean version 4.13.0-rc3).
When they type very slowly, 1 character at a time, everything is fine. When they type more quickly, then it seems that there is a desync between the local file and the state that the language server thinks the file is. One of the two following things happens (almost reliably):

• The file doesn't update, no matter what is typed, until a file restart
• Yellow bars appear and remain there indefinitely, until a file restart

Any suggestions/things to try/more information we can provide?

[Floris van Doorn]

(I asked them to post their setup information here, but they're having internet trouble at the moment)

[Sebastian Ullrich]

Could you have them try this? https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Yellow.20bar.20doesn't.20go.20away/near/428287485

[Raphael Gaedtke]

Floris van Doorn schrieb:

(I asked them to post their setup information here, but they're having internet trouble at the moment)

This are my setup information:

Operating system: Linux (release: 5.4.0-196-generic)
CPU architecture: x64
CPU model: 4 x Intel(R) Core(TM) i3-6006U CPU @ 2.00GHz
Available RAM: 8.24 GB

VS Code version: Reasonably up-to-date (version: 1.79.2)
Lean 4 extension version: 0.0.178
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.13.0-rc3)
Project: Valid Lean project (path: /home/raphael/Dokumente/Uni/Lean/leanCourse24)

---

Elan toolchains:

installed toolchains


--------------------




stable (default)

leanprover/lean4:v4.12.0
leanprover/lean4:v4.12.0-rc1
leanprover/lean4:v4.13.0-rc3



active toolchain


----------------


leanprover/lean4:v4.13.0-rc3 (overridden by '/home/raphael/Dokumente/Uni/Lean/leanCourse24/lean-toolchain')

Lean (version 4.13.0-rc3, x86_64-unknown-linux-gnu, commit 01d414ac36dc, Release)

[Raphael Gaedtke]

Sebastian Ullrich schrieb:

Could you have them try this? https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Yellow.20bar.20doesn't.20go.20away/near/428287485

Using killall lean unfortunately did not solve the problem. Running the recommended pidof command while seeing the yellow bars resulted in the following output:
output
I noticed that the processing usually is done after waiting for way more than ten minutes.

[Sebastian Ullrich]

Thanks, this is very helpful!

[Kunhong Du]

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

[Floris van Doorn]

Kunhong Du said:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

If you want to downgrade, you can edit your lakefile.lean and replace

require mathlib from git "https://github.com/leanprover-community/mathlib4"

by

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "<desired-commit>"

where <desired-commit> is the (Mathlib4) commit you want to go to. Then run lake update which will get the correct version of Lean/mathlib + dependencies.

[Raphael Gaedtke]

Kunhong Du schrieb:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

Going back to an older version actually solved the problem. I've tried that earlier and was unsuccessful back then. I think the difference is that I used killall lean this time.

[Kunhong Du]

Floris van Doorn said:

Kunhong Du said:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

If you want to downgrade, you can edit your lakefile.lean and replace

require mathlib from git "https://github.com/leanprover-community/mathlib4"

by

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "<desired-commit>"

where <desired-commit> is the (Mathlib4) commit you want to go to. Then run lake update which will get the correct version of Lean/mathlib + dependencies.

I used the commit code from Documentation but I received this error

$ lake update
info: mathlib: URL has changed; you might need to delete '.\.\.lake\packages\mathlib' manually
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
trace: stderr:
From https://github.com/leanprover-community/mathlib4
 * [new branch]            AffineLocalToPretop -> origin/AffineLocalToPretop
   f9511f900b..01081c6173  split-GroupTheory.Congruence.Basic -> origin/split-GroupTheory.Congruence.Basic
info: mathlib: updating repository '.\.\.lake\packages\mathlib' to revision '01d414ac36dc28f3e424dabd36d818873fea655c'
trace: .\.\.lake\packages\mathlib> git checkout --detach 01d414ac36dc28f3e424dabd36d818873fea655c --
trace: stderr:
fatal: reference is not a tree: 01d414ac36dc28f3e424dabd36d818873fea655c
error: external command 'git' exited with code 128

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/commit/01d414ac36dc28f3e424dabd36d818873fea655c indeed doesn't exist

[Kunhong Du]

Eric Wieser said:

https://github.com/leanprover-community/mathlib4/commit/01d414ac36dc28f3e424dabd36d818873fea655c indeed doesn't exist

Oh my fault, that's lean4 commit not mathlib4 commit. :joy:

[Kunhong Du]

Raphael Gaedtke said:

Kunhong Du schrieb:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

Going back to an older version actually solved the problem. I've tried that earlier and was unsuccessful back then. I think the difference is that I used killall lean this time.

Which version did you go back to?

I rollbacked to some mathlib4 commit created 1 week ago and the problem persists. It's still 4.13.0-rc3, so I guess I should go back to maybe rc2 or rc1?

Or is there an equivalent of killall for Windows I can try?

[Kunhong Du]

Update: the equivalent command for Windows seems to be taskkill /F /IM lean.exe, but unluckily it still doesn't work. Trying to go back to rc1 now.

[Raphael Gaedtke]

Kunhong Du schrieb:

Raphael Gaedtke said:

Kunhong Du schrieb:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

Going back to an older version actually solved the problem. I've tried that earlier and was unsuccessful back then. I think the difference is that I used killall lean this time.

Which version did you go back to?

I rollbacked to some mathlib4 commit created 1 week ago and the problem persists. It's still 4.13.0-rc3, so I guess I should go back to maybe rc2 or rc1?

Or is there an equivalent of killall for Windows I can try?

I wanted to go back to the end of August and randomly selected https://github.com/leanprover-community/mathlib4/commit/b03feaaa7875f105350ba8765a8ef4fba3b93cb2.

[Kunhong Du]

Raphael Gaedtke said:

Kunhong Du schrieb:

Raphael Gaedtke said:

Kunhong Du schrieb:

I'm having the exactly same problem on Windows aftering updating to  4.13.0-rc3. I guess the killall is a Linux command which doesn't work for Windows. Is going back to an older version a possible solution? If so, how can I do that?

Going back to an older version actually solved the problem. I've tried that earlier and was unsuccessful back then. I think the difference is that I used killall lean this time.

Which version did you go back to?

I rollbacked to some mathlib4 commit created 1 week ago and the problem persists. It's still 4.13.0-rc3, so I guess I should go back to maybe rc2 or rc1?

Or is there an equivalent of killall for Windows I can try?

I wanted to go back to the end of August and randomly selected https://github.com/leanprover-community/mathlib4/commit/b03feaaa7875f105350ba8765a8ef4fba3b93cb2.

Ah, just went back to late September and the problem is solved. So I guess it is really some bug in rc3? :upside_down:

[Sebastian Ullrich]

Thanks again for all the information, this should be fixed with lean#5736

[Floris van Doorn]

Are lean#5736 and lean#5752 considered for a new release candidate?
Multiple of my students are experiencing this issue (I made the mistake of relying on a release candidate with my Lean course).

[Kim Morrison]

v4.13.0-rc4 is coming out shortly, with these.