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

deprecate ZArith.Zdigits #17733

Merged
merged 1 commit into from Jul 5, 2023
Merged

deprecate ZArith.Zdigits #17733

merged 1 commit into from Jul 5, 2023

Conversation

andres-erbsen
Copy link
Contributor

@andres-erbsen andres-erbsen commented Jun 13, 2023 •
edited

  • Added changelog.

@andres-erbsen andres-erbsen added kind: cleanup Code removal, deprecation, refactorings, etc. part: standard library The standard library stdlib. labels Jun 13, 2023
@andres-erbsen andres-erbsen added this to the 8.18+rc1 milestone Jun 13, 2023
@andres-erbsen andres-erbsen requested a review from a team as a code owner June 13, 2023 20:28
@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 13, 2023
@andres-erbsen
Copy link
Contributor Author

@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 Jun 13, 2023
Alizter
Alizter reviewed Jun 13, 2023
View reviewed changes
Copy link
Contributor

@Alizter Alizter left a comment •
edited

Choose a reason for hiding this comment

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

could you add what to use instead for the deprecations? i.e. using the note option of the deprecated attribute.

doc/changelog/11-standard-library/17733-deprecate-Zdigits.rst Outdated Show resolved Hide resolved
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 14, 2023

🔴 CI failure at commit 19123b4 without any failure in the test-suite

✔️ Corresponding job for the base commit ca8db7b succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-geocoq
  • You can also pass me a specific list of targets to minimize as arguments.

⚠️ ⌛ You may want to wait until the pipeline for the base commit (ca8db7b) finishes.

@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 14, 2023
@andres-erbsen
Copy link
Contributor Author

could you add what to use instead for the deprecations? i.e. using the note option of the deprecated attribute.

I added note= statements. The standard library does not have an exact drop-in replacement for this functionality, so some of the recommendations are based on anticipated context of use. I added a corresponding request for comments to the changelog.

@andres-erbsen
Copy link
Contributor Author

Full CI failures at 19123b4 look unrelated (geocoq and ltac2 compiler)

@andres-erbsen andres-erbsen 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 Jun 15, 2023
@SkySkimmer
Copy link
Contributor

Didn't realize I broke ltac2 compiler, I should be more careful about making its changes go through its CI.
Should be fixed now

@gares
Copy link
Member

gares commented Jul 5, 2023

ping @coq/number-maintainers this PR seems ready, can you review it quickly please?

proux01
proux01 approved these changes Jul 5, 2023
View reviewed changes
Copy link
Contributor

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

Sorry, I thought I already merged that one (I apparently mixed it with #17601 ), let's merge.

@proux01 proux01 self-assigned this Jul 5, 2023
@proux01
Copy link
Contributor

proux01 commented Jul 5, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 2924529 into coq:master Jul 5, 2023
6 checks passed
@coqbot-app coqbot-app bot added this to Request 8.18+rc1 inclusion in Coq 8.18 Jul 5, 2023
gares added a commit to gares/coq that referenced this pull request Jul 7, 2023
@gares
Backport PR coq#17733: deprecate ZArith.Zdigits
9d58130
@coqbot-app coqbot-app bot moved this from Request 8.18+rc1 inclusion to Shipped in 8.18+rc1 in Coq 8.18 Jul 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter left review comments

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: standard library The standard library stdlib.
Projects
Coq 8.18
Shipped in 8.18+rc1
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@andres-erbsen @SkySkimmer @gares @proux01 @Alizter