tools: .NET hunter for SqlMmExampleFactory vs C# WktIntakeWalker μ #2150
Workflow file for this run
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 proofs | |
| # For CI / Quality Gatekeeper (formerly CI Cara): see docs/HELP.md + docs/READING-GUIDE.md (Quality Gatekeeper card) | |
| # for the full path. The registries and scripts/check_* are the core. | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| workflow_dispatch: | |
| # Opt into Node.js 24 for JavaScript actions (actions/checkout, | |
| # 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: | |
| guards: | |
| # Build-INDEPENDENT corpus guardrails, split into their own job so | |
| # registry / doc / allowlist drift fails in ~seconds and IN PARALLEL | |
| # with the proof builds, instead of gating behind the multi-minute | |
| # macOS `theories/` compile (where these used to run as trailing | |
| # steps). Every script here is pure grep/perl/python and scans the | |
| # SOURCE tree (both theories/ and theories-flocq/), so it needs no | |
| # `.vo` and no `rocq`. Reproduce locally with `make ci-guards`. | |
| name: Corpus guardrails (build-independent) | |
| runs-on: ubuntu-latest | |
| # Pure grep/perl/python; seconds in practice. A low ceiling turns a hung | |
| # script into a fast, clear failure instead of a 6h default-timeout stall. | |
| timeout-minutes: 10 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Run all corpus guardrails (make ci-guards) | |
| # Covers, in one fast pass (see the per-script headers for detail): | |
| # check_admitted two-tier Admitted registry | |
| # check_readme_axioms README <-> axiom-allowlist sync | |
| # check_deferred_registry_sync doc <-> Admitted-registry drift | |
| # validate-claims verified-claims.md references resolve | |
| # check_oracle_handrolled hand-rolled float-kernel ratchet | |
| # hunt.py --selfcheck RELATE_MATRIX token allowlist (no oracle) | |
| # The macOS `rocq` job below no longer repeats these — this job is | |
| # the single source of the guardrail verdict on every PR and push. | |
| run: make ci-guards | |
| rocq: | |
| name: Build with Rocq ${{ matrix.rocq-version }} | |
| # Gate the (slow, paid-runner) build on the fast guardrails: a | |
| # registry/doc/allowlist failure skips this job entirely instead of | |
| # burning a full macOS compile, and keeps the guardrail verdict a | |
| # hard prerequisite of this build even though it now lives in its own | |
| # job (so branch protection on this build still implies guards pass). | |
| needs: guards | |
| runs-on: macos-latest | |
| # A full theories/ build is well under this; the ceiling caps a runaway. | |
| timeout-minutes: 60 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| rocq-version: ['9.2.0'] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Install Rocq via Homebrew | |
| # Bottled install ~30s; caching the Cellar misses Homebrew's | |
| # config files under /opt/homebrew/etc/, which breaks ocamlfind. | |
| # Easier to install fresh each run. | |
| run: brew install rocq | |
| - name: Show Rocq version | |
| id: rocqv | |
| # Capture the ACTUAL installed version: `brew install rocq` is | |
| # unpinned, so the .vo cache key must track what Homebrew shipped | |
| # (not the cosmetic matrix string) or a compiler bump would try to | |
| # load version-incompatible cached .vo. | |
| run: | | |
| rocq -v | |
| echo "ver=$(rocq --version | head -1 | tr -cd '[:alnum:].-')" >> "$GITHUB_OUTPUT" | |
| - name: Restore theories/ .vo cache (PRs only) | |
| # PR == "theories-quick": restore the previous run's .vo + manifest so | |
| # only changed files + dependents recompile. Pushes to main skip this | |
| # and build "theories-full" from clean, re-seeding the cache — the | |
| # integrity anchor (every merge revalidates the whole lane). | |
| if: github.event_name == 'pull_request' | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| theories/*.vo* | |
| theories/*.glob | |
| theories/.*.aux | |
| .vo-manifest-theories | |
| key: theories-vo-${{ steps.rocqv.outputs.ver }}-${{ github.run_id }} | |
| restore-keys: | | |
| theories-vo-${{ steps.rocqv.outputs.ver }}- | |
| - name: Generate Makefile (parity with container + docs) | |
| # Use the same modern driver + .gen naming as the container job, | |
| # Dockerfile, README, and the committed convenience Makefile. | |
| # Never write to plain "Makefile" — that is the safe committed | |
| # convenience layer (make help, make host, etc.). | |
| run: rocq makefile -f _CoqProject -o Makefile.gen | |
| - name: Invalidate stale artefacts (content-addressed, theories/ lane) | |
| # Same content-addressed pass as the flocq job, pointed at the | |
| # Stdlib-only project + its own manifest: ages unchanged .v so make | |
| # skips them, touches changed/new ones so make rebuilds them + their | |
| # dependents. No-op on a cold cache (main, or first PR run). | |
| run: | | |
| CI_VO_PROJECT=_CoqProject CI_VO_MANIFEST=.vo-manifest-theories \ | |
| python3 scripts/ci_invalidate_stale_vo.py | |
| - name: Build proofs | |
| # Parallel + output-sync for readable logs (matches container job). | |
| # This job now does exactly one thing — compile the Stdlib-only | |
| # `theories/` lane end to end. The build-independent guardrails | |
| # run separately in the `guards` job above (fast, parallel), and | |
| # the Admitted scan there covers this lane's sources too. | |
| run: make -f Makefile.gen -j"$(sysctl -n hw.ncpu)" --output-sync=target || make -f Makefile.gen -j"$(sysctl -n hw.ncpu)" | |
| - name: Refresh theories/ manifest | |
| # Only reached when the build passed: records the content hash of every | |
| # host-lane .v so the next PR run's invalidation is sound. | |
| run: | | |
| CI_VO_PROJECT=_CoqProject CI_VO_MANIFEST=.vo-manifest-theories \ | |
| python3 scripts/ci_write_vo_manifest.py | |
| - name: Save theories/ .vo cache | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: | | |
| theories/*.vo* | |
| theories/*.glob | |
| theories/.*.aux | |
| .vo-manifest-theories | |
| key: theories-vo-${{ steps.rocqv.outputs.ver }}-${{ github.run_id }} | |
| rocq-flocq: | |
| # Container-based build of the Flocq-dependent corpus | |
| # (`theories-flocq/`). The host-runner `rocq` job above only builds | |
| # `theories/` -- it grep-scans `theories-flocq/` for the corpus | |
| # invariant but does not compile those files. This job closes that | |
| # gap using the project's pinned toolchain (Rocq 9.2.0 + opam | |
| # `coq-flocq.4.2.2`, see Dockerfile) to build `_CoqProject.full`. | |
| # | |
| # SPEED ARCHITECTURE (June 2026): | |
| # | |
| # - The toolchain image (Dockerfile `--target toolchain`, no | |
| # sources baked in) is published to GHCR under a tag derived | |
| # from the Dockerfile's hash; runs pull it (~seconds) instead of | |
| # reassembling layers from the buildx cache. A miss (new | |
| # Dockerfile) falls back to building it, and main pushes publish | |
| # the new tag. | |
| # - PULL REQUESTS build INCREMENTALLY: .vo artefacts, per-file | |
| # Print Assumptions chunks (.palog/), and a content manifest are | |
| # cached; scripts/ci_invalidate_stale_vo.py ages unchanged .v | |
| # files and touches changed/new ones (sha256-based -- immune to | |
| # rebase-backdated commit times), so make rebuilds exactly the | |
| # changed files plus their dependents. | |
| # - MAIN PUSHES always build from clean (the restore step is | |
| # skipped): every merge re-validates the whole corpus end to end | |
| # and re-seeds the cache. | |
| # | |
| # GUARDRAIL-4 SOUNDNESS UNDER INCREMENTALITY: the audit no longer | |
| # reads the raw build log (an incremental log only covers rebuilt | |
| # files). Instead, the output-synced log -- each target's `ROCQ | |
| # compile <file>` line plus its `Print Assumptions` blocks emitted | |
| # atomically -- is split into per-file chunks cached alongside the | |
| # .vo they were compiled with (same provenance). The audit runs on | |
| # the assembled chunks of EVERY project file, and a missing chunk | |
| # FAILS the build (scripts/ci_assemble_palog.sh), so coverage can | |
| # never silently shrink. History: the May 2026 axiom-leak | |
| # investigation showed plain parallel logs interleave; output-sync | |
| # removes that at the root (the old -j1 rebuild is gone). | |
| name: Build theories-flocq in pinned container | |
| # Same fast-fail gate as the `rocq` job: don't spin up the container | |
| # build (toolchain pull + incremental corpus compile + axiom audit) | |
| # when a build-independent guardrail already failed. | |
| needs: guards | |
| runs-on: ubuntu-latest | |
| # Cold path (toolchain build + full corpus + audit) fits comfortably; | |
| # the ceiling turns a hang into a clear failure well before GitHub's 6h. | |
| timeout-minutes: 90 | |
| permissions: | |
| contents: read | |
| packages: write | |
| 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 | |
| id: pull | |
| run: | | |
| if docker pull "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}"; then | |
| docker tag "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" nts-proofs-flocq: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 buildx GHA layer cache still shortcuts the | |
| # slow `opam install coq-flocq.4.2.2` step (~5 min cold). | |
| if: steps.pull.outputs.hit != 'true' | |
| uses: docker/build-push-action@v6 | |
| with: | |
| context: . | |
| target: toolchain | |
| load: true | |
| tags: nts-proofs-flocq:ci | |
| cache-from: type=gha | |
| cache-to: type=gha,mode=max | |
| - name: Publish toolchain image (main only) | |
| # Content-addressed tag: republishing only happens when the | |
| # Dockerfile actually changed. PRs that change the Dockerfile | |
| # build locally; the tag is published on merge. | |
| if: steps.pull.outputs.hit != 'true' && github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| run: | | |
| docker tag nts-proofs-flocq:ci "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" | |
| docker push "$TOOLCHAIN_IMAGE:${{ steps.toolchain.outputs.tag }}" | |
| - name: Restore compiled-corpus cache (PRs only) | |
| # Main pushes skip this on purpose: every merge rebuilds the | |
| # corpus from clean and re-seeds the cache (integrity anchor). | |
| 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) | |
| # Ages unchanged .v files / touches changed ones so make's | |
| # mtime logic agrees with actual content; wipes everything if | |
| # the _CoqProject.full flag lines changed; prunes artefacts and | |
| # chunks of files that left the project. No-op on a cold cache. | |
| run: python3 scripts/ci_invalidate_stale_vo.py | |
| - name: Compile corpus (mounted workspace, output-synced) | |
| # The live checkout is mounted over the image's /workspace, so | |
| # cached .vo files are visible to make and new artefacts land on | |
| # the runner for the cache-save step. chmod lets the image's | |
| # `rocq` user (uid 1000) write into runner-owned dirs; the chown | |
| # afterwards hands the artefacts back to the runner user. | |
| run: | | |
| chmod -R a+rwX . | |
| docker run --rm -v "$PWD:/workspace" -w /workspace \ | |
| nts-proofs-flocq:ci \ | |
| bash -lc ' | |
| 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)" --output-sync=target | |
| ' > /tmp/build_sync.log 2>&1 || { | |
| echo "::error::Corpus build failed; see /tmp/build_sync.log" | |
| grep -nE 'Error:|File "\./theories|Cannot find witness|Unable to unify|No primitive equality' \ | |
| /tmp/build_sync.log | head -80 || true | |
| echo "----- tail -----" | |
| tail -80 /tmp/build_sync.log | |
| exit 1 | |
| } | |
| sudo chown -R "$(id -u):$(id -g)" . | |
| - name: Smoke hunt probes (docs/h1-vacuity) | |
| # Qed-claiming hunt probes live next to the H1 pair and are | |
| # evidence, not _CoqProject.full product modules. Compile them | |
| # here so a probe that claims Qed is a checked fact (Print | |
| # Assumptions lands in this step's log). | |
| run: | | |
| set -o pipefail | |
| chmod -R a+rwX . | |
| docker run --rm -v "$PWD:/workspace" -w /workspace \ | |
| nts-proofs-flocq:ci \ | |
| bash -lc 'bash scripts/hunt_probe_smoke.sh' \ | |
| | tee /tmp/hunt_probe_smoke.log | |
| sudo chown -R "$(id -u):$(id -g)" . | |
| - name: Update per-file Print Assumptions chunks | |
| run: bash scripts/ci_update_palog.sh /tmp/build_sync.log | |
| - name: Per-theorem axiom audit on full-corpus chunk assembly (guardrails 1 + 4) | |
| # scripts/ci_assemble_palog.sh fails hard if ANY project file | |
| # lacks a chunk -- audit coverage cannot silently shrink. The | |
| # audit enforces docs/axiom-allowlist.txt against every | |
| # per-theorem PA block, with file-level exemptions from | |
| # docs/audit-exceptions.txt. | |
| run: | | |
| bash scripts/ci_assemble_palog.sh > /tmp/audit_input.log | |
| # Hunt probes are off _CoqProject.full; their smoke PA must | |
| # still hit the allowlist / audit-exceptions gate. | |
| cat /tmp/hunt_probe_smoke.log >> /tmp/audit_input.log | |
| bash scripts/audit_axioms.sh /tmp/audit_input.log | |
| - name: Refresh corpus manifest | |
| # Only reached when build + audit passed: the manifest never | |
| # blesses artefacts that failed the gauntlet. | |
| run: python3 scripts/ci_write_vo_manifest.py | |
| - name: Save compiled-corpus cache | |
| uses: actions/cache/save@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 }} |