Skip to content

Deprecate "end tac" ("...")#20917

Merged
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:depr-dots
Jul 28, 2025
Merged

Deprecate "end tac" ("...")#20917
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:depr-dots

Conversation

@SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Jul 16, 2025 •
edited
Loading

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 16, 2025
@SkySkimmer SkySkimmer requested review from a team as code owners July 16, 2025 12:54
@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, 2025
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 16, 2025

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

✔️ Corresponding jobs for the base commit f4e2506 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-stdlib, ci-stdlib
  • You can also pass me a specific list of targets to minimize as arguments.

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Jul 16, 2025
SkySkimmer
SkySkimmer commented Jul 16, 2025
View reviewed changes
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 17, 2025
@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 17, 2025
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 17, 2025
@SkySkimmer SkySkimmer requested a review from a team as a code owner July 17, 2025 14:27
@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 17, 2025
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 17, 2025

🔴 CI failures at commit 566c5f4 without any failure in the test-suite

✔️ Corresponding jobs for the base commit d6c1963 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-coqprime, ci-flocq, ci-math_classes
  • 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-trakt (because base job at d6c1963 failed)

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 18, 2025
@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 18, 2025
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 18, 2025

🔴 CI failures at commit 0f6a2ca without any failure in the test-suite

✔️ Corresponding jobs for the base commit e2b0a78 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-coqprime, ci-corn, ci-flocq
  • 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-trakt (because base job at e2b0a78 failed)

@ejgallego
Copy link
Contributor

ejgallego commented Jul 20, 2025

Previous attempt at #9174

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Jul 21, 2025

@coqbot run full ci

SkySkimmer added a commit to SkySkimmer/vsrocq that referenced this pull request Jul 21, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#20917 (changed with_end_tac arg in comtactic)
2449e04
SkySkimmer added a commit to SkySkimmer/rocq-lsp that referenced this pull request Jul 21, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst)
5c148f6
SkySkimmer added a commit to SkySkimmer/coq-tactician that referenced this pull request Jul 21, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst)
79ff02b
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Jul 21, 2025
@SkySkimmer SkySkimmer added this to the 9.2+rc1 milestone Jul 21, 2025
@SkySkimmer
Deprecate "end tac" ("...")
36b70cc 
NB: par ignored the with_end_tac flag so I removed the parsing support
for it.
@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 21, 2025
@proux01 proux01 added the kind: deprecation Deprecation label Jul 28, 2025
@proux01
Copy link
Contributor

proux01 commented Jul 28, 2025

@coqbot merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 28, 2025

@proux01: You cannot merge this PR because:

  • You are not among the assignees.

@proux01 proux01 self-assigned this Jul 28, 2025
@proux01
Copy link
Contributor

proux01 commented Jul 28, 2025

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d88426d into rocq-prover:master Jul 28, 2025
7 checks passed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 28, 2025

@proux01: Please take care of the following overlays:

  • 20917-SkySkimmer-depr-dots.sh

proux01 added a commit to rocq-prover/vsrocq that referenced this pull request Jul 28, 2025
@proux01
Merge pull request #1135 from SkySkimmer/depr-dots
4f791da 
Adapt to rocq-prover/rocq#20917 (changed with_end_tac arg in comtactic)
SkySkimmer added a commit to SkySkimmer/rocq-lsp that referenced this pull request Jul 28, 2025
@SkySkimmer
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst)
af83bf4
SkySkimmer added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 28, 2025
@SkySkimmer
Merge pull request #997 from SkySkimmer/depr-dots
d657899 
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst)
LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Jul 28, 2025
@LasseBlaauwbroek
Merge pull request #107 from SkySkimmer/depr-dots
e7949eb 
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst)
ejgallego added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 29, 2025
@ejgallego
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
a7365f1 
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917
@ejgallego ejgallego mentioned this pull request Jul 29, 2025
Merged
ejgallego added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 29, 2025
@ejgallego
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
e7941ca 
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917

We still keep our stdlib overlay due to
rocq-prover/stdlib#201
ejgallego added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 29, 2025
@ejgallego
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
eacc204 
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917

We still keep our stdlib overlay due to
rocq-prover/stdlib#201
ejgallego added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 29, 2025
@ejgallego
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
1d0f3e0 
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917

We still keep our stdlib overlay due to
rocq-prover/stdlib#201
ejgallego added a commit to rocq-community/rocq-lsp that referenced this pull request Jul 29, 2025
@ejgallego
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
21f897c 
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917

We still keep our stdlib overlay due to
rocq-prover/stdlib#201
@SkySkimmer SkySkimmer deleted the depr-dots branch September 1, 2025 12:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@proux01 proux01 proux01 left review comments

@gares gares gares approved these changes

Assignees

@proux01 proux01

Labels

kind: deprecation Deprecation

Projects

None yet

Milestone

9.2+rc1

Development

Successfully merging this pull request may close these issues.

Is "Proof with <tactic>" worth keeping?

4 participants

@SkySkimmer @ejgallego @proux01 @gares