coq 8.19.0; math-comp 1.19.0

[jesboat]

• Have you followed the guidelines for contributing?
• Have you ensured that your commits follow the commit style guide?
• Have you checked that there aren't other open pull requests for the same formula update/change?
• Have you built your formula locally with HOMEBREW_NO_INSTALL_FROM_API=1 brew install --build-from-source <formula>, where <formula> is the name of the formula you're submitting?
• Is your test running fine brew test <formula>, where <formula> is the name of the formula you're submitting?
• Does your build pass brew audit --strict <formula> (after doing HOMEBREW_NO_INSTALL_FROM_API=1 brew install --build-from-source <formula>)? If this is a new formula, does it pass brew audit --new <formula>?

---

[tchajed]

You can fix the CI failure by bumping the revision in the math-comp formula (see #135135 for an example).

[jesboat]

Looks like an actual incompatibility with the version of math-comp in the formula and coq 8.19:

  File "./algebra/qpoly.v", line 347, characters 0-18:
  Error: Let does not support Proof using.

Appears to be an (undocumented) side effect of coq/coq#17576 and addressed by math-comp/math-comp#1115, which was included in math-comp 1.19.0.

[jesboat]

Putting both coq and math-comp in the same PR seems like the least objectionable way to deal with this. If they're in separate PRs and math-comp lands first, then the bottle gets built with the old coq, and so the coq PR would need to bump math-comp's revision immediately. On the other hand, if the coq PR lands first, then there would be a gap between then and when the math-comp PR lands when math-comp's bottles wouldn't work. If they're in the same PR, they land simultaneously, and there is no interval when a brew update might result in a non-working configuration and it avoids a math-comp revision bump.

[github-actions]

🤖 An automated task has requested bottles to be published to this PR.