Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automate testing against Mathlib? #309

Open
joehendrix opened this issue Oct 20, 2023 · 6 comments
Open

Automate testing against Mathlib? #309

joehendrix opened this issue Oct 20, 2023 · 6 comments

Comments

@joehendrix
Copy link
Contributor

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
Copy link
Member

digama0 commented Oct 21, 2023

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?

@kim-em
Copy link
Collaborator

kim-em commented Oct 23, 2023

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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.

@joehendrix joehendrix closed this as not planned Won't fix, can't repro, duplicate, stale Oct 23, 2023
@kim-em kim-em reopened this Oct 24, 2023
@kim-em
Copy link
Collaborator

kim-em commented Oct 24, 2023

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

@kim-em
Copy link
Collaborator

kim-em commented Oct 24, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants