Open joehendrix opened 11 months ago
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?
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.
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.
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.
A post-merge hook that:
lake update std
in itauto-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:
std-bump-NNN
?)
main
instead of the Std PR branchlake update std
delegated
, label it with auto-merge-after-CI
(Currently I am doing this all by hand, and I would like to not be doing it. :-)
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 bystd4
maintainers, but too disruptive for Mathlib to accept right now.