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

Stop caring about unfolding state of primproj in constr_matching #15559

Merged
merged 1 commit into from Feb 2, 2022
Merged

Stop caring about unfolding state of primproj in constr_matching #15559

merged 1 commit into from Feb 2, 2022

Conversation

SkySkimmer
Copy link
Contributor

Fix #15554

@SkySkimmer SkySkimmer requested a review from a team as a code owner January 27, 2022 12:53
@SkySkimmer
Copy link
Contributor Author

Note all 9 combinations of matching with primitive projections in the added test.

@SkySkimmer
Copy link
Contributor Author

In this PR all the variants (compatibility constant, folded, unfolded) are equated by constr_matching (following the previous decision to equate compatibility constant and folded projection), other choices are possible.

@SkySkimmer
Copy link
Contributor Author

Not sure what the other tests were trying to do, the code I removed seems to test bugs(?)

@SkySkimmer
Copy link
Contributor Author

I guess this reverts b6e39ad

@ppedrot
Copy link
Member

ppedrot commented Jan 27, 2022

A good first step towards the removal of the unfolded flag if you ask me... But there is still quite a bit here and there.

@mattam82
Copy link
Member

In particular, equating the constant to the projection in evarconv when the constant is not delta-reducible, is giving me another headache (because whd_state_gen will not push a Zproj on the stack if it is not delta-reducible or does not have the unfolded flag)...

@ppedrot ppedrot self-assigned this Jan 27, 2022
@ppedrot ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Jan 27, 2022
@ppedrot ppedrot added this to the 8.16+rc1 milestone Jan 27, 2022
@ppedrot
Copy link
Member

ppedrot commented Jan 27, 2022

To be honest I am very surprised nobody relies on that in the CI.

@mattam82
Copy link
Member

Me too, I would have thought some of Jason's developments would rely on it.

JasonGross
JasonGross reviewed Jan 28, 2022
View reviewed changes
test-suite/bugs/bug_3656.v
Abort.

Goal forall h, setT h = setT h.
Proof. intro. progress unfold setT.
Copy link
Member

Choose a reason for hiding this comment

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

Does progress no longer see unfolding status as progress?

Copy link
Member

Choose a reason for hiding this comment

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

progress uses term equality, not matching. This PR shouldn't change this behaviour (but it will eventually, when we get rid of the unfolding flag).

ppedrot
ppedrot requested changes Jan 28, 2022
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.

This needs a changelog.

@ppedrot ppedrot added the needs: changelog entry This should be documented in doc/changelog. label Jan 28, 2022
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Feb 1, 2022
@SkySkimmer
Copy link
Contributor Author

changelogged

@ppedrot
Copy link
Member

ppedrot commented Feb 2, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 297cda7 into coq:master Feb 2, 2022
@SkySkimmer SkySkimmer deleted the constr-match-unfold-proj branch February 2, 2022 09:59
This was referenced Feb 5, 2022
Closed
Closed
@Blaisorblade Blaisorblade added the part: primitive records The primitive record and primitive projection mechanism. label May 11, 2022
@Blaisorblade Blaisorblade mentioned this pull request May 11, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JasonGross JasonGross JasonGross left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. part: primitive records The primitive record and primitive projection mechanism.
Projects
None yet
Milestone
8.16+rc1
Development

Successfully merging this pull request may close these issues.

match considers unfolded primitive projections as not matching against themselves
5 participants
@SkySkimmer @ppedrot @mattam82 @JasonGross @Blaisorblade