-
Notifications
You must be signed in to change notification settings - Fork 7
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
Bump MathComp version to >= 1.12.0 #3
Conversation
coq-community/coqeal#38 and coq/opam#1714 should fix the CI failure with coq.dev. |
Waiting for a fix on multinomials. https://github.com/math-comp/apery/pull/3/checks?check_run_id=3786055714 |
It seems that math-comp/math-comp#766 made hanson.v diverging🤦♂️ |
@pi8027 FYI, I started the CI again to test the to be released version of mathcomp |
I think this PR is ready. Shall we merge so that we can test apery in MathComp CI? @amahboubi |
The CI failure is spurious (and should eventually be solved by math-comp/multinomials#53 and a release AFAIU). |
CI green. |
Many thanks @pi8027 for this amazing work. I do not have time for reviewing such a PR right away, but I am of course fine with a review by someone else, or even with a merge after minimal checks. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Many thanks @pi8027 for this amazing work. I do not have time for reviewing such a PR right away, but I am of course fine with a review by someone else, or even with a merge after minimal checks.
I did a minimal check, and I approve.
Thanks a lot! |
Thanks! |
This PR makes apery compatible with MathComp 1.12.0 and later. It also cleans up proof scripts as preliminary work for #4. This PR itself does not add any extra dependency or enhance the proof automation facility.
Closes #2