A `lake build` failure that does not reproduce locally

Stream: CSLib

[Ching-Tsun Chou]

Alas, I'm now getting a lake build failure on Github (see cslib#216) which I'm not able to reproduce locally. I removed .lake/, re-downloaded the cache (lake exec cache get), and re-did lake build and lake test without generating any error message on my machine (M1 MBA). I restarted Lean in the file in question in VScode, which also did not produce any any error message. What's going on?

[Ching-Tsun Chou]

It seems that the Lean used by Github is version v4.27.0-rc1, but my local lean-toolchaincontains leanprover/lean4:v4.26.0. My patch is on top of a main that is at v4.26.0 (commit: c8bd20b10d7e9c0c5bed69f275eeb9fa300f4d5e). Shouldn't Github use the Lean version specified in my patch?

Anyway, I'm going to rebase on top of the current main (which is at v4.27.0-rc1) and try again.

[Sebastian Ullrich]

https://github.com/actions/checkout?tab=readme-ov-file#checkout-pull-request-head-commit-instead-of-merge-commit - we do this in lean4

[Ching-Tsun Chou]

After rebasing I can reproduce the error locally.

But shouldn't Github tell me that it is using a different version of Lean tool chain from the one specified in the PR?

[Chris Henson]

We could have a warning message for users when the merge commit has a different toolchain from the base branch, but this behavior overall makes sense to me.

[Ching-Tsun Chou]

A warning message would be much appreciated. BTW, grind behavior seems to have changed quite a bit from v4.26.0 to v4.27.0-rc1. I had to spell out many more details in a proof to make the newer version of grind happy; see the last commit in cslib#216.

[Chris Henson]

I have a guess why, I'll investigate further when I review. (Probably in a day or two, flying to visit family today)