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

Improve compat infrastructure #19370

Merged
merged 1 commit into from
Oct 11, 2024
Merged

Improve compat infrastructure #19370

merged 1 commit into from
Oct 11, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jul 15, 2024 •
edited
Loading

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 15, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 15, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 16, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 16, 2024
@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 17, 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 Sep 10, 2024
@Zimmi48
Copy link
Member

Zimmi48 commented Sep 27, 2024

The main argument in favor of this was that this compat infrastructure was no longer used.

In a Coq Call discussion, it was decided to keep this infrastructure, but make it more useful by:

  • only warning and not failing when a compat version is used which is no longer supported (similar to the behavior of flags and options)
  • using these compat files to silence deprecation warnings

@proux01 proux01 changed the title Try rm compat Improve compat infrastructure Sep 27, 2024
@proux01
Copy link
Contributor Author

proux01 commented Sep 27, 2024

Sorry, I'm still working on it, please let me a few weeks. I updated the title.

@proux01 proux01 mentioned this pull request Sep 30, 2024
Merged
43 tasks
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 6, 2024
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Oct 6, 2024
@proux01 proux01 added kind: infrastructure CI, build tools, development tools. needs: overlay This is breaking external developments we track in CI. needs: changelog entry This should be documented in doc/changelog. labels Oct 6, 2024
@proux01 proux01 added this to the 8.21+rc1 milestone Oct 6, 2024
proux01 added a commit to proux01/coq-serapi that referenced this pull request Oct 7, 2024
@proux01
Adapt to coq/coq#19370
9f32ab2
@proux01 proux01 mentioned this pull request Oct 7, 2024
Merged
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 7, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 7, 2024
@proux01 proux01 removed needs: overlay This is breaking external developments we track in CI. needs: changelog entry This should be documented in doc/changelog. labels Oct 7, 2024
@proux01 proux01 marked this pull request as ready for review October 7, 2024 14:24
@proux01 proux01 requested review from a team as code owners October 7, 2024 14:24
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 8, 2024
Zimmi48
Zimmi48 approved these changes Oct 8, 2024
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.

Looks great to me!

Minor comments below (the most important one being that we need to anticipate the move to Rocq). The previous infrastructure had the advantage that, by behind ad-hoc, it would have made this simpler. Maybe it can be decided whether to use the Coq or the Rocq prefix based on whether it starts by 8. or a bigger number?

doc/sphinx/practical-tools/coq-commands.rst Show resolved Hide resolved
doc/changelog/09-cli-tools/19370-compat-warning.rst Outdated Show resolved Hide resolved
doc/changelog/09-cli-tools/19370-compat-warning.rst Outdated Show resolved Hide resolved
sysinit/coqinit.ml Outdated Show resolved Hide resolved
theories/Compat/README.md Show resolved Hide resolved
@Zimmi48 Zimmi48 mentioned this pull request Oct 8, 2024
Merged
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 9, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 9, 2024
Zimmi48
Zimmi48 approved these changes Oct 9, 2024
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.

Do we want tests that the option behaves as it should when the file does not exist? And when it does?

Do we need other reviewers to look at this before merging?

doc/changelog/09-cli-tools/19370-compat-from.rst Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 self-assigned this Oct 9, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 9, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 9, 2024
@proux01
Copy link
Contributor Author

proux01 commented Oct 9, 2024

Do we want tests that the option behaves as it should when the file does not exist? And when it does?

I added a test (for each case)

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 9, 2024

Do we need other reviewers to look at this before merging?

I will merge at the end of the week if there are no more comments.

@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 Oct 10, 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 Oct 10, 2024
@proux01
Make compat more usable
50d4edb 
-compat X.Y used to produce an error when no CoqXY could be found,
this made the option rather unusable because one could use -compat X.Y
only on more recent X'.Y'.
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 10, 2024
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Oct 10, 2024
@Zimmi48
Copy link
Member

Zimmi48 commented Oct 11, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 462a65a into coq:master Oct 11, 2024
7 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 11, 2024

@Zimmi48: Please take care of the following overlays:

  • 19370-proux01-improve-compat.sh

@proux01 proux01 deleted the test_rm_compat branch October 11, 2024 15:44
ejgallego added a commit to rocq-archive/coq-serapi that referenced this pull request Oct 11, 2024
@ejgallego
Merge pull request #426 from proux01/coq_19370
5e8d6ad 
Adapt to coq/coq#19370
@proux01 proux01 mentioned this pull request Oct 16, 2024
Merged
1 task
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

Assignees

@Zimmi48 Zimmi48

Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@proux01 @Zimmi48