feat: create CACHEDIR.TAG file in .lake directory

[henkkuli]

Create CACHEDIR.TAG file in .lake directory when it is first created. The file does not get recreated if removed if .lake directory is not removed, too. While technically against the spec, this is how Rust does it, too. Moreover, this simplifies the implementation a lot.

This change also introduces a test to check that the file gets cretead but not recreated. This test needs to change e.g. if we decide that CACHEDIR.TAG should always be recreated.

---

Closes #4998

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4d4d485c19925cf8c4122e553328ce320ff02439 --onto 8c96d213f3089ac2352ed95e79645f4cdbd70ebf. (2024-08-15 15:55:36)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4d4d485c19925cf8c4122e553328ce320ff02439 --onto b486c6748b153bda628575635baa28aeeb38b8c5. (2024-08-20 09:31:18)

[henkkuli]

Marking this as non-draft as I noticed that @tydeu has initially approved the idea on Zulip.

[tydeu]

Looks pretty good to me! I have one major suggested change, but, nonetheless, great job! I really like the detailed test. 😄

[tydeu]

This is not really what this this does. If a user deletes the CACHEDIR.TAG (because they wish the directory to be cached) and then, unrelatedly, delete the configuration trace (e.g., due to an incomplete configuration), this will regenerate the CACHEDIR.TAG (which would be quite surprising behavior).

Now that creating the lake directory is something worth doing independently, I suggest refactoring out the cfg.lakeDir creation here to the top of this function (outside all the locking). That is, just add something like this to the top and remove it from here:

if !(<- cfg.lakeDir.pathExists) then
  IO.FS.createDirAll cfg.lakeDir
  -- Create CACHEDIR.TAG file only when .lake directory is first created
  IO.FS.writeFile (cfg.lakeDir / "CACHEDIR.TAG") cachedirTagContent

[tydeu]

Suggested change

	# Building craetes CACHEDIR.TAG
	# Building creates CACHEDIR.TAG

[tydeu]

This is an odd spec requirement that does not seem desirable. A user may wish to remove the tag and cache the directory and Lake should not override that.

[kim-em]

@henkkuli, would you be able to address @tydeu's review comments above? It would be nice to have this in.