lean-pr-testing and cache

Stream: mathlib4

[Mauricio Collares]

Does Lake hash the toolchain commit SHA (as displayed by lean -v) or does it hash the toolchain name (i.e. lean-toolchain's contents)? If the latter, then I think CI shouldn't use lake exe cache get/put when running on a PR with a lean-pr-testing toolchain, because those releases are updated "in-place" when new commits arrive on a PR.

[Scott Morrison]

:ping_pong: @Mac Malone

[Scott Morrison]

Following up, since we added the "check cache" step in Mathlib CI there have been many failures in lean-pr-testing-NNNN branches that I would like to get to the bottom of.

As an example, on branch#lean-pr-testing-2612, lake exe cache get reports retrieving 100% of the files, but then lake build starts from scratch.

[Scott Morrison]

The answer to Mauricio's question is relevant here, as this toolchain has been "updated in place".

[Mac Malone]

@Mauricio Collares @Scott Morrison It hashes the the commit SHA (i.e., lean --githash)

[Scott Morrison]

Thanks. Unfortunately that means I don't understand the cache failure on branch#lean-pr-testing-2612. :-(

[Mauricio Collares]

My bet is that the cache script hashes lean-toolchain only.

[Mauricio Collares]

https://github.com/leanprover-community/mathlib4/blob/master/Cache/Hashing.lean#L60

[Mauricio Collares]

So for the 2612 case, Lake will report different hashes, but the cache script will store them in the same place.

[Mauricio Collares]

But given Mac's information, this only causes rebuilds (the cache hit corresponds to out-of-date files), which seems less worrying than using out-of-date oleans.

[Scott Morrison]

#7513