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

Clean up deprecations #10575

Merged
merged 3 commits into from Dec 2, 2019
Merged

Clean up deprecations #10575

merged 3 commits into from Dec 2, 2019

Conversation

maximedenes
Copy link
Member

@maximedenes maximedenes commented Jul 25, 2019 •
edited

We try to make deprecations coherent between the manual and the code.

We also remove some deprecated and undocumented features.

@maximedenes maximedenes changed the title Document deprecated Clean-up deprecations Jul 26, 2019
@maximedenes maximedenes changed the title Clean-up deprecations Clean up deprecations Jul 26, 2019
@maximedenes maximedenes mentioned this pull request Jul 26, 2019
Closed
@maximedenes maximedenes marked this pull request as ready for review July 26, 2019 12:03
silene
silene approved these changes Jul 26, 2019
View reviewed changes
Copy link
Contributor

@silene silene left a comment

Choose a reason for hiding this comment

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

If cutrewrite is meant to be superseded by enough, should it not be reflected in ide/coq_commands.ml?

@silene
Copy link
Contributor

silene commented Jul 26, 2019

And same remark for commands, obviously.

Zimmi48
Zimmi48 reviewed Jul 26, 2019
View reviewed changes
doc/sphinx/addendum/generalized-rewriting.rst Outdated Show resolved Hide resolved
doc/sphinx/proof-engine/tactics.rst Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 added kind: cleanup Code removal, deprecation, refactorings, etc. kind: documentation Additions or improvement to documentation. labels Jul 26, 2019
@maximedenes
Copy link
Member Author

If cutrewrite is meant to be superseded by enough, should it not be reflected in ide/coq_commands.ml?

I'm not sure what you are suggesting I should do, concretely.

@silene
Copy link
Contributor

silene commented Jul 26, 2019

What I meant is that, if the users click on "cutrewrite", they get a deprecation warning. The interface should never make it much easier to use a deprecated feature than a non-deprecated one. So, "cutrewrite" should be removed from the list, and "enough" should be added. Similarly, for deprecated commands.

@maximedenes
Copy link
Member Author

What I meant is that, if the users click on "cutrewrite", they get a deprecation warning. The interface should never make it much easier to use a deprecated feature than a non-deprecated one. So, "cutrewrite" should be removed from the list, and "enough" should be added. Similarly, for deprecated commands.

I see, thanks. But this seems to me more like a CoqIDE maintenance task, which I'd rather not do (I'm working hard on VsCoq these days instead). Especially, if enough is missing, it probably means that a pass should be done on tactics by CoqIDE maintainers.

@Zimmi48

This comment has been minimized.

Sign in to view
@maximedenes
Copy link
Member Author

@Zimmi48 could you be the assignee for this PR?

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 14, 2019

Sure.

@Zimmi48 Zimmi48 self-assigned this Oct 14, 2019
Zimmi48
Zimmi48 reviewed Oct 16, 2019
View reviewed changes
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

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

What I meant is that, if the users click on "cutrewrite", they get a deprecation warning. The interface should never make it much easier to use a deprecated feature than a non-deprecated one. So, "cutrewrite" should be removed from the list, and "enough" should be added. Similarly, for deprecated commands.

I see, thanks. But this seems to me more like a CoqIDE maintenance task, which I'd rather not do (I'm working hard on VsCoq these days instead). Especially, if enough is missing, it probably means that a pass should be done on tactics by CoqIDE maintainers.

This deserves an issue at the very least.

Did you open one? Note the menu "Reference in new issue" which make it easy to open a new issue from a comment.

Remove deprecated commands AddPath, AddRecPath and DelPath

It doesn't look like they were clearly deprecated, but I don't mind removing them as they were not documented either.

doc/sphinx/addendum/generalized-rewriting.rst Outdated Show resolved Hide resolved
doc/sphinx/addendum/type-classes.rst Outdated Show resolved Hide resolved
doc/sphinx/proof-engine/tactics.rst Outdated Show resolved Hide resolved
tactics/equality.ml Outdated Show resolved Hide resolved
vernac/vernacentries.ml Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 added this to the 8.11+beta1 milestone Oct 16, 2019
@ppedrot ppedrot modified the milestones: 8.11+beta1, 8.12+beta1 Nov 1, 2019
cpitclaudel added a commit that referenced this pull request Nov 20, 2019
@cpitclaudel
Merge PR #11119: 8.10-backportable part of #10575
54d0af9 
Reviewed-by: cpitclaudel
vbgl added a commit to vbgl/coq that referenced this pull request Nov 21, 2019
@vbgl
Backport PR coq#11119: 8.10-backportable part of coq#10575
86260e1
ppedrot added a commit to ppedrot/coq that referenced this pull request Nov 25, 2019
@ppedrot
Backport PR coq#11119: 8.10-backportable part of coq#10575
1893389
This was referenced Nov 26, 2019
Merged
Merged
Merged
@vbgl vbgl mentioned this pull request Nov 27, 2019
Merged
19 tasks
@Zimmi48 Zimmi48 mentioned this pull request Nov 30, 2019
Closed
@maximedenes @Zimmi48
Actually deprecate the cutrewrite tactic
cd8c4fc 
The manual was already saying that it was deprecated, but no warning was
emitted.

Fixes coq#10572
@maximedenes @Zimmi48
Actually deprecate SearchAbout
a394876 
Fixes coq#10573
@Zimmi48 Zimmi48 modified the milestones: 8.12+beta1, 8.11+beta1 Nov 30, 2019
Zimmi48
Zimmi48 approved these changes Nov 30, 2019
View reviewed changes
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

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

I've removed commits made irrelevant or already integrated in PRs #11119, #11184, #11186, #11187, I've rebased and I've fixed the two remaining issues that I had noticed during my review (in particular the deprecation warning when calling Search). So this is now good to go and I will merge this on Monday.

@ppedrot
Copy link
Member

ppedrot commented Dec 1, 2019

@Zimmi48 if you can do it soon enough, we might still make the beta on time for the 1st of December AOE...

Zimmi48 added a commit that referenced this pull request Dec 2, 2019
@Zimmi48
Merge PR #10575: Clean up deprecations
31e1096 
Reviewed-by: Zimmi48
Reviewed-by: silene
@coqbot coqbot added this to Request 8.11+beta1 inclusion in Coq 8.11 Dec 2, 2019
@Zimmi48 Zimmi48 merged commit a394876 into coq:master Dec 2, 2019
ppedrot added a commit to ppedrot/coq that referenced this pull request Dec 2, 2019
@ppedrot
Backport PR coq#10575: Clean up deprecations
a3cc684
@coqbot coqbot moved this from Request 8.11+beta1 inclusion to Shipped in 8.11+beta1 in Coq 8.11 Dec 2, 2019
@maximedenes
Copy link
Member Author

Thanks for taking care of this!

@maximedenes maximedenes deleted the document-deprecated branch August 26, 2023 08:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

@silene silene silene approved these changes

@mattam82 mattam82 Awaiting requested review from mattam82

@PierreCorbineau PierreCorbineau Awaiting requested review from PierreCorbineau

@ppedrot ppedrot Awaiting requested review from ppedrot

Assignees

@Zimmi48 Zimmi48

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: documentation Additions or improvement to documentation.
Projects
No open projects
Coq 8.11
  
Shipped in 8.11+beta1
Milestone
8.11+beta1
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@maximedenes @silene @Zimmi48 @ppedrot