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

Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v #429

Merged
merged 3 commits into from Apr 1, 2020
Merged

Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v #429

merged 3 commits into from Apr 1, 2020

Conversation

pi8027
Copy link
Member

@pi8027 pi8027 commented Nov 15, 2019 •
edited

Motivation for this change

This PR partially addresses #404. It extends the comparison predicates leqP, ltnP, and ltngtP in ssrnat.v to allow case analysis on minn and maxn. It also changes the ordering of arguments of lcomparableP, (lcomparable_)leP, (lcomparable_)ltP, and (lcomparable_)ltgtP in order.v.

Things done/to do
  • merge dependency: Add FCSL-PCM library to CI #435
  • added a compatibility module
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • [ ] added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

@pi8027 pi8027 force-pushed the extend-nat-comparison branch 3 times, most recently from bc57dcf to e3f9b97 Compare November 21, 2019 09:27
@anton-trunov anton-trunov mentioned this pull request Nov 21, 2019
Merged
2 tasks
pi8027
pi8027 commented Nov 23, 2019
View reviewed changes
mathcomp/ssreflect/ssrnat.v Outdated Show resolved Hide resolved
@pi8027 pi8027 force-pushed the extend-nat-comparison branch 2 times, most recently from 47ce0a9 to ec83f47 Compare November 30, 2019 04:00
@pi8027 pi8027 marked this pull request as ready for review January 3, 2020 15:03
@pi8027 pi8027 changed the title [WIP] Extend comparison predicates for nat with minn and maxn Extend comparison predicates for nat with minn and maxn Jan 3, 2020
@pi8027 pi8027 force-pushed the extend-nat-comparison branch 5 times, most recently from 3c03bf1 to 698108c Compare January 9, 2020 09:57
@gares gares added the needs: documentation PR that lacks documentation, or with broken documentation. label Jan 30, 2020
@pi8027 pi8027 changed the title Extend comparison predicates for nat with minn and maxn Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v Jan 30, 2020
@pi8027
Copy link
Member Author

pi8027 commented Jan 30, 2020

I just changed the title and resolved a conflict with #453. Since order.v has not been released yet, I'm still not sure how it should be recorded in CHANGELOG.

pi8027
pi8027 commented Mar 16, 2020
View reviewed changes
CHANGELOG_UNRELEASED.md
Comment on lines +95 to +125
+ In the development process of this version of Mathematical Components, the
ordering of arguments of comparison predicates `lcomparableP`,
`(lcomparable_)ltgtP`, `(lcomparable_)leP`, and `(lcomparable_)ltP` in
`order.v` has been changed as follows. This is a potential source of
incompatibilities.
* before the change:
```
lcomparableP x y : incomparel x y
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
(y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
ltgtP x y : comparel x y
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
(y `&` x) (x `&` y) (y `|` x) (x `|` y).
leP x y :
lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
ltP x y :
ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
```
* after the change:
```
lcomparableP x y : incomparel x y
(y `&` x) (x `&` y) (y `|` x) (x `|` y)
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
ltgtP x y : comparel x y
(y `&` x) (x `&` y) (y `|` x) (x `|` y)
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
leP x y :
lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
ltP x y :
ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
```
Copy link
Member Author

Choose a reason for hiding this comment

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

So I did this documentation work. Since we decided to have a beta release, I think we should keep this entry in the beta version and remove it in the stable release.

Copy link
Member

Choose a reason for hiding this comment

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

I agree

@pi8027
Copy link
Member Author

pi8027 commented Mar 18, 2020

Hello @ggonthier, @CohenCyril, can we merge this before the next beta release? Thanks.

CohenCyril
CohenCyril approved these changes Mar 18, 2020
View reviewed changes
Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

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

LGTM @ggonthier

@ybertot
Copy link
Member

ybertot commented Mar 25, 2020

There remains a tag "Needs:documentation" that is confusing for release managers. Can you please clarify, complete the work if needed, and merge? @CohenCyril @ggonthier

@CohenCyril CohenCyril removed the needs: documentation PR that lacks documentation, or with broken documentation. label Mar 25, 2020
@CohenCyril
Copy link
Member

There remains a tag "Needs:documentation" that is confusing for release managers. Can you please clarify, complete the work if needed, and merge? @CohenCyril @ggonthier

I was a bit worried about the backward compatibility issues triggered by this PR, but after @pi8027's experiments, it does not not look so bad. I also thought @ggonthier could be opposed to it for the same reasons (or others?). I think we can merge for the beta and backtrack if this causes more trouble than relief to our users (in the former case, we could have distinct spec lemmas for the enhanced cased analysis instead of overloading leqP...).

@ybertot ybertot merged commit e44b131 into math-comp:master Apr 1, 2020
@ybertot
Copy link
Member

ybertot commented Apr 1, 2020

Thanks @pi8027 @CohenCyril

@pi8027 pi8027 deleted the extend-nat-comparison branch April 8, 2020 03:58
@pi8027 pi8027 mentioned this pull request Apr 10, 2020
Open
@pi8027 pi8027 mentioned this pull request Apr 28, 2020
Closed
pi8027 added a commit to pi8027/math-comp that referenced this pull request May 4, 2020
@pi8027
Remove a CHANGELOG entry introduced in math-comp#429
565bc40 
that explains an incompatibility between development versions
@pi8027 pi8027 mentioned this pull request May 4, 2020
Merged
pi8027 added a commit to pi8027/math-comp that referenced this pull request May 5, 2020
@pi8027
Reformulate a CHANGELOG entry introduced in math-comp#429
4961a67 
that explains an incompatibility between development versions
pi8027 added a commit to pi8027/math-comp that referenced this pull request May 5, 2020
@pi8027
Reword a CHANGELOG entry introduced in math-comp#429
6658910 
that explains an incompatibility between development versions
CohenCyril added a commit that referenced this pull request May 5, 2020
@CohenCyril
Merge pull request #495 from pi8027/post-cleaning-pr429
3515b33 
Reword a CHANGELOG entry introduced in #429
@pi8027 pi8027 mentioned this pull request Aug 13, 2020
Merged
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

Assignees

@ggonthier ggonthier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@pi8027 @ybertot @CohenCyril @gares @ggonthier