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

Quickfix for deprecated #19300

Merged
merged 4 commits into from
Jul 8, 2024
Merged

Quickfix for deprecated #19300

merged 4 commits into from
Jul 8, 2024

Conversation

gares
Copy link
Member

@gares gares commented Jul 1, 2024 •
edited
Loading

Deprecation and UserWarn declare type t and 'a with_qf the latter being like t but enriched with a quick fix generated by the datum of type 'a.
Attributes provides the parser for simple case and for the with_qf variant when 'a is Libnames.extended_global_reference (a syndef of a globref).

Now stuff like Definition x := t of Notation x := t can carry #[deprecated(use=this.qualified.name)] and that qualid is resolved in the context of the declaration and used to print a quickfix using the Nametab, so that the proposed replacement does not incur in a capture.

Overlay:

playground-1720012114147

@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 Jul 1, 2024
@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 Jul 2, 2024
@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 Jul 2, 2024
@gares gares force-pushed the quickfix-deprecated branch from def6094 to 6060cdc Compare July 2, 2024 20:56
@gares gares marked this pull request as ready for review July 2, 2024 21:04
@gares gares requested review from a team as code owners July 2, 2024 21:04
@gares gares added this to the 8.21+rc1 milestone Jul 2, 2024
@gares gares added the kind: user messages Error messages, warnings, etc. label Jul 2, 2024
@gares gares force-pushed the quickfix-deprecated branch from 6060cdc to 1308474 Compare July 2, 2024 21:31
@gares gares requested a review from a team as a code owner July 2, 2024 21:31
@gares gares force-pushed the quickfix-deprecated branch from 1308474 to 724c19a Compare July 3, 2024 08:52
@gares
Copy link
Member Author

gares commented Jul 3, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jul 3, 2024
@gares gares force-pushed the quickfix-deprecated branch from 724c19a to d499b64 Compare July 3, 2024 09:01
@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 Jul 3, 2024
@gares
Copy link
Member Author

gares commented Jul 3, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jul 3, 2024
@gares
Copy link
Member Author

gares commented Jul 3, 2024

@SkySkimmer or @silene would you take this one? It is mostly infrastructure for library maintenance

SkySkimmer
SkySkimmer reviewed Jul 3, 2024
View reviewed changes
vernac/attributes.mli Outdated Show resolved Hide resolved
@SkySkimmer SkySkimmer self-assigned this Jul 3, 2024
@gares gares force-pushed the quickfix-deprecated branch from 1df32d2 to af8fa8e Compare July 3, 2024 13:19
@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 Jul 3, 2024
@gares gares force-pushed the quickfix-deprecated branch from af8fa8e to 50a86b0 Compare July 3, 2024 14:00
@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 Jul 3, 2024
@gares
Copy link
Member Author

gares commented Jul 3, 2024

@coqbot run full ci

gares added a commit to gares/coq-elpi that referenced this pull request Jul 5, 2024
@gares
adapt to coq/coq#19300
cea331c
@gares gares force-pushed the quickfix-deprecated branch from aff3771 to 4054719 Compare July 5, 2024 15:22
@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 Jul 5, 2024
@gares gares force-pushed the quickfix-deprecated branch from 4054719 to cfb758a Compare July 5, 2024 15:23
@gares
Copy link
Member Author

gares commented Jul 5, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jul 5, 2024
@gares gares force-pushed the quickfix-deprecated branch from cfb758a to 2347950 Compare July 5, 2024 15:51
@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 Jul 5, 2024
@gares
Copy link
Member Author

gares commented Jul 5, 2024 •
edited
Loading

done again, taking off.

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jul 5, 2024
@gares
Copy link
Member Author

gares commented Jul 5, 2024

I must have messed up something

@gares gares force-pushed the quickfix-deprecated branch from 2347950 to 878546b Compare July 5, 2024 21:36
@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 Jul 5, 2024
@gares
Copy link
Member Author

gares commented Jul 5, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jul 5, 2024
@gares
Copy link
Member Author

gares commented Jul 6, 2024

Looks like the failure is unrelated

@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0356dd9 into coq:master Jul 8, 2024
5 of 7 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 8, 2024

@SkySkimmer: Please take care of the following overlays:

  • 19300-gares-quickfix-deprecated.sh

@gares gares deleted the quickfix-deprecated branch July 8, 2024 09:14
@gares
Copy link
Member Author

gares commented Jul 8, 2024

thanks

gares added a commit to LPCIC/coq-elpi that referenced this pull request Jul 8, 2024
@gares
Merge pull request #649 from gares/quickfix-deprecated
f421547 
adapt to coq/coq#19300
ejgallego added a commit to ejgallego/coq-lsp that referenced this pull request Jul 8, 2024
@ejgallego
Merge pull request #801 from gares/quickfix-deprecated
821edf9 
adapt to coq/coq#19300
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Jul 8, 2024
@ppedrot
Merge pull request #610 from gares/quickfix-deprecated
abed609 
adapt to coq/coq#19300
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@silene silene silene left review comments

@herbelin herbelin herbelin left review comments

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: user messages Error messages, warnings, etc.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@gares @SkySkimmer @herbelin @silene