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

Remove REVERTcast #14773

Merged
merged 4 commits into from Oct 9, 2021
Merged

Remove REVERTcast #14773

merged 4 commits into from Oct 9, 2021

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Aug 12, 2021 •
edited by Alizter

@SkySkimmer SkySkimmer added needs: documentation Documentation was not added or updated. 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 Aug 12, 2021
@maximedenes
Copy link
Member

I don't quite remember, but the debug printer may also not print these casts. How about adding them there too?

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Aug 19, 2021
@SkySkimmer SkySkimmer removed the needs: test-suite update Test case should be added to / updated in the test-suite. label Aug 19, 2021
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Sep 13, 2021
@SkySkimmer
Adapt to coq/coq#14773 (cast_type is just an enum)
1a4108c
SkySkimmer added a commit to SkySkimmer/QuickChick that referenced this pull request Sep 13, 2021
@SkySkimmer
Adapt to coq/coq#14773 (cast_kind is an enum)
2ce41ed
@SkySkimmer SkySkimmer added kind: user messages Improvement of error messages, new warnings, etc. and removed needs: documentation Documentation was not added or updated. needs: overlay This is breaking external developments we track in CI. needs: changelog entry This should be documented in doc/changelog. labels Sep 13, 2021
@SkySkimmer SkySkimmer marked this pull request as ready for review September 13, 2021 12:45
@SkySkimmer SkySkimmer requested review from a team as code owners September 13, 2021 12:45
@JasonGross
Copy link
Member

How does this factor with the _ = _ :> _ notation? (Is this tested in the test-suite?)

@SkySkimmer
Copy link
Contributor Author

How does this factor with the _ = _ :> _ notation? (Is this tested in the test-suite?)

It seems to work fine. There were already some incidental tests (eg

coq/test-suite/ssr/view_case.v

Line 23 in eeb4bc6

Goal forall x : 'I_1, x = 0 :> nat.
), I added a specific test.

@SkySkimmer SkySkimmer removed the request for review from a team October 9, 2021 09:04
@SkySkimmer
Copy link
Contributor Author

Can I get an assignee / merge?

@Alizter Alizter self-assigned this Oct 9, 2021
@Alizter
Copy link
Contributor

Alizter commented Oct 9, 2021

@SkySkimmer Do I need to check/do anything with the overlays?

@SkySkimmer
Copy link
Contributor Author

Tell upstream to merge when you merge

@Alizter
Copy link
Contributor

Alizter commented Oct 9, 2021

@SkySkimmer I don't have an account for the inria gitlab overlay, so you will have to tell them there.

@Alizter
Copy link
Contributor

Alizter commented Oct 9, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0acddf0 into coq:master Oct 9, 2021
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 9, 2021

@Alizter: Please take care of the following overlays:

  • 14773-SkySkimmer-revertcast.sh

This was referenced Oct 9, 2021
Merged
Merged
Merged
Merged
Merged
Merged
@SkySkimmer SkySkimmer deleted the revertcast branch October 9, 2021 10:24
SkySkimmer added a commit to SkySkimmer/QuickChick that referenced this pull request Oct 9, 2021
@SkySkimmer
Adapt to coq/coq#14773 (cast_kind is an enum)
574def4
SkySkimmer added a commit to coq-community/aac-tactics that referenced this pull request Oct 9, 2021
@SkySkimmer
Merge pull request #88 from SkySkimmer/revertcast
cba7dba 
Adapt to coq/coq#14773 (convert_concl has a ~cast argument)
@herbelin
Copy link
Member

herbelin commented Oct 9, 2021 •
edited

Note: I would not have spent time myself to investigate further how to exploit the REVERTcast for better controlling the const-const critical pair in conversion, and thus, it is ok to remove an unused infrastructure, but it seems to still be a direction which is worth to be investigated at some time (among the various pending ideas to control conversion efficiency).

ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Oct 9, 2021
@ppedrot
Merge pull request #429 from SkySkimmer/revertcast
922467e 
Adapt to coq/coq#14773 (convert_concl has a ~cast argument)
ppedrot added a commit to MetaCoq/metacoq that referenced this pull request Oct 9, 2021
@ppedrot
Merge pull request #589 from SkySkimmer/revertcast
615c12a 
Adapt to coq/coq#14773 (removal of revertcast)
damien-pous pushed a commit to damien-pous/relation-algebra that referenced this pull request Oct 9, 2021
@SkySkimmer @damien-pous
Adapt to coq/coq#14773 (convert_concl has a ~cast argument)
8577db1 
With DEFAULTcast cast:false is the previous behaviour, otherwise cast:true.
Lysxia pushed a commit to QuickChick/QuickChick that referenced this pull request Oct 9, 2021
@SkySkimmer @Lysxia
Adapt to coq/coq#14773 (cast_kind is an enum)
a379035
gares added a commit to LPCIC/coq-elpi that referenced this pull request Oct 9, 2021
@gares
Merge pull request #288 from SkySkimmer/revertcast
cd88387 
Adapt to coq/coq#14773 (cast_type is just an enum)
LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Oct 25, 2021
@LasseBlaauwbroek
Adapt to a bunch of upstream PR's (see below), possibly more
d710f31 
coq/coq#15023
coq/coq#14598
coq/coq#13837
coq/coq#14773
@ppedrot ppedrot mentioned this pull request Feb 25, 2022
Closed
@clayrat clayrat mentioned this pull request Nov 29, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@herbelin herbelin herbelin approved these changes

@Zimmi48 Zimmi48 Zimmi48 approved these changes

Assignees

@Alizter Alizter

Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.15+rc1
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@SkySkimmer @maximedenes @JasonGross @herbelin @Alizter @Zimmi48 @jfehrle