refactor: .lake directory for Lake outputs

[tydeu]

Store the build directory, build archives, package directory, and compiled configuration inside a dedicated directory for Lake outputs (i.e., .lake). There is also now a more rigorous check on lakefile.olean compatibility. (edit: split out into #2842)

Closes #2713.

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-25 09:38:43) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-25 11:38:09) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-27 10:17:22) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-27 20:32:39) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-28 21:20:28) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-29 10:52:48) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-29 23:28:20) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-30 19:02:07) View Log
• 💥 Mathlib branch lean-pr-testing-2749 build failed against this PR. (2023-10-30 23:00:36) View Log
• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-07 19:08:40)
• 🟡 Mathlib branch lean-pr-testing-2749 build against this PR was cancelled. (2023-11-09 01:51:45) View Log
• ✅ Mathlib branch lean-pr-testing-2749 has successfully built against this PR. (2023-11-09 03:10:52) View Log
• ✅ Mathlib branch lean-pr-testing-2749 has successfully built against this PR. (2023-11-13 13:34:55) View Log
• ✅ Mathlib branch lean-pr-testing-2749 has successfully built against this PR. (2023-11-13 23:44:55) View Log
• ✅ Mathlib branch lean-pr-testing-2749 has successfully built against this PR. (2023-11-14 03:10:45) View Log

[tydeu]

@Kha I was going to ask you if the IO.FS additions looked good since they were outside my module ownership. Does your 🎉 imply you are satisfied with them?

[tydeu]

@semorrison A note for you when you can take a look: The mathlib CI is currently breaking for reasons other than this PR and I think this PR will likely need a proper CI run on mathlib since it may break some assumptions there about the location of the build directory.

[kim-em]

Options for a successful PR run:

• rebase this PR onto d126c09 (the commit underlying nightly-2023-10-25), which should give an immediate run.
• wait until nightly-2023-10-26 lands and I have fixed Std+Mathlib for it (approximately +10 hours from now), and then push an empty commit (or anything) to this branch.

[Kha]

@Kha I was going to ask you if the IO.FS additions looked good since they were outside my module ownership. Does your 🎉 imply you are satisfied with them?

I see they are being used in the lockfile code but I can't tell what's going on for lack of comments. What is the difference to readFile/writeFile?

[tydeu]

@Kha

What is the difference to readFile/writeFile?

readFile/writeFile would allow two racing lake processes to load a bad olean (e.g., one writes an updating lock and then another loads the old olean before the other writes the new one, or one writes a new olean and another loads it before the other writes the new lock). The new primitives allow us to open a handle, read the old hash, and not release it until we write the new one. I will add a comment to this effect in the code.

[Kha]

The new primitives allow us to open a handle, read the old hash, and not release it until we write the new one.

Mmh, if I understand you correctly and you believe that open/fdopen locks the file against concurrent access from other processes, that is simply untrue I'm afraid. That is, it is still racy.

[tydeu]

@Kha

that is simply untrue I'm afraid. That is, it is still racy.

Oops, yeah, it appears I confused the exclusion offered by e.g. O_EXCL in writeNew with general file handles. 🤦‍♂️ I guess I actually also needed lock/unlock file handle bindings for flock, LockFileEx, and UnlockFileEx.

[Kha]

I guess I actually also needed lock/unlock file handle bindings for flock, LockFileEx, and UnlockFileEx.

Phew, I'm impressed you made that work in quick time but this looks like it will take some time to review. Why not leave worrying about races to #2766 as mentioned there? On a positive note, this looks like the right functions to implement a general build lock that avoids the issues of the first try.

[Kha]

@joehendrix Speaking in general, I think it would be great if you could review additions to Init.System.IO and similar modules from a standard library perspective - they may as well be in std4 if it wasn't for bootstrapping. But for this one, let's first wait which functions we actually need in the end.

[tydeu]

Anyway, this should be done. The last platform addition was some thing I was supposed to add after a discussion with Mario, but it slipped my mind until now. The lakefile.olean should now be properly lock-guarded to avoid race conditions and store enough information to be invalidated by Lake on any relevant change.

[tydeu]

I split the lakefile.olean improvement out into a separate PR that builds on this one (#2842). Hopefully, this will be cleaner.

[Kha]

I'll remove my review request, unless there's something specific you want me to look at

[tydeu]

Following the Zulip poll, I have decided to follow the majority and make the default Lake directory .lake. Furthermore, as this is now a pure-Lake PR, I will likely merge soon after the mathlib incompatibility is resolved, unless there are any objections.

/cc @semorrison, @Kha, @joehendrix: Since you all commented, it seems proper to notify all of you before I merge in case there is anything else you wish to add.