Improving the Windows user experience

Stream: lean4

[Yaël Dillies]

Could we try polishin the Windows experience of using Lean a bit? For once, I am trying to use Lean on Windows and it's roadblock after roadblock.

[Yaël Dillies]

I want to do a simple task: bump PFR (https://github.com/teorth/pfr). So I update lean-toolchain and run

Yael@DESKTOP-38SA6QH MINGW64 ~/Documents/Lean/pfr (master)
$ lake -R -Kenv=dev update
error: permission denied (error code: 13)
  file: .· error: permission denied (error code: 13)
  file: .· error: permission denied (error code: 13)
  file: .\.\.lake\lakefile.olean

[Yaël Dillies]

Okay great. I guess to run

Yael@DESKTOP-38SA6QH MINGW64 ~/Documents/Lean/pfr (master)
$ rm -rf .lake
rm: cannot remove '.lake/packages/mathlib/.lake/build/lib/Mathlib/Analysis/Fourier/ZMod.ilean': Device or resource busy
rm: cannot remove '.lake/packages/mathlib/.lake/build/lib/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.ilean': Device or resource busy
rm: cannot remove '.lake/packages/mathlib/.lake/build/lib/Mathlib/Analysis/InnerProductSpace/ProdL2.ilean': Device or resource busy
# etc

[Rémy Degenne]

Yes, that's annoying: you have to close VSCode before getting the cache or doing an update from the command line.

[Yaël Dillies]

Ah but now I can run

Yael@DESKTOP-38SA6QH MINGW64 ~/Documents/Lean/pfr (master)
$ lake -R -Kenv=dev update
trace: .\.\.lake\packages\LeanAPAP> git fetch --tags --force origin
trace: .\.\.lake\packages\doc-gen4> git fetch --tags --force origin
info: mathlib: URL has changed; you might need to delete '.\.\.lake\packages\mathlib' manually
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
info: mathlib: updating repository '.\.\.lake\packages\mathlib' to revision 'd27f22898a74975360dd1387155c6031b501a90b'
trace: .\.\.lake\packages\mathlib> git checkout --detach d27f22898a74975360dd1387155c6031b501a90b --
trace: stderr:
fatal: reference is not a tree: d27f22898a74975360dd1387155c6031b501a90b
error: external command 'git' exited with code 128

[Yaël Dillies]

... and Lean has successfully ruined my mood

[Yaël Dillies]

Rémy Degenne said:

Yes, that's annoying: you have to close VSCode before getting the cache or doing an update from the command line.

I understand the solution, but can we come up with something better?

[Marc Huisinga]

For the "Device or resource busy" errors, can you use the VS Code extension command to update LeanAPAP? It shuts down the language server before performing the update and restarts it afterwards.

I tried doing so quickly on a Windows machine and the update of LeanAPAP in pfr goes through without errors.
I do see the following error when opening VS Code on Linux as well:

/home/mhuisi/LeanProjects/PFR> lake --version
Lake version 5.0.0-01d414a (Lean version 4.13.0-rc3)
info: LeanAPAP: updating repository '././.lake/packages/LeanAPAP' to revision 'ece13c901dde033807bd3c72c40c9ae48f060f7b'
error: external command 'git' exited with code 128
warning: package configuration has errors, falling back to plain `lean --server`

Not sure what it's caused by.

BTW, I'm not sure if -R -Kenv=dev is still necessary?

[Marc Huisinga]

Rémy Degenne said:

Yes, that's annoying: you have to close VSCode before getting the cache or doing an update from the command line.

You shouldn't have to do that if you use the VS Code commands for getting the cache or performing updates, since they try to ensure that the language server is shut down when running these commands.

[Yaël Dillies]

Marc Huisinga said:

For the "Device or resource busy" errors, can you use the VS Code extension command to update LeanAPAP? It shuts down the language server before performing the update and restarts it afterwards.

Is it Lean 4: Project: Update dependency? I did not know about this :idea:

[Marc Huisinga]

Yaël Dillies said:

Marc Huisinga said:

For the "Device or resource busy" errors, can you use the VS Code extension command to update LeanAPAP? It shuts down the language server before performing the update and restarts it afterwards.

Is it Lean 4: Project: Update dependency? I did not know about this :idea:

Yes!

[Kim Morrison]

I'd really encourage projects to try to stop using -R -Kenv=dev if at all possible.

[Kim Morrison]

(I think a downstream project that has a standard require on doc-gen, and does the documentation generation, is the preferred alternative?)

[Rémy Degenne]

Marc Huisinga said:

Rémy Degenne said:

Yes, that's annoying: you have to close VSCode before getting the cache or doing an update from the command line.

You shouldn't have to do that if you use the VS Code commands for getting the cache or performing updates, since they try to ensure that the language server is shut down when running these commands.

Yes I know and I want to get used to those VSCode commands, but since I am often in a terminal for git related things I tend to type lake commands there as well.

[Rémy Degenne]

Kim Morrison said:

(I think a downstream project that has a standard require on doc-gen, and does the documentation generation, is the preferred alternative?)

That preferred alternative means setting up and updating two projects instead of one: that's quite cumbersome.

[Edward van de Meent]

Rémy Degenne said:

Yes, that's annoying: you have to close VSCode before getting the cache or doing an update from the command line.

actually, just stopping the server seems to be enough to get the cache...

[Edward van de Meent]

(for me)

[Edward van de Meent]

still, this is not the best behaviour

[Yaël Dillies]

Kim Morrison said:

(I think a downstream project that has a standard require on doc-gen, and does the documentation generation, is the preferred alternative?)

This is not my preferred alternative for the reason Rémy is pointing out.

[Sebastian Ullrich]

I haven't tried yet but a separate repo should not be necessary? It could be a separate directory with its own lakefile

[François G. Dorais]

Sebastian Ullrich said:

I haven't tried yet but a separate repo should not be necessary? It could be a separate directory with its own lakefile

I just tested it. It works great!

[François G. Dorais]

I created a directory in my repo containing this lakefile.toml:

name = "Docs"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "main"

[[require]]
name = <fill-in-your-library-name>
path = ".."

[[lean_lib]]
name = "Docs"

For the lean-toolchain I just symlinked ../lean-toolchain. And Docs.lean just imports my library.

[François G. Dorais]

Then lake build Docs:docs works perfectly.

[François G. Dorais]

Actually, path = ".." is dangerous since lake might try to delete that path! Better to require from your git repo.

[François G. Dorais]

Well, I think I just discovered a serious bug in lake! lean4#5876

[François G. Dorais]

@Mac Malone :up:

[Mac Malone]

@François G. Dorais Ah, yes. I had discovered this bug while working on lean4#5864. Since it had existed for a while and no one had reported an issue, I had hoped merging that would leave this danger unrealized. Apparently, no such luck. :cry: Regardless, thank you for reminding me of this, as the PR in question will not be part of the next release so I should separate this fix out. :thank_you:

[Mac Malone]

lean4#5878

[Kim Morrison]

@Mac Malone, let's backport that one?

[François G. Dorais]

@Mac Malone Thank you for the quick response! I'm just happy that one of my typos finally did something good! :smile:

[Mauricio Collares]

The fix mentions .. explicitly. Is it also possible to escape the source dir by using .../.... (EDIT: apparently I'm very old) or slashes/backslashes?

[Eric Wieser]

That .. is the lean .. not the posix ..

[Mauricio Collares]

Ah, makes sense, thanks

[Yaël Dillies]

@Marc Huisinga said:

For the "Device or resource busy" errors, can you use the VS Code extension command to update LeanAPAP? It shuts down the language server before performing the update and restarts it afterwards.

I just tried so and got
image.png

[Yaël Dillies]

I assume it's because .lake/lakefile.olean.lock exists

[Yaël Dillies]

rm .lake/lakefile.olean.lock indeed fixes it. Should the action do this automatically?

[Ruben Van de Velde]

The lock file exists to stop you changing the file while some other process is using it, so I don't think so

[Yaël Dillies]

@Bhavik Mehta and I wanted to try splitting files in the context of #mathlib4 > #18328 delay importing ultrafilters, so we updated my copy of mathlib, which made it go from 4.13.0-rc3 to 4.13.0 and then we tried getting cache

[Yaël Dillies]

We pushed the extension buttons for roughly 20 minutes before giving up

[Yaël Dillies]

I would consider the user experience of using Windows as "Pretty bad" :sad: Is this a shared diagnosis? Does @Marc Huisinga want to hop on a screenshare call to see exactly what goes wrong?

[Richard Copley]

Yaël Dillies said:

Bhavik Mehta and I wanted to try splitting files in the context of #mathlib4 > #18328 delay importing ultrafilters, so we updated my copy of mathlib, which made it go from 4.13.0-rc3 to 4.13.0 and then we tried getting cache

The branch for that PR is only a few days old, and the lean-toolchain file in the branch says leanprover/lean4:v4.13.0-rc3. What actually happened, in your opinion: where could 4.13.0 have come from?

We pushed the extension buttons for roughly 20 minutes before giving up

When you put it like that, it doesn't sound like a good idea!

I would consider the user experience of using Windows as "Pretty bad" :sad: Is this a shared diagnosis?

It's mostly fine for me.

Conceivably, lake or the vscode extension tried and failed to replace (for example) the lean-toolchain file, but didn't check the status of the operation (assuming that it could not fail, which might be a good assumption on Linux, but less so on Windows if a process might have had an open handle to the file), then signalled lake or lean to restart. If so, it's a small bug, and might even be easy to fix. These things happen. On behalf of my fellow programmers, I apologise for the inconvenience.

If you can find a recipe to reliably reproduce the condition, please describe it here (or as an issue on Github if you can deduce that there is a bug in a particular program).

Meanwhile as a general work-around for issues like this on Windows, close or kill all the processes concerned, then update the files they are using, then launch the application again.

[Yaël Dillies]

Richard Copley said:

The branch for that PR is only a few days old, and the lean-toolchain file in the branch says leanprover/lean4:v4.13.0-rc3. What actually happened, in your opinion: where could 4.13.0 have come from?

we were not on the branch we were on master

[Marc Huisinga]

Could you be more specific?

[Bhavik Mehta]

We were on mathlib master from a couple of days earlier, and decided to update. We did git pull (updating to 4.13.0), then fetched cache using the extension button. After this point, the file we were in (something like Data.Set.Finite) wouldn't build (it either said imports are out of date in red, or said it was building something in Aesop and was doing so really slowly), so we did a series of clean project, fetch cache, restart server and reload window in various orders. And after 20 minutes, the state of the file remained about the same, and we gave up.

[Marc Huisinga]

Was there an error in the troubleshooting output window while pulling the cache?

[Bhavik Mehta]

Not that I saw, but I don't think I checked. Nothing popped up, but that's not to say there was nothing there for some other reason.

[Shreyas Srinivas]

Data.Set.Finite.Basic (or was it Data.Finite.Basic?) disappeared. Is that the reason? We had an issue with that on equational_theories too, hence checking.

[Marc Huisinga]

I just tried the following steps on a Windows machine:

• Start on a clean slate with cache on b758def5262ecb106a626ec885176ed1ece2e4ba (commit that updated Mathlib to v4.13.0-rc3)
• Open VS Code in Data.Set.Finite
• Check out d5ab93e3a3afadaf265a583a92f7e7c47203b540 (commit that updated Mathlib to v4.13.0) from a terminal
• Run 'Fetch Mathlib Build Cache' command in VS Code and wait until it completes

At the end of the fetch cache operation, the server restarts automatically and the file works without errors. Do these concrete steps produce a different result for you?

[Marc Huisinga]

@Yaël Dillies @Bhavik Mehta

[Bhavik Mehta]

Will wait for Yaël on this, it was on their machine (I'm not on windows)