Skip to content

Revert (most of) #15802 #16237

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
Jun 27, 2022
Merged

Revert (most of) #15802 #16237

merged 1 commit into from
Jun 27, 2022

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jun 23, 2022 •
edited
Loading

As discussion in #15802 indicates we should revert most fo this and rather go for the plan in #16224 implemented by #16230

  • Updated changelog.
  • Updated documentation.

@proux01 proux01 requested review from a team as code owners June 23, 2022 16:11
@proux01 proux01 added this to the 8.16.0 milestone Jun 23, 2022
@proux01 proux01 added part: typeclasses The typeclass mechanism. part: coercions The coercion mechanism. labels Jun 23, 2022
@proux01
Copy link
Contributor Author

proux01 commented Jun 23, 2022

@ppedrot an alternative would be to backport #16230 in 8.16 which would save a release cycle for the deprecation.
The risks of breaking anything seem very limited since #16230 only introduces a new syntax currently unused, but the decision belongs to the RM, let me know what you prefer.

Zimmi48
Zimmi48 reviewed Jun 23, 2022
View reviewed changes
@Alizter Alizter self-assigned this Jun 25, 2022
@Zimmi48
Copy link
Member

Zimmi48 commented Jun 25, 2022

FWIW, PRs should not be manually added to the Coq 8.16 backporting project. The milestone is sufficient and coqbot takes care of adding PRs to the project after they are merged.

@Alizter Alizter removed their assignment Jun 25, 2022
@Zimmi48 Zimmi48 added kind: fix This fixes a bug or incorrect documentation. kind: cleanup Code removal, deprecation, refactorings, etc. labels Jun 26, 2022
@Zimmi48
Copy link
Member

Zimmi48 commented Jun 26, 2022

Given that this is related to class and instances and can impact performance, I'm a bit worried by the three jobs having timed out. Is there a known explanation for them?

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 26, 2022
@proux01
Revert (most of) rocq-prover#15802
14392e4 
As discussion in rocq-prover#15802 indicates we
should revert most fo this and rather go for the plan in
rocq-prover#16224 implemented by
rocq-prover#16230
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 27, 2022
@proux01
Copy link
Contributor Author

proux01 commented Jun 27, 2022

I just reran the jobs and they completed in much less than 3h.
Then I had to rebase and again the CI seems green.
So I don't know what happened (but since this is mostly removing a deprecation warning, I'm not expecting any performance impact here).
So I guess this is ready and waiting for an assignee.

@Alizter Alizter self-assigned this Jun 27, 2022
@Alizter
Copy link
Contributor

Alizter commented Jun 27, 2022

@ppedrot just to double check, will you be backporting this.

@ppedrot
Copy link
Member

ppedrot commented Jun 27, 2022

@Alizter yes.

@Alizter
Copy link
Contributor

Alizter commented Jun 27, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 8721957 into rocq-prover:master Jun 27, 2022
@proux01 proux01 deleted the revert_15802 branch June 27, 2022 21:00
@proux01
Copy link
Contributor Author

proux01 commented Jun 27, 2022

Thanks!
@ppedrot feel free to ask for a backporting PR targeting branch 8.16 if needed
(there were changes on master so cherry pick may not work out of the box)

@ppedrot
Copy link
Member

ppedrot commented Jun 29, 2022

I wouldn't mind a standalone PR against 8.16 indeed, if you have a bit of time.

@proux01
Copy link
Contributor Author

proux01 commented Jun 30, 2022

@ppedrot: here it is #16256

ppedrot added a commit that referenced this pull request Jun 30, 2022
@ppedrot
Merge PR #16256: [8.16] Backport #16237
ffcc588 
Ack-by: Alizter
Reviewed-by: ppedrot
@Zimmi48 Zimmi48 modified the milestones: 8.16.0, 8.17+rc1 Jun 30, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 left review comments

@Alizter Alizter Alizter approved these changes

Assignees

@Alizter Alizter

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: fix This fixes a bug or incorrect documentation. part: coercions The coercion mechanism. part: typeclasses The typeclass mechanism.
Projects
None yet
Milestone
8.17+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@proux01 @Zimmi48 @Alizter @ppedrot