8000 Fix #6297: handle constraints like (u+1 <= Set/Prop) by SkySkimmer · Pull Request #6298 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fix #6297: handle constraints like (u+1 <= Set/Prop) #6298

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
Merged
merged 1 commit into from
Jan 17, 2018
Merged

Fix #6297: handle constraints like (u+1 <= Set/Prop) #6298

merged 1 commit into from
Jan 17, 2018

Conversation

SkySkimmer
Copy link
Contributor

Universe.levels is super suspicious honestly, we should make the caller explicitly ignore the +1s if they need to (but not in a backportable fix).

@SkySkimmer SkySkimmer added kind: fix This fixes a bug or incorrect documentation. needs: review part: universes The universe system. labels Dec 1, 2017
@SkySkimmer SkySkimmer added this to the 8.7.1 milestone Dec 1, 2017
@ppedrot
Copy link
Member
ppedrot commented Dec 1, 2017

Could @mattam82 document in the code a few of the invariants expected by this function? Apart from being inefficient, I share @SkySkimmer's concerns about the suspiciousness of this code.

@mattam82
Copy link
Member
mattam82 commented Dec 1, 2017

I agree it is suspicious, I'll try to explain the intent better

@mattam82 mattam82 self-assigned this Dec 1, 2017
@Zimmi48 Zimmi48 added the kind: anomaly An uncaught exception has been raised. label Dec 1, 2017
@SkySkimmer SkySkimmer mentioned this pull request Dec 2, 2017
Closed
@Zimmi48
Copy link
Member
Zimmi48 commented Dec 8, 2017

This PR has been inactive for the last 7 days. @SkySkimmer @ppedrot @mattam82 How to do progress?
I'll remind that this is in the 8.7.1 milestone but 8.7.1 is planned to be released next Friday (and thus should be ready before that).

@SkySkimmer
Copy link
Contributor Author

I'm just waiting for review.
This is a pretty simple change where we say that if we want u <= v and v is small then u must not contain any +1.
It's in the middle of a complicated function which could use better documentation but that's not in scope of this PR.

@Zimmi48
Copy link
Member
Zimmi48 commented Dec 14, 2017

@mattam82 Can you review this today?!

@Zimmi48 Zimmi48 modified the milestones: 8.7.1, 8.7.2 Dec 14, 2017
ppedrot
ppedrot approved these changes Jan 15, 2018
View reviewed changes
Copy link
Member
@ppedrot ppedrot left a comment

Choose a reason for hiding this comment

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

Relatively to my understanding of that part of the code, I believe that this patch is correct. I've already thought several times about a potential bug here actually.

maximedenes added a commit to maximedenes/coq that referenced this pull request Jan 17, 2018
@maximedenes
Merge PR rocq-prover#6298: Fix rocq-prover#6297: handle constraints l…
79b6f22 
…ike (u+1 <= Set/Prop)
@maximedenes maximedenes merged commit 8acf323 into rocq-prover:master Jan 17, 2018
@SkySkimmer SkySkimmer deleted the fix-6297 branch January 18, 2018 14:34
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Jan 19, 2018
@Zimmi48
Backport PR rocq-prover#6298: Fix rocq-prover#6297: handle constraint…
6654dcc 
…s like (u+1 <= Set/Prop)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

@mattam82 mattam82 Awaiting requested review from mattam82

Assignees

@mattam82 mattam82

Labels
kind: anomaly An uncaught exception has been raised. kind: fix This fixes a bug or incorrect documentation. part: universes The universe system.
Projects
None yet
Milestone
8.7.2
Development

Successfully merging this pull request may close these issues.
5 participants
@SkySkimmer @ppedrot @mattam82 @Zimmi48 @maximedenes
0