feat: use Lake.withLockFile in cache

[semorrison]

---

[semorrison]

It might be a while before we can merge this! (Edit: mistakenly thought we needed a Lean bump first.)

[semorrison]

@tydeu, could you advise how an end-user should specify the path to the lockfile, rather than hard-coding as I've done here?

[tydeu]

@semorrison Why does this need a Lean bump? lake.lock landed before the current 08-15 nightly used by mathlib?

[tydeu]

@semorrison As to your question:

could you advise how an end-user should specify the path to the lockfile, rather than hard-coding as I've done here?

The filename (lake.lock) is available as Lake.lockFileName. To get the full path, you can load he configuration and using it to determine the location of the build directory and lock file. However, that is expensive and probably not worth it here. Hard coding it seems fine, especially as the build directory is already hard coded in cache elsewhere (e.g., LIBDIR). Eventually, a solution to leanprover/lean4#2753 may help solve this.

[semorrison]

@semorrison Why does this need a Lean bump? lake.lock landed before the current 08-15 nightly used by mathlib?

Absolutely right, I must not have branched off the latest master on my first attempt at this. I will force push this now.

[alreadydone]

(Edit: Oh nevermind, I see it's reported on Zuliip.)

My PR fails CI run and the only error (I think) concerns lake.lock. Do you know what's happening? Thanks.

[3800/3804] Building Mathlib.NumberTheory.ZetaFunction
[3802/3804] Building Mathlib.AlgebraicGeometry.Morphisms.FiniteType
[3803/3804] Building Mathlib
error: no such file or directory (error code: 2)
  file: ./build/lake.lock
Error: The process '/usr/bin/bash' failed with exit code 1
Remove matcher: gcc

[tydeu]

@semorrison One issue that just occurred to me with this PR is that the cache lock will conflict with Lake's in #6603. Thus, there needs to be a --no-lock flag in cache (or something similar) to disable locking when called from within the build process.

[semorrison]

I've implemented --no-lock.

Really we should be using the lean4-cli library here, but as we want to replace cache anyway I don't think it's worth doing, so I've just added to step to the argument mangling.

[tydeu]

LGTM.

[semorrison]

Marking as WIP, as we have temporarily reverted the lockfile.