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)

[Yaël Dillies]

One year later, I am back at trying to use lean on Windows, and it's still not great :frown: This time, the dialog inside vscode fails to install elan. I do not think it's a PATH issue, since I simply cannot find the elan files anywhere (to be sure, where should they be?)

[Marc Huisinga]

What's the error message?

[Yaël Dillies]

When I open my mathlib clone, the following popup appears:
image.png

[Yaël Dillies]

If I press it, it goes to:
image.png

[Yaël Dillies]

If I press "Install Lean Versions Automatically", it gets me back to the first popup. If I do the same process a second time, no popup appears but instead I get the following vscode notification:
image.png

[Marc Huisinga]

Oh, that's not good.

Some more things to check:

• Does lean --version from a command line prompt work?
• What is the output of the 'Show Troubleshooting Output' command in the VS Code session where you attempted to install Elan?
• Is there a .elan folder in your home directory? (at C:\Users\<user>)

[Yaël Dillies]

$ lean --version
bash: lean: command not found

[Marc Huisinga]

Yaël Dillies said:

$ lean --version
bash: lean: command not found

A Windows command prompt :-)

[Yaël Dillies]

Ah sorry!

C:\Users\Yael>lean --version
'lean' n’est pas reconnu en tant que commande interne
ou externe, un programme exécutable ou un fichier de commandes.

[Yaël Dillies]

The output is

d:\Users\Yael\Documents\Lean\mathlib4> curl --version
curl 8.16.0 (Windows) libcurl/8.16.0 Schannel zlib/1.3.1 WinIDN
Release-Date: 2025-09-10
Protocols: dict file ftp ftps gopher gophers http https imap imaps ipfs ipns ldap ldaps mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss
Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

d:\Users\Yael\Documents\Lean\mathlib4> git --version
git version 2.51.2.windows.1

d:\Users\Yael\Documents\Lean\mathlib4> lean --version
=> Operation failed. Exit code: -4058.
> Invoke-WebRequest -Uri "https://elan.lean-lang.org/elan-init.ps1" -OutFile "elan-init.ps1"
Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
$rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable
del .\elan-init.ps1
exit $rc
Invoke-WebRequest : L'acc�s au chemin d'acc�s 'C:\Program Files\Microsoft VS Code\elan-init.ps1' est refus�.
Au caract�re Ligne:1 : 1
+ Invoke-WebRequest -Uri "https://elan.lean-lang.org/elan-init.ps1" -Ou ...
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : NotSpecified: (:) [Invoke-WebRequest], UnauthorizedAccessException
    + FullyQualifiedErrorId : System.UnauthorizedAccessException,Microsoft.PowerShell.Commands.InvokeWebRequestCommand
.\elan-init.ps1 : Le terme �.\elan-init.ps1� n'est pas reconnu comme nom d'applet de commande, fonction, fichier de
script ou programme ex�cutable. V�rifiez l'orthographe du nom, ou si un chemin d'acc�s existe, v�rifiez que le chemin
d'acc�s est correct et r�essayez.
Au caract�re Ligne:3 : 7
+ $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4: ...
+       ~~~~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (.\elan-init.ps1:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException
del : Impossible de trouver le chemin d'acc�s �C:\Program Files\Microsoft VS Code\elan-init.ps1�, car il n'existe pas.
Au caract�re Ligne:4 : 1
+ del .\elan-init.ps1
+ ~~~~~~~~~~~~~~~~~~~
    + CategoryInfo          : ObjectNotFound: (C:\Program File...e\elan-init.ps1:String) [Remove-Item], ItemNotFoundEx
   ception
    + FullyQualifiedErrorId : PathNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand
d:\Users\Yael\Documents\Lean\mathlib4> elan --version
=> Operation failed. Exit code: -4058.
d:\Users\Yael\Documents\Lean\mathlib4> lean --version
=> Operation failed. Exit code: -4058.

[Yaël Dillies]

There is no .elan folder in my home directory

[Marc Huisinga]

OK, so there is a clear bug in the extension here where the installation failed and it wasn't being correctly reported by the extension.

[Marc Huisinga]

I assume you don't have write access to C:\ where VS Code is installed and the extension is attempting to download the Elan installation script to? That's likely the reason for the failed install then and also something we should fix.

[Yaël Dillies]

I am admin of this machine. I didn't start vscode with admin rights though. Let me try

[Marc Huisinga]

You probably want to make sure that it installs Elan for your regular user account, so not sure if running it as an administrator will help.

Can you confirm that you can't write (e.g. create new files) at C:\Program Files\Microsoft VS Code\ with your regular user account?

[Eric Taucher]

Noticed the directory d: instead of c: for the Documents directory, e.g. d:\Users\Yael\Documents\Lean\mathlib4>. Is that of importance? As I don't know the details of how all of Lean is installed and maintained on Windows, noting in case it was missed. :slight_smile:

[Yaël Dillies]

What might be confusing the extension here is that I have two mounts C:\ and D:\, the first one meant for Windows and the second one meant for data (and it's shared with the Ubuntu dual boot)

[Marc Huisinga]

I'd still be curious if you can create files in the directory I mentioned.

Also: how did you install VS Code?

[Marc Huisinga]

(I'm asking because it usually installs it to C:\Users\<user>\AppData\Local\Programs\Microsoft VS Code), not C:\Program Files\Microsoft VS Code\)

[Yaël Dillies]

.msi from the official website

[Yaël Dillies]

Marc Huisinga said:

I'd still be curious if you can create files in the directory I mentioned.

Indeed I cannot

[Marc Huisinga]

Yaël Dillies said:

Marc Huisinga said:

I'd still be curious if you can create files in the directory I mentioned.

Indeed I cannot

Then my next question would be whether you installed VS Code itself as an administrator (which IIRC the installer even warns about?), because the installer will probably have a hard time writing to that location as well otherwise :-)

[Yaël Dillies]

Oh :idea: Yes, I did

[Marc Huisinga]

Generally, I'd recommend to see whether you can install VS Code to your home directory, because I'm not sure that this won't cause any other problems.
If you can't for whatever reason, you can try the manual installation steps from a command prompt in your home directory where you have write permissions (Git and Curl are already installed, so you can skip that).

I'll still see if I can fix that installing Elan won't work in this configuration and that it correctly reports errors.

[Marc Huisinga]

vscode-lean4#689