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

Rename Coq requirement prefix to Stdlib #19310

Merged
merged 7 commits into from
Sep 10, 2024
Merged

Rename Coq requirement prefix to Stdlib #19310

merged 7 commits into from
Sep 10, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jul 3, 2024 •
edited
Loading

In anticipation of renaming to Rocq.
For backward compatibility, "Coq" still works by being replaced on the fly with "Stdlib" and emiting a warning.

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

Overlays (to be merged in sync with the current PR)

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 3, 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 3, 2024
@Villetaneuse
Copy link
Contributor

Is this a record for the number of reviewers? 😄

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 3, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from ddf5e5d to 3324c9d Compare July 3, 2024 13:03
@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 3, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 3, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from 3324c9d to 18a492e Compare July 3, 2024 22:51
@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 3, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 4, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from 18a492e to bb685b5 Compare July 4, 2024 21:43
@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 4, 2024
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 5, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from bb685b5 to 972db10 Compare July 5, 2024 12:56
@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 5, 2024
proux01 added a commit to proux01/coqutil that referenced this pull request Jul 6, 2024
@proux01
Adapt to coq/coq#19310
38105d3
proux01 added a commit to coq-community/aac-tactics that referenced this pull request Jul 6, 2024
@proux01
Adapt to coq/coq#19310
186dd60
proux01 added a commit to proux01/QuickChick that referenced this pull request Jul 6, 2024
@proux01
Adapt to coq/coq#19310
508339b
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 6, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from 972db10 to 0d0d19c Compare July 6, 2024 13:10
@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 6, 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 8, 2024
proux01 added a commit to coq-community/coq-dpdgraph that referenced this pull request Jul 12, 2024
@proux01
Adapt to coq/coq#19310
0459e94
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 12, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from 0d0d19c to 72e23e7 Compare July 12, 2024 16:23
@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. labels Jul 12, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 12, 2024

🔴 CI failures at commit 72e23e7 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 439641c succeeded

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

🏃 @coqbot ci minimize will minimize the following targets: ci-elpi_hb, ci-fiat_crypto_legacy, ci-metacoq
  • You can also pass me a specific list of targets to minimize as arguments.
  • If you tag me saying @coqbot ci minimize all, I will additionally minimize the following target (which I do not suggest minimizing): ci-coq_tools (because coq-tools is too sensitive to the output of coqc to be minimized at this time (instead, @JasonGross can help diagnose and fix the issue))

proux01 added a commit to proux01/metacoq that referenced this pull request Jul 13, 2024
@proux01
Adapt to coq/coq#19310
92b8d82
@coq coq deleted a comment from coqbot-app bot Jul 13, 2024
@silene
Copy link
Contributor

silene commented Sep 4, 2024

Unless someone proposes a solution for the following kind of issue, I will merge by the end of the week.

Module Coq. Definition foo := ... End Coq.
Check Coq.foo. (* not found *)

@mattam82
Copy link
Member

mattam82 commented Sep 9, 2024

Shouldn't we change so that it at least warns of the Coq -> Stdlib renaming in addition to the Not_found in that case? And mention in the changelog this incompatibility

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 9, 2024
@proux01 proux01 force-pushed the stdlib-logical-name branch from 96b56eb to 48eeb50 Compare September 9, 2024 09:22
@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 Sep 9, 2024
@proux01
Copy link
Contributor Author

proux01 commented Sep 9, 2024

Done

@proux01
Copy link
Contributor Author

proux01 commented Sep 9, 2024

@silene CI green (fcsl failure is unrelated)

@silene silene added part: standard library The standard library stdlib. part: config Configuration, e.g. -R -Q -I for libraries labels Sep 10, 2024
@silene
Copy link
Contributor

silene commented Sep 10, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 7fec4bd into coq:master Sep 10, 2024
5 of 7 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 10, 2024

@silene: Please take care of the following overlays:

  • 19310-proux01-stdlib-logical-name.sh

@proux01 proux01 deleted the stdlib-logical-name branch September 10, 2024 07:01
proux01 added a commit to coq-community/coq-dpdgraph that referenced this pull request Sep 10, 2024
@proux01
Merge pull request #133 from coq-community/coq_19310
4904006 
Adapt to coq/coq#19310
ppedrot added a commit to MetaCoq/metacoq that referenced this pull request Sep 10, 2024
@ppedrot
Merge pull request #1093 from proux01/coq_19310
1d547df 
Adapt to coq/coq#19310
liyishuai pushed a commit to QuickChick/QuickChick that referenced this pull request Sep 10, 2024
@proux01 @liyishuai
Adapt to coq/coq#19310
ae0c2bc
ejgallego added a commit to rocq-archive/coq-serapi that referenced this pull request Sep 10, 2024
@ejgallego
Merge pull request #422 from proux01/coq_19310
652a8cc 
Adapt to coq/coq#19310
ejgallego pushed a commit to proux01/coq-lsp that referenced this pull request Sep 10, 2024
@proux01 @ejgallego
[coq] Adapt to coq/coq#19310
2180402
ejgallego added a commit to ejgallego/coq-lsp that referenced this pull request Sep 10, 2024
@ejgallego
Merge pull request #809 from proux01/coq_19310
ce2bea5 
Adapt to coq/coq#19310
@ejgallego ejgallego mentioned this pull request Sep 20, 2024
Merged
43 tasks
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Oct 9, 2024
@Zimmi48
Replace forgotten Coq prefixes by Stdlib.
b4ec8da 
Follow up of coq#19310.
@Zimmi48 Zimmi48 mentioned this pull request Oct 9, 2024
Merged
@jfehrle jfehrle mentioned this pull request Oct 17, 2024
Merged
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

@samuelgruetter samuelgruetter samuelgruetter left review comments

@Zimmi48 Zimmi48 Zimmi48 left review comments

@JasonGross JasonGross JasonGross left review comments

@silene silene silene approved these changes

Assignees

@silene silene

Labels
kind: deprecation Deprecation part: config Configuration, e.g. -R -Q -I for libraries part: standard library The standard library stdlib.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
10 participants
@proux01 @Villetaneuse @SkySkimmer @JasonGross @andres-erbsen @ejgallego @silene @mattam82 @Zimmi48 @samuelgruetter