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

[Merged by Bors] - feat: polyrith tactic #942

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: polyrith tactic #942

wants to merge 4 commits into from

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Dec 9, 2022

The main functionality of polyrith is represented here: it contacts Sagemath to get the coefficients required to pass to linear_combination.

TODO:

  • fix docs & lint
  • fix tests
    • There are some auxiliary tactics used to construct test cases for polyrith and perform dry-run testing which does not require contacting sage in CI.

Since the mock testing setup is not done yet, you can only test it for real right now, but I don't want to run that in CI for the same reason so currently all the tests are commented out. Most of them are still failing though because of things like a missing instance for CommSemiring Rat or the existence of the Real type entirely.

@digama0 digama0 force-pushed the polyrith branch 2 times, most recently from cb9c25c to 5660838 Compare December 13, 2022 13:04
@semorrison
Copy link
Contributor

I've merged master, imported Mathlib.Data.Rat.Basic, and verified that the tests over ℚ now work. (I've left the tests commented out in the repo as Mario explained.)

@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 20, 2022
bors bot pushed a commit that referenced this pull request Dec 20, 2022
The main functionality of `polyrith` is represented here: it contacts Sagemath to get the coefficients required to pass to linear_combination.

TODO:
* [x] fix docs & lint
* [ ] fix tests
  * There are some auxiliary tactics used to construct test cases for `polyrith` and perform dry-run testing which does not require contacting sage in CI.

Since the mock testing setup is not done yet, you can only test it for real right now, but I don't want to run that in CI for the same reason so currently all the tests are commented out. Most of them are still failing though because of things like a missing instance for `CommSemiring Rat` or the existence of the `Real` type entirely.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Dec 21, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: polyrith tactic [Merged by Bors] - feat: polyrith tactic Dec 21, 2022
@bors bors bot closed this Dec 21, 2022
@bors bors bot deleted the polyrith branch December 21, 2022 00:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors.
Projects
Status: Done
Development

Successfully merging this pull request may close these issues.

None yet

2 participants