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.

Sign up for GitHub

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

Jump to bottom

Lia bugfix 11191 #11362

Merged
merged 1 commit into from
Jan 17, 2020
Merged

Lia bugfix 11191 #11362

merged 1 commit into from
Jan 17, 2020

Conversation

fajb
Copy link
Contributor

@fajb fajb commented Jan 6, 2020 •
edited
Loading

This PR solves regressions of lia reported by #11191 regarding Z.pow.

The regression is due to the fact that zify is now able to deal with Pos.pow and therefore some positivity constraints need to be added explicitly.

When the exponent of Z.pow is a variable, this is solved by adding an instance ZifyInst stating that
forall a b, 0 < a -> 0 < b -> 0 < a ^ b.

When the exponent of Z.pow is a constant, this is actually a product of variables and this is solved by performing a more aggressive pre-processing step performing interval analysis of monomials.

Kind: bug fix

Fixes #11191

  • Added test-suite

@fajb
[micromega] fix of bug coq#11191
97bec68 
- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.
@fajb fajb marked this pull request as ready for review January 7, 2020 08:50
@fajb fajb requested a review from a team as a code owner January 7, 2020 08:50
@fajb fajb added the kind: regression Problems that were not present in previous versions. label Jan 7, 2020
@fajb
Copy link
Contributor Author

fajb commented Jan 7, 2020 •
edited by Zimmi48
Loading

@ppedrot @maximedenes this is a regression in 8.10.
I leave to you to decide whether this can be integrated into 8.11.

@Zimmi48 Zimmi48 added the kind: fix This fixes a bug or incorrect documentation. label Jan 7, 2020
@ppedrot
Copy link
Member

ppedrot commented Jan 16, 2020

Ping @coq/micromega-maintainers. If you react in time this may make it into 8.11.0.

@maximedenes
Copy link
Member

Looks good, but let's launch a bench, just to be sure.

@maximedenes
Copy link
Member

https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/836/console

@maximedenes
Copy link
Member

Some small slowdown on coq performance tests, it seems.

@ppedrot
Copy link
Member

ppedrot commented Jan 17, 2020

@maximedenes this dev is always on the verge of noise, I think. I wouldn't take that as a positive proof of a slowdown.

@ppedrot
Copy link
Member

ppedrot commented Jan 17, 2020

(It's not even using lia, actually, for now it only contains a test for the pattern tactic.)

@maximedenes
Copy link
Member

maximedenes commented Jan 17, 2020 •
edited
Loading

this dev is always on the verge of noise, I think. I wouldn't take that as a positive proof of a slowdown.

Are you saying that our dedicated performance test has less reliable timings than other developments ? :o

@ppedrot
Copy link
Member

ppedrot commented Jan 17, 2020

AFAIU, this development is there to check for drastic performance changes, e.g. going from linear to quadratic. It amplifies minute timing diffs, so it's by design quite noisy. Furthermore, as I said, for now this is testing exactly one performance issue, namely the linearity of pattern.

maximedenes
maximedenes approved these changes Jan 17, 2020
View reviewed changes
Copy link
Member

@maximedenes maximedenes left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be nice to add some documentation on the introduced code, but apart from that, LGTM.

@maximedenes maximedenes self-assigned this Jan 17, 2020
@maximedenes maximedenes added this to the 8.11.0 milestone Jan 17, 2020
maximedenes added a commit that referenced this pull request Jan 17, 2020
@maximedenes
Merge PR #11362: Lia bugfix 11191
55ded80 
Reviewed-by: maximedenes
@maximedenes maximedenes merged commit 97bec68 into coq:master Jan 17, 2020
ppedrot added a commit to ppedrot/coq that referenced this pull request Jan 19, 2020
@ppedrot
Backport PR coq#11362: Lia bugfix 11191
199ac35
@ppedrot
Copy link
Member

ppedrot commented Jan 20, 2020

Backporting this looks like it's breaking flocq. Should we still backport the fix?

@fajb
Copy link
Contributor Author

fajb commented Jan 20, 2020

@ppedrot Is the flocq version frozen for 8.11 ?

I can think of another fix. It would consist in removing the support for Z.pow in zify.
This would be a (minor) regression of zify but probably less intrusive -- the support could be moved to another place and loaded on demand...

@ppedrot ppedrot mentioned this pull request Jan 20, 2020
Merged
@Zimmi48
Copy link
Member

Zimmi48 commented Jan 20, 2020

Given that support for Z.pow was added in 8.11, I suppose it makes sense to remove it in the 8.11 branch only. Thus, it wouldn't even qualify as a regression. We should just be careful to tweak the changelog.

@ppedrot
Copy link
Member

ppedrot commented Jan 20, 2020

How is that supposed to be removed? We need a 8.11-specific PR in any case...

@ppedrot ppedrot modified the milestones: 8.11.0, 8.12+beta1 Jan 20, 2020
@fajb fajb mentioned this pull request Jan 20, 2020
Merged
2 tasks
@andres-erbsen andres-erbsen mentioned this pull request Jan 21, 2020
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maximedenes maximedenes maximedenes approved these changes

Assignees

@maximedenes maximedenes

Labels
kind: fix This fixes a bug or incorrect documentation. kind: regression Problems that were not present in previous versions.
Projects
None yet
Milestone
8.12+beta1
Development

Successfully merging this pull request may close these issues.

Regression of lia ?
4 participants
@fajb @ppedrot @maximedenes @Zimmi48