lake lock file

Stream: lean4

[Yury G. Kudryashov]

I have to killall lean sometimes (e.g., to make sure that a running lean doesn't break lake exe cache get). Recently (today or yesterday), Lean started to show this warning:

warning: waiting for prior `lake build` invocation to finish... (remove './build/lake.lock' if stuck)

I have 2 suggestion:

• add a TERM signal handler that deletes this lock file;
• if there is no process with the number recorded in this file, then delete it.

[Yury G. Kudryashov]

The second suggestion assumes that nobody tries to run lake on 2 computers that mount the same directory via some network filesystem.

[Scott Morrison]

:ping_pong: @Mac Malone

[Scott Morrison]

These would be both lovely, I am deleting lake.lock about 20 times a day, mostly after ctrl-c on a build.

[Mac Malone]

@Yury G. Kudryashov Thanks for the feedback! Sadly, it is my understanding that both of these suggestions would require new platform-sensitive Lean primitives. Thus, deciding how, when, and whether to implement this will require some discussion internally.

[Scott Morrison]

Here's a new one @Mac Malone:

...
info: [996/997] Building Mathlib.GroupTheory.Sylow
error: no such file or directory (error code: 2)
  file: ./build/lake.lock

I can create an issue if you'd like!

[Eric Wieser]

This just happened in CI

[Mac Malone]

It looks like this error is caused by Lake being unable to delete the lock file, implying that something deleted it between its initial locking and the end of the build.

[Mac Malone]

@Scott Morrison / @Eric Wieser

[Mac Malone]

I should definitely make Lake not care if the lockfile is there to delete, but it is still weird that this would happen, so I am curious what caused the lock file to disappear.

[François G. Dorais]

The usual solution is to just issue an info? That won't block but it can still be tracked if necessary.

[Joachim Breitner]

I also saw it on CI today, when a build was cancelled during lake build (because of a new push to that PR), and then the “upload cache” job is stuck due to the stale lock file.
(e.g. https://github.com/leanprover-community/mathlib4/actions/runs/5895203319/job/15990444490?pr=6643)
I’m not sure if the intention was to upload such partial cancelled builds to the cache.

[Scott Morrison]

Yes, we definitely want to upload partial cancelled builds.

[Joachim Breitner]

It looks like in this case the github action doesn’t show the “waiting for lockfile” message (maybe because GHA timed out the job), but I saw it while watching that job’s output

[Matthew Ballard]

Does this also prevent one from editing files while building or is it just me?

[Mario Carneiro]

no I don't think it does, although you could potentially be stuck editing without lean

[Matthew Ballard]

Sorry, I should have said "editing files with the language server"

[Mario Carneiro]

the language server will block waiting for a lake build to work, so if you open a new file during that time you won't get any infos

[Matthew Ballard]

Previously, I would see some dependencies rebuilt but would be able to edit normally once that finished while having a global lake build call going

[Mario Carneiro]

I don't actually know whether lake takes the lock eagerly or only when it realizes it needs to write something

[Matthew Ballard]

Now, the infoview warns tells me about lake.lock until lake build finishes

[Mario Carneiro]

certainly it would be good to allow that use case, i.e. if you start a lake build of mathlib, see X.lean finishes building, and then open X.lean while the overall build is still ongoing

[Matthew Ballard]

For example, if you break stuff with a new toolchain and have lots to build and fix

[Mac Malone]

Mario Carneiro said:

I don't actually know whether lake takes the lock eagerly or only when it realizes it needs to write something

It takes the lock eagerly. Doing the later would be very difficult due to how the build system works (i.e., each build would have to independently request the lock if it determines it needs building and would require an atomic cross-task lock on getting the lock, which would introduce quite some overhead).

[Scott Morrison]

Mario Carneiro said:

certainly it would be good to allow that use case, i.e. if you start a lake build of mathlib, see X.lean finishes building, and then open X.lean while the overall build is still ongoing

I have been frequently encountering this over the last few days. To make it worse, the current solution when faced with this problem is to ctrl-c the global build that is happening in a terminal, but then you still need to rm build/lake.lock by hand before the editor window will take over the build.

[Mac Malone]

Yep, this is part of the trade off of having a general lock file. While it prevents Lake processes from stepping on each other toes (which was a previous source of concern), it also prevents them from stepping on each others toes when you want them to (which is the new source of concerns).

[James Gallicchio]

is it possible for the processes to 'release' their file locks before exiting?