x64 and arm64 GitHub runners sharing cached `.lake` files

Stream: general

[Austin Letson]

Is it correct that x64 and arm64 systems cannot share cached .lake files?

For context, currently lean-action uses this cache key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

With the current cache key an ubuntu runner will never use the cache from a macos runner. However an x64 ubuntu runner could potentially use a cache from an arm64 ubuntu runner. This is potentially leading to problems.

My thought was to modify the lean-action key to also include the {{ runner.arch }} context variable so that runners with different architectures do not share cache entries.

[Eric Wieser]

Yes, I don't think these can be shared across platforms

[Eric Wieser]

Especially if one is a GMP-enabled platform and the other is not

[Eric Wieser]

Though what you _can_ cache is the output of lake exe cache pack, which is platform independent

[Austin Letson]

Okay, thanks for the confirmation.

Eric Wieser said:

Though what you _can_ cache is the output of lake exe cache pack, which is platform independent

Interesting. I may look into if we could leverage this.