theories: #518 core slice — fully_intersected_host + named side condi… #1457
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
| name: Build and publish oracle_bin | |
| # Build the standalone `oracle_bin` (the RocqRefRunner used by | |
| # NetTopologySuite.Curve's differential-test harness) and publish it as a | |
| # GHA artifact on every push to main. On release events the same binary | |
| # is attached to the release as a downloadable asset, giving .Curve's CI | |
| # a stable URL to consume. | |
| # | |
| # Toolchain pin: reuses the project's Dockerfile `toolchain` stage | |
| # (rocq 9.2.0 + ocaml 4.14.2-flambda + coq-flocq.4.2.2 + ocamlfind), | |
| # pulled from GHCR under its Dockerfile-hash tag (published by ci.yml on | |
| # main pushes) with a buildx + GHA-layer-cache fallback on a miss, so | |
| # the slow `opam install coq-flocq.4.2.2` step is not repeated. | |
| # | |
| # SPEED (June 2026): PULL REQUESTS reuse the incremental corpus cache | |
| # that ci.yml maintains (.vo artefacts + sha256 manifest; | |
| # scripts/ci_invalidate_stale_vo.py makes make's mtime logic sound | |
| # against it by content). This job is a STRICTLY READ-ONLY cache | |
| # consumer: it never saves the cache and never writes the manifest, | |
| # because it does not run the axiom audit or refresh the .palog/ | |
| # chunks -- a cache saved here could pair a fresh manifest with stale | |
| # Print Assumptions chunks and silently weaken ci.yml's guardrail 4. | |
| # Main pushes and release events skip the restore entirely: the | |
| # PUBLISHED oracle_bin always comes from a full from-clean build. | |
| # `Validate_binary64_extract.v` (a leaf: nothing imports it) is touched | |
| # after the invalidation pass so the extraction always re-runs and | |
| # oracle/extracted.ml is always regenerated fresh. | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'oracle/**' | |
| - 'theories-flocq/**' | |
| - '_CoqProject.full' | |
| - 'Dockerfile' | |
| - '.github/workflows/build-oracle.yml' | |
| # Gate `oracle/driver.ml` (the RocqRefRunner sources) on PRs into main. | |
| # Without this trigger the oracle is only compiled AFTER merge to main: | |
| # ci.yml never runs `make -C oracle/`, so a syntax/type error in a new | |
| # driver mode (e.g. CLOTHOID_INTERSECT) would otherwise reach main | |
| # unvalidated. Same `paths:` filter as the push trigger keeps the slow | |
| # container build off PRs that don't touch the oracle/flocq corpus. | |
| pull_request: | |
| branches: [main] | |
| paths: | |
| - 'oracle/**' | |
| - 'theories-flocq/**' | |
| - '_CoqProject.full' | |
| - 'Dockerfile' | |
| - '.github/workflows/build-oracle.yml' | |
| workflow_dispatch: | |
| release: | |
| types: [published] | |
| # Opt into Node.js 24 for JavaScript actions (actions/checkout, | |
| # actions/upload-artifact, docker/* actions etc.). GitHub Actions | |
| # deprecated the Node.js 20 runtime on 2025-09-19 and forces Node.js 24 | |
| # as the default on 2026-06-02; setting this flag now silences the | |
| # transitional deprecation warning and verifies the workflow runs | |
| # cleanly on the new runtime before the cutover. See | |
| # https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/ | |
| env: | |
| FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true" | |
| jobs: | |
| build-oracle: | |
| name: Build oracle_bin in pinned rocq 9.2.0 + flocq 4.2.2 container | |
| # Skip standalone-package releases (robust-predicates-v* / spatial-algebra-v*): | |
| # those are published by the package-*.yml workflows and have nothing to do | |
| # with oracle_bin. Without this guard, every package release triggers this | |
| # job and its release-attach step fails ("Resource not accessible by | |
| # integration" -- this job only has contents: read), reding the release. | |
| if: >- | |
| github.event_name != 'release' || | |
| (!startsWith(github.event.release.tag_name, 'robust-predicates-v') && | |
| !startsWith(github.event.release.tag_name, 'spatial-algebra-v')) | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| packages: read | |
| env: | |
| TOOLCHAIN_IMAGE: ghcr.io/${{ github.repository_owner }}/nts-proofs-toolchain | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Compute toolchain tag (content-addressed by Dockerfile) | |
| id: toolchain | |
| run: echo "tag=df-$(sha256sum Dockerfile | cut -c1-16)" >> "$GITHUB_OUTPUT" | |
| - name: Log in to GHCR | |
| continue-on-error: true | |
| uses: docker/login-action@v3 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.actor }} | |
| password: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Pull toolchain image from GHCR | |
| # Publishing is ci.yml's job (it runs on EVERY main push); this | |
| # workflow only consumes the tag, with a local build fallback. | |
| id: pull | |
| run: | | |
| if docker pull "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"; then | |
| docker tag "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" nts-proofs-oracle:ci | |
| echo "hit=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "hit=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Set up Docker Buildx | |
| if: steps.pull.outputs.hit != 'true' | |
| uses: docker/setup-buildx-action@v3 | |
| - name: Build toolchain image (GHCR miss) | |
| # Only when the Dockerfile changed (or the tag was never | |
| # published). The GHA layer cache is shared with ci.yml's | |
| # `rocq-flocq` job, so the slow `opam install coq-flocq.4.2.2` | |
| # step (~5 min cold) is not repeated. | |
| if: steps.pull.outputs.hit != 'true' | |
| uses: docker/build-push-action@v6 | |
| with: | |
| context: . | |
| target: toolchain | |
| load: true | |
| tags: nts-proofs-oracle:ci | |
| cache-from: type=gha | |
| cache-to: type=gha,mode=max | |
| - name: Restore compiled-corpus cache (PRs only) | |
| # READ-ONLY reuse of the cache ci.yml maintains. Main pushes | |
| # and releases skip this: the published oracle_bin is always | |
| # built from clean (artifact provenance). See the header | |
| # comment for why this job must never SAVE the cache. | |
| if: github.event_name == 'pull_request' | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| theories/*.vo* | |
| theories/*.glob | |
| theories/.*.aux | |
| theories-flocq/*.vo* | |
| theories-flocq/*.glob | |
| theories-flocq/.*.aux | |
| .palog | |
| .vo-manifest | |
| key: vo-cache-${{ hashFiles('Dockerfile') }}-${{ github.run_id }} | |
| restore-keys: | | |
| vo-cache-${{ hashFiles('Dockerfile') }}- | |
| - name: Invalidate stale artefacts (content-addressed) | |
| # Same script as ci.yml: ages unchanged .v files / touches | |
| # changed ones by sha256 so make rebuilds exactly the changed | |
| # files plus dependents. No-op on a cold cache. | |
| run: python3 scripts/ci_invalidate_stale_vo.py | |
| - name: Force extraction freshness | |
| # Validate_binary64_extract.v is a leaf (nothing imports it); | |
| # touching it AFTER the invalidation pass guarantees the | |
| # extraction target always re-runs, so oracle/extracted.ml and | |
| # .mli are regenerated from the (cached or rebuilt) dependency | |
| # chain on every run. extracted.ml is gitignored -- it never | |
| # exists before the build. | |
| run: touch theories-flocq/Validate_binary64_extract.v | |
| - name: Build corpus, extract, link oracle_bin | |
| # Inside the pinned container, on the MOUNTED live checkout | |
| # (cached .vo files are visible to make; oracle_bin lands | |
| # directly in the runner workspace -- no docker cp dance): | |
| # 1. Clean host-leaked makefile artefacts (NOT .vo -- those | |
| # are the incremental cache). | |
| # 2. rocq makefile -f _CoqProject.full -o Makefile.gen. | |
| # 3. make -- rebuilds changed files + dependents + the touched | |
| # extraction leaf, which writes oracle/extracted.ml + .mli. | |
| # 4. make -C oracle/ -- links extracted.cmx + driver.cmx | |
| # against -package str (ocamlfind is baked into the | |
| # toolchain image). | |
| # chmod lets the image's `rocq` user (uid 1000) write into | |
| # runner-owned dirs; the chown hands the artefacts back. | |
| run: | | |
| chmod -R a+rwX . | |
| docker run --rm -v "$PWD:/workspace" -w /workspace \ | |
| nts-proofs-oracle:ci \ | |
| bash -lc ' | |
| set -euxo pipefail | |
| rm -f Makefile.gen Makefile.gen.conf .Makefile.d .Makefile.gen.d \ | |
| .nra.cache | |
| rocq makefile -f _CoqProject.full -o Makefile.gen | |
| make -f Makefile.gen -j"$(nproc)" | |
| test -f oracle/extracted.ml | |
| test -f oracle/extracted.mli | |
| make -C oracle/ | |
| test -x oracle/oracle_bin | |
| make -C oracle/ ffi | |
| test -f oracle/libntsrocq.so | |
| test -x oracle/ffi_probe | |
| ' | |
| sudo chown -R "$(id -u):$(id -g)" . | |
| - name: Sanity check artifact | |
| run: | | |
| test -x oracle/oracle_bin | |
| file oracle/oracle_bin | |
| ls -la oracle/oracle_bin | |
| test -f oracle/libntsrocq.so | |
| file oracle/libntsrocq.so | |
| ls -la oracle/libntsrocq.so | |
| - name: FFI parity gate (libntsrocq == oracle_bin, bit for bit) | |
| # Phase 5: the in-process C ABI and the stdin/stdout oracle protocol | |
| # call the SAME extracted code, so any divergence is a marshalling bug | |
| # (argument order, enum encoding, truncated result list). Doubles are | |
| # compared as raw IEEE 754 bit patterns. Nonzero exit on any '!!'. | |
| run: | | |
| docker run --rm -v "$PWD:/workspace" -w /workspace \ | |
| nts-proofs-oracle:ci \ | |
| bash -lc ' | |
| set -euxo pipefail | |
| python3 oracle/gen_ffi_parity_tests.py | |
| ' | |
| - name: Run oracle gated-invariant tests | |
| # Runs each oracle test generator that gates proven invariants. | |
| # oracle/oracle_bin was just built and is at the expected path. | |
| # Nonzero exit on any '!!' invariant violation fails the build. | |
| run: | | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_winding_number_tests.py \ | |
| > oracle/winding_number_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_disc_overlay_tests.py \ | |
| > oracle/disc_overlay_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_lec_circle_tests.py \ | |
| > oracle/lec_circle_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_obstacle_distance_tests.py \ | |
| > oracle/obstacle_distance_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_arc_distance_tests.py \ | |
| > oracle/arc_distance_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_i_circular_tests.py \ | |
| > oracle/i_circular_tests.txt | |
| ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_ieee_oracle_bridge_tests.py \ | |
| > oracle/ieee_oracle_bridge_run.txt | |
| - name: Upload oracle_bin artifact (90-day retention) | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: oracle-bin-linux | |
| path: oracle/oracle_bin | |
| retention-days: 90 | |
| - name: Upload libntsrocq artifact (90-day retention) | |
| # Phase 5: the in-process native library + its ABI header, so the | |
| # NetTopologySuite.Curve consumer can bind it without rebuilding the | |
| # corpus. Linux x64 only for now (the runner's architecture). | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: libntsrocq-linux-x64 | |
| path: | | |
| oracle/libntsrocq.so | |
| oracle/nts_ffi.h | |
| retention-days: 90 | |
| - name: Attach oracle_bin to release (release events only) | |
| if: github.event_name == 'release' | |
| uses: softprops/action-gh-release@v2 | |
| with: | |
| files: | | |
| oracle/oracle_bin | |
| oracle/libntsrocq.so | |
| oracle/nts_ffi.h |