Remove upstream-only GitHub workflows from fork#10
Merged
Conversation
This fork exists for Java extraction development, but two workflows were
inherited from upstream Rocq and serve no purpose here:
- check-conflicts.yml: runs on every push to label conflicting PRs
("needs: rebase") — upstream PR-flow automation irrelevant to this fork,
and it consumes Actions minutes on each push.
- stale.yml: guarded by `github.repository_owner == 'rocq-prover'`, so it
is already inert on this fork; removed for tidiness.
ci-github.yml is kept: it builds Rocq and runs the test-suite, which now
includes the Java extraction scripted tests (misc/java-extraction.sh).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Two pre-existing failures surfaced once CI was enabled on the fork; neither is related to the Java extraction work. Both are fixed by matching upstream (rocq-prover/rocq) rather than suppressing symptoms. - Linux `output/` extraction tests (EmptyExtraction.v, bug7348.v) failed because OCaml 5.5 makes ocamlfind print "[WARNING] Cannot read directory ../stublibs which is mentioned in ld.conf" during `Extraction TestCompile`, and that stderr line leaks into the captured test output, which is diffed verbatim against the .out fixtures. This is exactly the issue upstream fixed in 7d09774 ("github actions linux job use ocaml 5.4 to avoid warning with 5.5"): our `ocaml: 5` resolves to 5.5. Pin the Linux job to `ocaml: 5.4` to match upstream and avoid the warning at the source (no test-suite filter needed). - Windows job failed at the Build step with "Extension coq was deleted in the 3.24 version of the dune language". Upstream's Windows job passes because upstream master has migrated off the deprecated dune `coq` extension; this fork predates that migration. Windows also disables the `misc` subsystem, so it never runs the Java extraction tests. Drop the Windows matrix entry rather than backport the dune migration; this fork targets Java extraction on Linux/macOS. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
cedretaber
force-pushed
the
chore/remove-upstream-workflows
branch
from
July 2, 2026 13:03
58b838c to
0e158a1
Compare
cedretaber
commented
Jul 2, 2026
| - name: Linux (latest OCaml) | ||
| os: ubuntu-latest | ||
| ocaml: 5 | ||
| ocaml: 5.4 |
Author
There was a problem hiding this comment.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
目的
この fork は Java extraction 開発のためのものですが、上流 Rocq から継承した2つの GitHub Actions ワークフローがこの fork では不要なため削除します。
変更内容
check-conflicts.ymlon: [push]で毎 push 起動し、コンフリクトした PR にneeds: rebaseラベルを付ける上流の PR 運用自動化。この fork には無関係で、毎 push に Actions 分を消費する。stale.ymlif: github.repository_owner == 'rocq-prover'でガードされており、この fork(owner = proof-ninja)では既に不活性。掃除のため削除。ci-github.ymlは残します — Rocq をビルドして test-suite を実行し、その中に Java extraction の scripted test(misc/java-extraction.sh)が含まれるためです。確認
この PR の push で
ci-github.ymlが起動し、macOS / Linux ジョブの test-suitemiscサブシステムでjava-extraction.shが実行されることを確認します。削除した2ワークフローは走らないはずです。🤖 Generated with Claude Code