Lake on Windows

Stream: lean4

[Richard Copley]

On Windows, in a newly created project or after deleting ".lake", lake update works as expected. Subsequent runs of lake update print "error: no error (error code: 0)" and exit with error code 1.

[Mario Carneiro]

Do you have a MWE?

[Mario Carneiro]

something like this?

lake new foo
cd foo
lake update
lake update

?

[Richard Copley]

Yep, that should do it. I'll test

[Mario Carneiro]

what version of lean/lake are you using?

[Richard Copley]

Lean (version 4.3.0, commit 8e5cf6466061, Release)
Lake version 5.0.0-8e5cf64 (Lean version 4.3.0)

[Richard Copley]

Ah, I think I see. It seems that starting Lake as a language server in the project is also a necessary part of the recipe, so the solution is to stop the language server before updating.

[Richard Copley]

In earlier versions of Lake, lake update would run, but it was always a bad idea, since lake exe cache get would make a mess when it couldn't overwrite oleans open in Lean. This is actually an improvement, but maybe a slightly less amusing error message would be nice.

[Mac Malone]

Certainly! Identifying were the error: no error (error code: 0) is coming from is key. That seems like a serious bug somewhere (an error code of 0 should not be producing an error).

[Mario Carneiro]

I was not able to reproduce this on windows or linux

[Junyan Xu]

On my new Windows laptop (mostly using MacBook previously), I'm getting errors like

C:\Users\...\.cache\mathlib\52322cf9463d4500.ltar: The process cannot access the file because it is being used by another process. (os error 32)
...
uncaught exception: leantar failed with error code 1

when running lake exe cache get if the Lean server is also running in the same directory (e.g. Lake is building dependencies of a file open in VSCode).

(It also appears that cache doesn't work consistently on Windows. Initially when installing git I mistakenly selected "checkout Windows-style" (CRLF), and cache didn't work. Then I set git config --global core.autocrlf input (recommended here) and re-checked out mathlib4 branches but Lake is still building from scratch, and I noticed that .lake/packages/std etc. still contain .lean files with CRLF in them. I then cloned the mathlib4 repo again, and finally cache works, but sometimes after I check out a different branch and run cache get, Lake still build from scratch. Cloning a new copy of the repo seems to always work initially. I'll report if the problem persists and if I could find some patterns ...)

[Mario Carneiro]

I think there isn't anything that can be done about this, windows really doesn't like concurrent modification of files that are being read

[Mario Carneiro]

cache should work with CRLF files

[Mario Carneiro]

it normalizes line endings

[Richard Copley]

Mario Carneiro said:

I was not able to reproduce this on windows or linux

lake new foo math
cd foo
lake update
REM start language server in Foo.lean, make coffee
lake update

[Scott Morrison]

@Richard Copley, this does not repro for me on Windows.

• For your comment "start language server", I assume you mean you are opening the foo folder in VSCode, and then clicking on Foo.lean
• For me that then takes a few seconds, and then a "Imports are out of data and must be rebuilt; use the 'Restart File' command in your editor." message appears.
• Because that wasn't mentioned in your instructions, I didn't click that, but went back to the command line to run the final
• lake update then runs without errors, in a few seconds.

[Scott Morrison]

(and then clicking the button is VSCode prompting to rebuilt imports succeeds, and I can edit Foo.lean as expected)

[Richard Copley]

Ok, many thanks @Mario Carneiro and @Scott Morrison. I use Emacs. I will try to understand and explain what it is I'm seeing. In the next few days, if I have time.

[Scott Morrison]

Oh! VSCode is the supported editor.

[Richard Copley]

I do get the same error if I run lake update in the command line while VSCode is running. In your experiment, the language server wasn't running due to the error you describe. If you get the project up and running in the usual way, so the info view is responding properly, then run lake update in the command line, you should see it too.