Automate testing against Mathlib?

[joehendrix]

This repo is upstream from Mathlib, but we'd like to ensure changes to main do not break Mathlib.

Should we add a build step or task that builds Mathlib (perhaps storing the relevant Mathlib version in a file here (e.g., .github/mathlib_test_version)?

I'm not sure of the exact policy; perhaps main commits that break mathlib are allowed if a Mathlib PR that fixes the issues is approved?

Hopefully it would not be needed, but if this slows things down, we could potentially add a staging branch (devel) for changes that are accepted by std4 maintainers, but too disruptive for Mathlib to accept right now.

[digama0]

I think the best solution would be something like what lean core has: a bot which tests changes against mathlib, but does not gate CI. Maybe @semorrison can hook us up?

[semorrison]

Building Mathlib directly from Std CI is not a great option: it will turn 2 minutes CI into 90 minutes of CI.

We could certainly reproduce the setup from Lean core. However it is already pretty kludgy, and relies on manual work keeping nightly-testing up to date, and makes some not-quite-true assumptions that regularly result in spurious failures.

I'd prefer not to reproduce that whole setup here if possible, until we have some good ideas about reducing the manual burden of that system.

My preference is for now to stick with the current system (i.e. let Mathlib break). I think we are experiencing a transient phase at the moment as we try to pull lots of material out of Mathlib, and during that I think it's easiest if we are flexible/ad-hoc. Assuming this phase actually ends, we can then have a think about the long-term CI setup.

[joehendrix]

I'll close this for now and keep the current approach in place. Perhaps revisit as library and tooling becomes more mature so that builds are faster.

[joehendrix]

One thing we could do if we revisit is add a post-merge hook that builds Mathlib. This way we aren't slowing down std merges, but at least have notice of whether Mathlib may need to delay upgrading or need patches.

[semorrison]

A post-merge hook that:

• checks out a copy of Mathlib
• runs lake update std in it
• opens a PR at Mathlib for that change
• labels with auto-merge-after-CI

would already be helpful.

Of course sometimes this PR would fail, because Mathlib actually needs updates. In the basic model, this would be up to the humans to deal with (hopefully by merging an existing open PR into the auto-generated one, or closing the auto-generated one in favour of the existing open one).

We could then optionally make two further additions:

1. Have CI for that Mathlib PR ping a comment back to the (by now closed) Std PR if it fails, for visibility.
2. Automate looking for an existing Mathlib PR (perhaps by branch name? std-bump-NNN?)

• If we find an existing Mathlib PR that corresponds to this Std PR
• Edit the lakefile to point back to main instead of the Std PR branch
• Run lake update std
• If that PR is already labelled delegated, label it with auto-merge-after-CI

[semorrison]

(Currently I am doing this all by hand, and I would like to not be doing it. :-)