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

Correctly handle opaque primitive projections in Evarconv #17788

Merged
merged 1 commit into from Sep 8, 2023
Merged

Correctly handle opaque primitive projections in Evarconv #17788

merged 1 commit into from Sep 8, 2023

Conversation

rlepigre
Copy link
Contributor

@rlepigre rlepigre commented Jun 29, 2023 •
edited

This is a fix for #17774.

The adds missing cases to function evar_eqappr_x, where in the Rigid, Rigid case we know that projections are opaque, and so are unifiable if the projections are equal, the projected terms convertible, and the stacks convertible.

The bug can be observed on master with the included test-suite file.

@rlepigre rlepigre requested a review from a team as a code owner June 29, 2023 16:06
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 29, 2023
@SkySkimmer
Copy link
Contributor

Please use more descriptive PR and commit titles

@rlepigre rlepigre changed the title Fix #17774. Correctly handle opaque primitive projections in Evarconv Jun 29, 2023
SkySkimmer
SkySkimmer approved these changes Jul 3, 2023
View reviewed changes
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

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

Seems reasonable. Handling the projection / constant case is kinda dubious but it's always hard to figure out what the correct thing to do is with these projection constants.

Needs tests and changelog.

@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. needs: test-suite update Test case should be added to / updated in the test-suite. labels Jul 3, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Jul 3, 2023
@SkySkimmer SkySkimmer added kind: fix This fixes a bug or incorrect documentation. part: unification The unification mechanism. part: primitive records The primitive record and primitive projection mechanism. labels Jul 3, 2023
@rlepigre
Copy link
Contributor Author

rlepigre commented Jul 3, 2023

I added a changelog entry, but I can't directly add tests for this fix on master, as I said in the description. One solution is to first merge #17777, and use the code in the description.

@rlepigre rlepigre mentioned this pull request Jul 10, 2023
Merged
2 tasks
@rlepigre
Copy link
Contributor Author

rlepigre commented Sep 6, 2023

I now added a test case, so as far as I'm concerned this is also ready to be merged @SkySkimmer.

ppedrot
ppedrot reviewed Sep 6, 2023
View reviewed changes
pretyping/evarconv.ml Outdated Show resolved Hide resolved
@rlepigre rlepigre mentioned this pull request Sep 6, 2023
Closed
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Sep 6, 2023
@SkySkimmer SkySkimmer self-assigned this Sep 6, 2023
@rlepigre rlepigre force-pushed the br/fix-17774 branch 2 times, most recently from 41e01ae to 372ba1e Compare September 6, 2023 12:42
@gares gares added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: test-suite update Test case should be added to / updated in the test-suite. labels Sep 7, 2023
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 7, 2023
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 96dd231 into coq:master Sep 8, 2023
6 checks passed
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
8fdd835 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
609c958 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
5565c7e 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
3fddc8c 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 25, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
957331c 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 30, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17788: Correctly handle opaque primitive projections in …
f4af145 
…Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
@Janno Janno mentioned this pull request Nov 8, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot left review comments

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

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

Successfully merging this pull request may close these issues.

None yet
4 participants
@rlepigre @SkySkimmer @ppedrot @gares