From b0903abd3f43343becd2dafb57f2fe37c6dd9135 Mon Sep 17 00:00:00 2001 From: cedretaber Date: Thu, 2 Jul 2026 21:00:22 +0900 Subject: [PATCH 1/2] Remove upstream-only GitHub workflows from fork MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- .github/workflows/check-conflicts.yml | 18 ------------------ .github/workflows/stale.yml | 19 ------------------- 2 files changed, 37 deletions(-) delete mode 100644 .github/workflows/check-conflicts.yml delete mode 100644 .github/workflows/stale.yml diff --git a/.github/workflows/check-conflicts.yml b/.github/workflows/check-conflicts.yml deleted file mode 100644 index 8b0de4c01515..000000000000 --- a/.github/workflows/check-conflicts.yml +++ /dev/null @@ -1,18 +0,0 @@ -name: "Check conflicts" -on: [push] -# Only on push because @coqbot already takes care of checking for -# conflicts when PRs are opened or synchronized - -permissions: - contents: read - -jobs: - main: - permissions: - pull-requests: write - runs-on: ubuntu-latest - steps: - - uses: eps1lon/actions-label-merge-conflict@b8bf8341285ec9a4567d4318ba474fee998a6919 - with: - dirtyLabel: "needs: rebase" - repoToken: "${{ secrets.GITHUB_TOKEN }}" diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml deleted file mode 100644 index aae73dddba36..000000000000 --- a/.github/workflows/stale.yml +++ /dev/null @@ -1,19 +0,0 @@ -name: Stale PRs - -on: - schedule: - # Every workday at 2am - - cron: '0 2 * * 1-5' - -permissions: - contents: read - -jobs: - stale_prs: - # Do not run on forks (we want this request to happen only once every night) - permissions: - contents: none - if: github.repository_owner == 'rocq-prover' - runs-on: ubuntu-latest - steps: - - run: curl -d "rocq-prover:rocq:${{ secrets.DAILY_SCHEDULE_SECRET }}" https://coqbot.herokuapp.com/check-stale-pr From 0e158a178cf9c654974300ead38e8f7547db2244 Mon Sep 17 00:00:00 2001 From: cedretaber Date: Thu, 2 Jul 2026 21:47:40 +0900 Subject: [PATCH 2/2] CI: make the workflow green for this fork 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 7d09774aa ("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) --- .github/workflows/ci-github.yml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/.github/workflows/ci-github.yml b/.github/workflows/ci-github.yml index 33d0319a0b98..468f14874b53 100644 --- a/.github/workflows/ci-github.yml +++ b/.github/workflows/ci-github.yml @@ -21,15 +21,9 @@ jobs: test_disabled: # We exclude the coq-core package packages: ./coqide-server.opam ./rocq*.opam - - name: Windows - os: windows-latest - ocaml: 4.14 - test_disabled: misc coq-makefile precomputed-time-tests - # we don't support rocqide on Windows yet, so we filter it, see #20631 - packages: ./coqide-server.opam ./rocq-*.opam - name: Linux (latest OCaml) os: ubuntu-latest - ocaml: 5 + ocaml: 5.4 test_disabled: packages: ./coqide-server.opam ./rocq*.opam fail-fast: false