Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: lake.lock file for builds #2385

Merged
merged 2 commits into from
Aug 8, 2023
Merged

feat: lake.lock file for builds #2385

merged 2 commits into from
Aug 8, 2023

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Aug 4, 2023

A feature frequently requested on Zulip (c.f. 1, 2, 3).

@tydeu tydeu force-pushed the lake-lock branch 3 times, most recently from 068334d to 34629b0 Compare August 5, 2023 01:18
@tydeu
Copy link
Member Author

tydeu commented Aug 5, 2023

I am currently stumped. I have no clue why this or #2384 is failing. The do not fail on my machine (in MSY?S2 or WSL), so it likely has to be some difference between how the CI and my local machine handle background processes.

@digama0
Copy link
Collaborator

digama0 commented Aug 5, 2023

You made an ABI breaking change to a type in Init, you most likely need to set interpreter.prefer_native in stage0/src/stdflib_flags.h and possibly do a stage0 update

@tydeu
Copy link
Member Author

tydeu commented Aug 5, 2023

@digama0 That does not appear to be the bug. Looking at the logs, lake is working fine (the lock file is generated and waiting on properly). The test is simply not terminating once the script finishes for some reason.

FYI, I think the reason this did not cause ABI breakage is that FS.Mode is still a uint8_t and the name of the C symbol for Handle.mk has not changed.

Copy link
Member

@Kha Kha left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good but I'd also like to hear about potential future plans. Do we believe we'll want to end up with granular locking, e.g. per-module? What would that look like?

src/lake/Lake/Build/Monad.lean Show resolved Hide resolved
@Kha
Copy link
Member

Kha commented Aug 7, 2023

The test is simply not terminating once the script finishes for some reason.

Are we sure it's the end of the script and not fg that's blocking? Could the background process for some reason interfere?

@tydeu
Copy link
Member Author

tydeu commented Aug 7, 2023

@Kha

Are we sure it's the end of the script and not fg that's blocking? Could the background process for some reason interfere?

I am not yet, but that is what I plan on testing today. However, my reason for believing it is the end of the script is that Lake background job does successfully resume, acquire the lock and begin building (as can be seen from the Building Test output).

@tydeu
Copy link
Member Author

tydeu commented Aug 7, 2023

@Kha

Do we believe we'll want to end up with granular locking, e.g. per-module? What would that look like?

While theoretically useful, I am incline to avoid this. If the watchdog is merged into Lake, one lock for the server is fine. For the CLI, invoking multiple lake builds in parallel is already a bad idea (as it prevents internal build deduplication and adds Lake workspace overhead). Thus, a single per-Workspace build lock file seems sufficient.

@tydeu
Copy link
Member Author

tydeu commented Aug 7, 2023

@Kha The last run confirms that the problem is on the script finish, not the fg (and pkill does not work).

@tydeu
Copy link
Member Author

tydeu commented Aug 8, 2023

@Kha Update: It appears the problem is the process substitution. CTest is waiting on it finish before completing the test.

@tydeu tydeu merged commit 3e4232c into leanprover:master Aug 8, 2023
12 checks passed
@tydeu tydeu deleted the lake-lock branch August 8, 2023 20:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants