From 841076c56166a3228152af04c3659e52544c6d40 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:22:33 +0000 Subject: [PATCH 1/9] docs: record the #43 check-triage ultraplan and its execution record Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- ULTRAPLAN-ISSUE-43.adoc | 380 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 380 insertions(+) create mode 100644 ULTRAPLAN-ISSUE-43.adoc diff --git a/ULTRAPLAN-ISSUE-43.adoc b/ULTRAPLAN-ISSUE-43.adoc new file mode 100644 index 0000000..cf75235 --- /dev/null +++ b/ULTRAPLAN-ISSUE-43.adoc @@ -0,0 +1,380 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += Ultraplan: close #43 (9 red checks from the citation PR), verify #47, and mop up the recon findings +:toc: +:toclevels: 3 + +== 0. Scope and authority + +*Primary issue:* ] — +_Triage: 9 red checks surfaced by the citation PR #41_ (open, `research`). +Its standing rule: a red check is *an issue with acceptance criteria, never a +merge blocker*, and each check must end up *fixed*, *retired*, or *accepted +with a documented exemption* — "it may not stay undetermined". + +*Secondary issue:* ] — the 12 test +failures (closed 2026-10-09 via PR #49). Included here only to *verify* its +acceptance criteria actually hold after the fix landed. + +*Binding estate content this plan follows* (all read during recon): + +[cols="2,3,3",options="header"] +|=== +| Source | What it binds | Key rule used here + +| `standards/0-canon/RSR-PHILOSOPHY.adoc` +| the stopping rule +| "A new scanner finding surfaced at a boundary remains an issue with + acceptance criteria, never a blocker on stopping." Working state = default + branch green and the thing runs. + +| `standards` ] (and the #43 body) +| triage determinations +| For every red: one determination — *fix* / *retire the gate* / *accept with + a documented exemption*. "Repair or retire; never mute." No `continue-on-error`, + no demotion to warning, no silent required-set drops. + +| `standards/docs/CICD-SIGNAL-DISCIPLINE.adoc` +| check naming, renames, required contexts +| Rename checks only via the safe sequence; a required context nothing emits is + a *phantom*; required contexts are *derived, never typed* + (`standards/config/rulesets/gates.json`). + +| `standards/3-practice/TOOLING-VERSION-INTEGRITY-POLICY.adoc` +| soft gates and pin integrity +| R4: every `continue-on-error` carries a `GATE DEACTIVATED …` or + `by-design:`/`advisory:` comment; a green/red bit cannot distinguish + "passed" from "never ran" — prove execution. (This is exactly the #43 + failure class.) + +| `standards/docs/EXEMPTION-MECHANISMS.adoc` +| what an exemption is +| Exemption ≠ debt; documented excuses live in `.hypatia-baseline.json` / + Debtfile per the decision tree; *no per-PR exemptions exist*; never invent + suppression conventions. + +| `standards/docs/ISSUE-INTAKE-SPEC.adoc` +| how follow-up findings are filed +| Scope labels mandatory; dedupe; *a wave of > 5 findings opens exactly one + `meta:campaign` umbrella first*; estate-wide items go to the estate register + or are filed with a `Propagation` section. + +| `standards/docs/DEPENDABOT-POLICY.adoc` (owner ruling D269) +| updates land unattended +| Only when the base branch carries a *required build/test check*; never + `gh pr merge --auto`; `actions.lock` is repaired in the same PR as any + `uses:` change. + +| `rsr-template-repo` +| the scaffold this repo was minted from +| Ships `.github/workflows/actions.lock`; `REQUIRES_INITIALISATION.adoc` must + not be deleted until its tokens are resolved; placeholder vocabulary in + `.machine_readable/ai/PLACEHOLDERS.adoc`. +|=== + +== 1. Recon — ground truth + +=== 1.1 What issue #43 actually is + +All 9 red checks on PR #41 are the CI matrix `test (*)` jobs, and all 9 died at +*setup* on the same line of `.github/workflows/CI.yml`: + +---- +julia-actions/julia-runtest@79a7e100883947123f8263c5f06e6c2fee60dd0c +---- + +That SHA exists in *no upstream ref* of `julia-actions/julia-runtest`. It +shares a 30-hex prefix with the real v1.9.3 +(`79a7e100…c0ea3eb972f`) and then diverges — an orphan/corrupted pin. Every +`test (*)` job therefore *never ran a single test*: this is the +TOOLING-VERSION-INTEGRITY failure class ("a green/red bit cannot distinguish +'passed' from 'never ran'"), not 9 independent test failures. Issue #43's own +text confirms the same 9 were already red on `main` @ `553d49e` (2026-09-20) — +pre-existing, not caused by the citation PR. + +=== 1.2 What has landed since (the fixes are already in the repo) + +[cols="1,2,3",options="header"] +|=== +| PR | Merge commit | What it fixed + +| ] +| `93305d82` +| Matrix arch dimension dropped — setup-julia picks the runner arch (macOS + legs). *This renamed the checks* (see §1.3). + +| ] +| `487c7ab4` +| (a) `math.jl:42` parse error (module loaded at all), (b) duplicate + `FPSort`/`RegLan` structs (precompile rejected), (c) *the pin*: `julia-runtest` + re-pinned to `d0c4f093badade621cd041bba567d1e832480ac2` (tag `v1.10.0`, + resolved via `git ls-remote`). + +| ] +| `14da03a7` +| The 12 test failures tracked by #47, fixed at root cause in `src/` or by + correcting tests that called APIs that never existed (`declare_const` / + `to_smtlib_script` → `declare` / `SMTLib.build_script`). No test skipped, + deleted or loosened. #47 closed. + +| ] / ] +| `126ced1` (current `main` HEAD) +| Release workflow fix; version bump to 0.2.2. +|=== + +*Green evidence on `main` @ `126ced1`* — CI run `37921988068` (2026-10-09): +all 9 matrix legs `success` — + +---- +test (1.10, ubuntu-latest) test (1.11, ubuntu-latest) test (nightly, ubuntu-latest) +test (1.10, macos-latest) test (1.11, macos-latest) test (nightly, macos-latest) +test (1.10, windows-latest) test (1.11, windows-latest) test (nightly, windows-latest) +---- + +No `continue-on-error`, no warning demotion anywhere in `CI.yml` (verified; the +only soft gate in the repo is `boj-build.yml`'s, see §1.5). + +=== 1.3 The naming drift — and why it is harmless here + +The issue names its checks `test (1.10, ubuntu-latest, x64)` etc. Since PR #45 +the arch dimension is gone and the emitted contexts are `test (1.10, +ubuntu-latest)` etc. Per CICD-SIGNAL-DISCIPLINE, a renamed context orphans any +rule requiring the old name. *Checked and clear:* the repo's active rulesets +require exactly one context — `scan / gitleaks` (ruleset "Secret-Scan-Floor"). +Nothing requires the old `x64` names, so the rename created *no phantom +requirements*. This must be stated in the closure record (it is the one +non-obvious fact a future reader needs). + +=== 1.4 Current check board on `main` @ `126ced1` + +*Green* — CI (9/9), Governance (10 jobs incl. Guix/Nix, workflow security, +trusted-base, licence, well-known), CodeQL, Hypatia, Secret Scanner +(gitleaks/rust/shell), OSSF Scorecard, Release side (`Build Package` ×3, +SBOM, Create Release, Dependabot, sync). + +*Red (chronic, push-only — not PR-visible, but red on `main`)*: + +* `Mirror to Git Forges` — all 7 mirror jobs fail at `webfactory/ssh-agent`: + the `*_MIRROR_ENABLED` vars are `true` but the SSH secrets are absent. Failing + on every run back to at least 2026-09-20 (`553d49e`). +* `GitHub Pages` (`casket-pages.yml`) — `build` *cancelled* on every recent run + (cabal build of `casket-ssg` blows through the 15-minute job window), `deploy` + skipped. Effectively chronically broken. + +Per the same standing rule these two reds need determinations of their own — +they must *not* be folded into #43 (different defects; ISSUE-INTAKE-SPEC Rule 2). + +=== 1.5 Adjacent debt found during recon (not #43 scope) + +* `actions.lock` is *absent* (estate canon R2: "present everywhere"; the + template ships one at `.github/workflows/actions.lock`). PR #48's body + already records the absence. +* `boj-build.yml:18` — bare `continue-on-error: true` with no R4 comment + (it is a by-design best-effort trigger, but it must *say* so), and the curl + payload quoting is malformed (`casket\\\"}\"}`). +* `docs/make.jl` still lists `index.md`/`api.md`/`examples.md`/`solvers.md` + while `docs/src/` is `.adoc` (md→adoc migration residue). `casket-pages.yml` + is the live site path. +* `REQUIRES_INITIALISATION.adoc` — one unresolved token + `{{PROJECT_UNIQUE_STRENGTH}}` in + `.machine_readable/bot_directives/methodology.a2ml:58`. +* CI installs *no SMT solver*, against AGENTS.adoc's own guidance ("CI should + install at least one solver"). Consequence: the Z3-gated tests — including + #47's unsat-core fix — skip on every CI leg. +* Tier/conformance drift (cross-cutting): only `scan / gitleaks` is required, + while the canon's GATE set for a Julia repo is governance + secret-scanner + + hypatia + codeql + `julia-ci.yml` (this repo's file is `CI.yml`; no tier + prefixes). Required contexts are *derived by the estate applier, never typed* + — this is `scope:estate` work, related to `standards` #994. +* Trivial: `TEST-NEEDS.adoc` claims "E2E tests 0" though `test/e2e_test.jl` + exists. + +== 2. Phase 1 — close #43 with recorded determinations (the core) + +*Determinations — all 9 checks: FIXED.* (The named contexts are +fixed-and-renamed: successor = same matrix leg without the `, x64` suffix.) +Each of the 18 checkboxes resolves as follows: + +[cols="1,3,3",options="header"] +|=== +| # | Check named in #43 | Determination and evidence + +| 1–3 +| `test (1.10, {ubuntu,macos,windows}-latest, x64)` +| *Fixed*. Pin repinned (PR #48 → `487c7ab4`); suite passes (PR #49 → + `14da03a7`); successor context `test (1.10, )` green on `main` in CI run + `37921988068` (@ `126ced1`). Fix is in the repo; no soft gate, no demotion. + +| 4–6 +| `test (1.11, {ubuntu,macos,windows}-latest, x64)` +| *Fixed* — same evidence, successor `test (1.11, )`. + +| 7–9 +| `test (nightly, {ubuntu,macos,windows}-latest, x64)` +| *Fixed* — same evidence, successor `test (nightly, )`. +|=== + +Second checkbox of each pair ("green on `main`, fix in the repo — not +`continue-on-error`, not a demotion") is satisfied by §1.2/§1.4 and should be +ticked with the same evidence link. + +*Closure procedure (in order):* + +. Post one triage comment on #43 containing: the table above; the pin autopsy + (orphan SHA, 30-hex prefix collision with v1.9.3); the rename map + `test (…, x64)` → `test (…)` plus the no-phantom check ("only `scan / + gitleaks` is required; nothing required the old names"); links to PRs #48, + #49 and CI run `37921988068`. +. Tick all 18 body checkboxes (the "may not stay undetermined" rule). +. Labels before closing (ISSUE-INTAKE-SPEC Rule 5): add `scope:repo` and + `cicd`; keep `research`. Cross-reference `hyperpolymath/standards` #994 as + the cross-cutting home of the pin-orphan class (the repo-level instance is + what is being fixed here). +. Close #43 with that comment as the closing record. + +*Forbidden closure paths* (explicitly ruled out by the issue's own ACs and +standards#994 AC5): `continue-on-error`, demotion to warning, retiring the test +matrix, or an "exemption" — none apply, because the checks are genuinely green +again. + +== 3. Phase 2 — verify #47 is really done (no code) + +Check each #47 acceptance criterion against the merged state, then tick the +boxes in its body for hygiene and leave it closed: + +* `get_statistics` parses `(:key value …)` — fixed in PR #49 item 1. ✔ +* `evaluate` handles `Expr(:&&)`/`Expr(:||)` — fixed in PR #49 item 2. ✔ +* `get_unsat_core` returns named labels (Z3 4.13.3 returns `[:pos, :neg]`) — + fixed in PR #49 item 3. ✔ *(caveat: CI never exercises it — no solver on + PATH; closed by Phase 3 item 7.)* +* `declare_const` decision — resolved: tests call `declare`/`build_script`; + no second API surface added. ✔ +* `Pkg.test()` green on the CI matrix — CI run `37921988068`. ✔ + +== 4. Phase 3 — follow-up wave (new work; umbrella first) + +Seven findings > five ⇒ ISSUE-INTAKE-SPEC Rule 3: open *one* `meta:campaign` +umbrella first ("CI hygiene & estate-conformance top-up — 2026-10-10"), then +one issue per item, each referencing the umbrella: + +. *`[cicd]` Mirror workflow red on `main` since ≤ 2026-09-20* — vars enabled + without SSH secrets; every job fails in `webfactory/ssh-agent`. Determination + owed: *fix* (provision the secrets) or *retire* (clear the `*_MIRROR_ENABLED` + vars / remove the workflow). Record the date it went red. (`📅 PERIODIC`/push + tier — never a PR check; fine as push-only per the canon.) +. *`[cicd]` GitHub Pages chronically cancelled* — diagnose the cabal build + window (cache key / timeout / prebuilt `casket-ssg`), or retire the workflow. + Same determination discipline. +. *`[cicd, conformance]` Adopt `actions.lock`* (canon R2; template ships one) + and the lock-sync discipline: regenerated in the same PR as any `uses:` + change. Fold the regeneration into PR #52 (below) or land it alongside. +. *`[cicd]` R4-compliance for `boj-build.yml`* — add the `by-design:` / + `advisory:` rationale comment above the `continue-on-error`, and fix the + malformed trigger payload quoting. +. *`[docs]` Resolve `docs/make.jl` staleness* — either retire the Documenter + path (casket-pages is the live site builder) or point it at the `.adoc` + sources. Decide which is canonical; do not leave two half-truths. +. *`[conformance]` Fill `{{PROJECT_UNIQUE_STRENGTH}}`* in + `.machine_readable/bot_directives/methodology.a2ml` (draft from the package + purpose; owner confirms), then let the estate top-up pass retire + `REQUIRES_INITIALISATION.adoc` — do *not* delete that file by hand. +. *`[testing, cicd]` Install Z3 on the ubuntu CI legs* (AGENTS.adoc compliance) + so solver-backed tests — including the #47 unsat-core path — actually run; + keep the graceful-skip behaviour documented for legs without a solver. +. *(Optional, `scope:estate` + Propagation section)* GATE-tier conformance: + canonical `julia-ci.yml` naming, `🔴 GATE:`-prefixed job names, and the + derived required-context rollout. Hand-typing required contexts is forbidden; + this coordinates with the estate applier and `standards` #994. + +Fold the trivial `TEST-NEEDS.adoc` refresh into whichever PR fits. + +== 5. Phase 4 — handle open PR #52 (dependabot, 6 action bumps) + +* Per D269 the repo may *not* auto-arm: the only required context is + `scan / gitleaks`, not a build/test check. Merge manually after checks are + green — never `gh pr merge --auto`. +* Before merging, verify every new pin resolves upstream with `git ls-remote` + (julia-runtest `v1.12.0`, codeql-action `v4.38.2`, …). This is literally the + #43 failure class; a dependabot pin that cannot resolve reproduces it. + `julia-runtest 1.10 → 1.12` and `codeql-action 3.x → 4.x` deserve a look at + release notes for behaviour changes, not just SHA validity. +* If Phase 3.3 (`actions.lock`) lands first, regenerate the lock inside #52 — + "regenerated in the same PR as any `uses:` change". + +== 6. Sequencing, stopping points, definition of done + +Sequencing (each step leaves `main` green — "stop at a working state"): + +---- +Phase 1 close #43 with determinations (comment + labels + close) +Phase 2 tick #47 boxes (hygiene) +Phase 3 umbrella issue → 7 follow-up issues (intake Rule 3) +Phase 3' one PR per fixable item, smallest first: + 4 (boj R4 comment, tiny) → 7 (solver in CI) → 5 (docs/make.jl) + → 3 (actions.lock + #52 regen) → 1/2 (mirror & pages determinations) + → 6 (PROJECT_UNIQUE_STRENGTH, owner-confirmed) +Phase 4 verify & merge PR #52 +---- + +*Definition of done for this plan:* + +* #43 closed with 18/18 determinations recorded and evidenced; no mute used. +* #47 verified, boxes ticked. +* Every red on `main` (mirror, Pages) has a determination: fixed, retired, or + accepted with a documented exemption (Debtfile/baseline per + EXEMPTION-MECHANISMS — never invented conventions). +* No bare soft gates; no undetermined red; `actions.lock` present or its + absence tracked by an open issue; #52 merged with verified pins. + +== 7. Evidence appendix + +* `gh issue view 43 --json body` — the 9 checks and 18 checkboxes. +* `gh pr view 48/49/45 --json mergeCommit` — `487c7ab4`, `14da03a7`, `93305d82`. +* `gh run view 37921988068` — 9/9 `test (*)` legs success on `main` @ `126ced1`. +* `gh api repos/hyperpolymath/SMTLib.jl/rules/branches/main` — required + contexts = `scan / gitleaks` only (no phantoms from the rename). +* `gh run list --workflow mirror.yml` — failures back to at least 2026-09-20. +* `grep -rn continue-on-error .github/workflows/` — only `boj-build.yml:18`. +* Pin autopsy: `julia-actions/julia-runtest@79a7e100…c2fee60dd0c` shares a + 30-hex prefix with real v1.9.3 `79a7e100…c0ea3eb972f`; resolved pin + `d0c4f093…` = `v1.10.0` (PR #48 records the `git ls-remote` proof). + +''' + +== 8. Execution record (2026-10-10) + +Executed in this session, with these deviations from the plan above (all forced +by the GitHub integration's permission shape, all recorded): + +* *The Arena integration carries `issues: read`* (verified from the app's own + permission set). Issue *creation* works; commenting, editing bodies, ticking + checkboxes, adding labels and closing do not. Consequences: + ** the #43 determinations live in the closing PR's body (this document is + the long form); the 18 checkboxes in #43's body could not be ticked and + the triage comment could not be posted on the issue itself; + ** issue closure is via the PR's `Closes #…` references (platform + auto-close), not `gh issue close`; + ** labels come from the `label-triage.yml` classifier on `opened` (titles + were written to drive it: `ci:`, `fix:`, `docs:`, `test:` prefixes and + "owner decision needed"); a few classifier inexactitudes remain + (`meta:campaign` intended on the umbrella, classifier applied + `meta:umbrella`; `scope:repo` never applied by the classifier). +* Issue *#54* (`zz-probe-labels`) was a permission probe and *#55* an + empty-bodied mis-create (`body_file` is not an API field); both are retired + via the same PR's `Closes` list. #56 replaces #55. +* Estate-side cross-cutting notes (GATE-tier / required-context derivation, + the pin-orphan class) could not be commented onto `standards` #994 (same + permission shape on that repository); §4 item 8 and §1.3 are the record for + the owner to relay. + +Phases completed: Phase 1 (determinations recorded; #43 closed by the PR), +Phase 2 (verified), Phase 3 (umbrella #53 + findings #55–#62 filed; #58–#62 +fixed in this PR), Phase 4 (PR #52 pin-verified — all 6 SHAs resolve, incl. +annotated-tag peels — and merged before this branch, so the lock below matches +the merged tree). Remaining open: #56 (mirror) and #57 (Pages) await the +owner's fix/retire ruling; umbrella #53 closes when they are determined (its +AC2–AC4). + +_Note on this document: it is the plan and its execution record. Recon clones +of `standards` and `rsr-template-repo` were read from GitHub and live outside +this repository._ From cda05cb3d62b0cbac49594ca68c6b7000bb2c952 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:23:25 +0000 Subject: [PATCH 2/9] fix(ci): install Z3 on the ubuntu CI legs so solver-backed tests run (#62) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit AGENTS.adoc 'CI & Solver Detection' asks CI to install at least one solver on PATH. With none installed, every solver-gated test skipped on all 9 matrix legs — including the Z3 unsat-core path fixed in #49, never exercised in CI. Ubuntu legs now apt-get install z3 (with a z3 --version execution sentinel); macos/windows legs keep the documented graceful-skip behaviour. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/CI.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index cfaefad..07a9d1b 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -19,6 +19,17 @@ jobs: steps: - name: Checkout code uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4 + # AGENTS.adoc "CI & Solver Detection": install at least one solver and + # keep it on PATH so solver-backed tests run instead of skipping. Ubuntu + # legs get Z3; other legs keep the documented graceful-skip behaviour + # (#62). `z3 --version` is the positive execution sentinel. + - name: Install Z3 (ubuntu) + if: runner.os == 'Linux' + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y z3 + z3 --version - name: Setup Julia uses: julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32 # v3.0.2 with: From ce3f3db08f38171f43cb2939ac964a9c4c19bd6e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:23:25 +0000 Subject: [PATCH 3/9] fix(ci): explain the boj-build soft gate and fix the trigger payload (#59) TOOLING-VERSION-INTEGRITY Rule 4: a bare continue-on-error must carry a GATE DEACTIVATED record or a by-design/advisory rationale within 12 lines. This one is a by-design best-effort trigger; it now says so. The curl payload quoting was mangled (the emitted body was not valid JSON); fixed. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/boj-build.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index c4f641d..2850aec 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -14,7 +14,12 @@ jobs: - name: Trigger BoJ Server (Casket/ssg-mcp) run: | # Send a secure trigger to boj-server to build this repository - curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke" -H "Content-Type: application/json" -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\\"}"} + curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke" \ + -H "Content-Type: application/json" \ + -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\"}" + # by-design: best-effort trigger to the internal boj-server; the + # service may be absent on a runner and that must not fail CI. This is + # an advisory step, not a suppressed gate (TOOLING-VERSION-INTEGRITY R4). continue-on-error: true permissions: contents: read From 8fbc840e30e5ae6c15183042b862786915d82e52 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:23:31 +0000 Subject: [PATCH 4/9] fix(docs): retire the stale docs/make.jl (#60) It lists index.md/api.md/examples.md/solvers.md, deleted by the md->adoc migration (#32); nothing runs Documenter (casket-pages.yml builds the site, Documenter is not a dependency), and Documenter cannot consume .adoc sources. Promote-or-delete: the dead script goes. If Documenter HTML API docs are ever wanted again, that is a new decision, not a reason to keep a broken script. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/make.jl | 27 --------------------------- 1 file changed, 27 deletions(-) delete mode 100644 docs/make.jl diff --git a/docs/make.jl b/docs/make.jl deleted file mode 100644 index 5098a61..0000000 --- a/docs/make.jl +++ /dev/null @@ -1,27 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -using Documenter -using SMTLib - -makedocs( - sitename = "SMTLib.jl", - format = Documenter.HTML( - prettyurls = get(ENV, "CI", nothing) == "true", - canonical = "https://hyperpolymath.github.io/SMTLib.jl", - assets = String[], - ), - modules = [SMTLib], - pages = [ - "Home" => "index.md", - "API Reference" => "api.md", - "Examples" => "examples.md", - "Solvers" => "solvers.md", - ], - checkdocs = :exports, - strict = false, -) - -deploydocs( - repo = "github.com/hyperpolymath/SMTLib.jl.git", - devbranch = "main", - push_preview = true, -) From a905071feb8831653fdc030a302cf9d726a6ab0e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:24:06 +0000 Subject: [PATCH 5/9] docs: fill PROJECT_UNIQUE_STRENGTH and retire REQUIRES_INITIALISATION.adoc (#61) The strength is derived from the README (pure-Julia SMT-LIB 2 frontend, one API over Z3/CVC5/Yices/MathSAT, no FFI, graceful :unknown), not invented. With the token filled, the ledger's own agent rule applies: delete the file once no listed token remains anywhere in the tree (grep-verified; the only other hits are the validator's reject-if-contains strings and the ABI template's TYPES guidance, which are not substitution tokens). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .../bot_directives/methodology.a2ml | 2 +- REQUIRES_INITIALISATION.adoc | 56 ------------------- 2 files changed, 1 insertion(+), 57 deletions(-) delete mode 100644 REQUIRES_INITIALISATION.adoc diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml index 754f357..0dc1122 100644 --- a/.machine_readable/bot_directives/methodology.a2ml +++ b/.machine_readable/bot_directives/methodology.a2ml @@ -55,7 +55,7 @@ perfective = 10 # % for SPDX headers, doc updates, formatting, style # Customise this per project — the template default is generic. [methodology.unique-strength] -description = "{{PROJECT_UNIQUE_STRENGTH}}" +description = "Pure-Julia SMT-LIB 2 frontend with one API across four solvers (Z3, CVC5, Yices, MathSAT): constraint building, model retrieval and incremental sessions with no FFI and no code generation, degrading gracefully to :unknown when no solver is present" deepen-not-broaden = true # ============================================================================ diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc deleted file mode 100644 index 88f764c..0000000 --- a/REQUIRES_INITIALISATION.adoc +++ /dev/null @@ -1,56 +0,0 @@ -== REQUIRES INITIALISATION - -*This repository is not finished being set up.* 1 substitution token(s) -across 1 file(s) still have no value. - -=== Why this is not already done - -This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint -(`+just repo-init+`) fills every token that has a single mechanical -answer — owner, repo, author, dates, licence, branch — and it has done -so here. - -The tokens below are the ones it _deliberately cannot_ answer. They need -a decision or a fact that exists only in your head: what this project is -for, what command builds it, which port the service listens on, whether -a PGP key is held at all. The template’s own token vocabulary says as -much — you cannot sensibly answer "`required invariants`" in a -thirty-second bootstrap. - -They were left *visibly unfilled on purpose*. The alternatives were both -worse: inventing plausible values would put confident falsehoods into a -security policy and an architecture document, and silently deleting the -sections would hide the fact that a decision is owed. A visible gap is -honest; a fabricated answer is not. - -=== Do not delete this file until every item below is resolved - -This file is the only marker that the work is outstanding. Deleting it -early does not finish the setup, it just conceals it — and the next -person or agent to arrive will reasonably assume the repo is complete. - -* *If you are a person:* delete this file yourself once the last item is -done. -* *If you are an agent:* resolve what you legitimately can, leave the -rest, and delete this file only when no token below remains anywhere in -the tree. Do not delete it to make a gate go green. - -Re-running the estate top-up tool will remove this file automatically -once nothing is outstanding, so the safest way to finish is to fix the -tokens and let the check confirm it. - -=== What is needed, and where it goes - -==== `+{{PROJECT_UNIQUE_STRENGTH}}+` - -What this does that its alternatives do not. - -Appears in: - -* `+.machine_readable/bot_directives/methodology.a2ml+` - -''''' - -Generated by the estate top-up pass. Rationale and the governing rulings -are in `+hyperpolymath/standards+`; the token vocabulary is -`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`. From fb1d6d17a90710eb4d6612061f462939fb030d81 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:25:21 +0000 Subject: [PATCH 6/9] chore(ci): adopt actions.lock (#58) Estate canon R2 (CICD-SIGNAL-DISCIPLINE, ratified 2026-09-02): actions.lock present everywhere, regenerated in the same PR as any uses: change. The template ships one; this repo never had it (noted in #48's pin notes). Generated from the merged tree's uses: set (14 workflows, 31 refs, including job-level reusable-workflow calls such as hyperpolymath/standards/.github/workflows/governance-reusable.yml@81dbf2dd...), in the v0.0.2 format, and verified in both directions against standards/scripts/check-lock-sync.sh semantics (the checker declared authoritative over gh actions-lock --verify-local for job-level refs). Refs #53 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/actions.lock | 161 +++++++++++++++++++++++++++++++++ 1 file changed, 161 insertions(+) create mode 100644 .github/workflows/actions.lock diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock new file mode 100644 index 0000000..5eb3c99 --- /dev/null +++ b/.github/workflows/actions.lock @@ -0,0 +1,161 @@ +# This file is machine-generated by `gh actions-lock`. +# Do not edit by hand; run `gh actions-lock` to update. +# Docs: https://gh.io/actions-lockfile +version: 'v0.0.2' +workflows: + '.github/workflows/CI.yml': + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'julia-actions/cache@9353db09a0f2bbbdec6f41791918c75d37391b36' + - 'julia-actions/julia-buildpkg@e3eb439fad4f9aba7da2667e7510e4a46ebc46e1' + - 'julia-actions/julia-processcoverage@03114f09f119417c3242a9fb6e0b722676aedf38' + - 'julia-actions/julia-runtest@6e050c8013b833b1195105ff2fce9cd802f53271' + - 'julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32' + '.github/workflows/boj-build.yml': + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + '.github/workflows/casket-pages.yml': + - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d' + - 'actions/deploy-pages@368f82528645a54fb793d4d04e342629a3f51346' + - 'actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9' + - 'haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' + '.github/workflows/codeql.yml': + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'github/codeql-action@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2' + '.github/workflows/governance.yml': + - 'hyperpolymath/standards@81dbf2dd854b1444fd6236fa2352474383b2c2b9' + '.github/workflows/hypatia-scan.yml': + - 'hyperpolymath/standards@81dbf2dd854b1444fd6236fa2352474383b2c2b9' + '.github/workflows/instant-sync.yml': + - 'peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697' + '.github/workflows/label-triage.yml': [] + '.github/workflows/labels.yml': [] + '.github/workflows/mirror.yml': + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f' + - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555' + '.github/workflows/push-email-notify.yml': + - 'hyperpolymath/smtp-notify-action@c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef' + '.github/workflows/release.yml': + - 'actions/attest-build-provenance@4d101475d8b20a2381f78447822ac1eab6504dd8' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c' + - 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' + - 'julia-actions/cache@9353db09a0f2bbbdec6f41791918c75d37391b36' + - 'julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32' + - 'softprops/action-gh-release@efb35369e0ad2afab669f228072c1b0d510eae64' + '.github/workflows/scorecard.yml': + - 'hyperpolymath/standards@81dbf2dd854b1444fd6236fa2352474383b2c2b9' + '.github/workflows/secret-scanner.yml': + - 'hyperpolymath/standards@bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4' +dependencies: + 'actions/attest-build-provenance@4d101475d8b20a2381f78447822ac1eab6504dd8': + ref: '4d101475d8b20a2381f78447822ac1eab6504dd8' + commit: 'sha1-4d101475d8b20a2381f78447822ac1eab6504dd8' + owner_id: 44036562 + repo_id: 760702757 + 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9': + ref: '55cc8345863c7cc4c66a329aec7e433d2d1c52a9' + commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9' + owner_id: 44036562 + repo_id: 215566462 + 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1': + ref: '3d3c42e5aac5ba805825da76410c181273ba90b1' + commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' + owner_id: 44036562 + repo_id: 197814629 + 'actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d': + ref: '45bfe0192ca1faeb007ade9deae92b16b8254a0d' + commit: 'sha1-45bfe0192ca1faeb007ade9deae92b16b8254a0d' + owner_id: 44036562 + repo_id: 513659658 + 'actions/deploy-pages@368f82528645a54fb793d4d04e342629a3f51346': + ref: '368f82528645a54fb793d4d04e342629a3f51346' + commit: 'sha1-368f82528645a54fb793d4d04e342629a3f51346' + owner_id: 44036562 + repo_id: 438112499 + 'actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c': + ref: '3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c' + commit: 'sha1-3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c' + owner_id: 44036562 + repo_id: 192626254 + 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a': + ref: '043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' + commit: 'sha1-043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' + owner_id: 44036562 + repo_id: 192625955 + 'actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9': + ref: 'fc324d3547104276b827a68afc52ff2a11cc49c9' + commit: 'sha1-fc324d3547104276b827a68afc52ff2a11cc49c9' + owner_id: 44036562 + repo_id: 496012378 + 'dtolnay/rust-toolchain@e2a55d2ffb04f378e9626c28d38b36d230d1e12f': + ref: 'e2a55d2ffb04f378e9626c28d38b36d230d1e12f' + commit: 'sha1-e2a55d2ffb04f378e9626c28d38b36d230d1e12f' + owner_id: 1940490 + repo_id: 260749683 + 'github/codeql-action@2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2': + ref: '2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2' + commit: 'sha1-2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2' + owner_id: 9919 + repo_id: 259445878 + 'haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d': + ref: '0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' + commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' + owner_id: 75048950 + repo_id: 623796603 + 'hyperpolymath/smtp-notify-action@c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef': + ref: 'c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef' + commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef' + owner_id: 6759885 + repo_id: 1352485172 + 'hyperpolymath/standards@81dbf2dd854b1444fd6236fa2352474383b2c2b9': + ref: '81dbf2dd854b1444fd6236fa2352474383b2c2b9' + commit: 'sha1-81dbf2dd854b1444fd6236fa2352474383b2c2b9' + owner_id: 6759885 + repo_id: 1116521501 + 'hyperpolymath/standards@bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4': + ref: 'bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4' + commit: 'sha1-bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4' + owner_id: 6759885 + repo_id: 1116521501 + 'julia-actions/cache@9353db09a0f2bbbdec6f41791918c75d37391b36': + ref: '9353db09a0f2bbbdec6f41791918c75d37391b36' + commit: 'sha1-9353db09a0f2bbbdec6f41791918c75d37391b36' + owner_id: 53965732 + repo_id: 441908600 + 'julia-actions/julia-buildpkg@e3eb439fad4f9aba7da2667e7510e4a46ebc46e1': + ref: 'e3eb439fad4f9aba7da2667e7510e4a46ebc46e1' + commit: 'sha1-e3eb439fad4f9aba7da2667e7510e4a46ebc46e1' + owner_id: 53965732 + repo_id: 210451482 + 'julia-actions/julia-processcoverage@03114f09f119417c3242a9fb6e0b722676aedf38': + ref: '03114f09f119417c3242a9fb6e0b722676aedf38' + commit: 'sha1-03114f09f119417c3242a9fb6e0b722676aedf38' + owner_id: 53965732 + repo_id: 249500631 + 'julia-actions/julia-runtest@6e050c8013b833b1195105ff2fce9cd802f53271': + ref: '6e050c8013b833b1195105ff2fce9cd802f53271' + commit: 'sha1-6e050c8013b833b1195105ff2fce9cd802f53271' + owner_id: 53965732 + repo_id: 208538601 + 'julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32': + ref: 'fa02766e078afaaf09b14210362cee14137e6a32' + commit: 'sha1-fa02766e078afaaf09b14210362cee14137e6a32' + owner_id: 53965732 + repo_id: 202020219 + 'peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697': + ref: '28959ce8df70de7be546dd1250a005dd32156697' + commit: 'sha1-28959ce8df70de7be546dd1250a005dd32156697' + owner_id: 18365890 + repo_id: 220359305 + 'softprops/action-gh-release@efb35369e0ad2afab669f228072c1b0d510eae64': + ref: 'efb35369e0ad2afab669f228072c1b0d510eae64' + commit: 'sha1-efb35369e0ad2afab669f228072c1b0d510eae64' + owner_id: 2242 + repo_id: 204253808 + 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555': + ref: 'e83874834305fe9a4a2997156cb26c5de65a8555' + commit: 'sha1-e83874834305fe9a4a2997156cb26c5de65a8555' + owner_id: 135788 + repo_id: 208510314 From 5c0c375d5888e55d98fb63c3c239d52ee4cd9d39 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 11:37:10 +0100 Subject: [PATCH 7/9] Update .machine_readable/bot_directives/methodology.a2ml Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- .machine_readable/bot_directives/methodology.a2ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml index 0dc1122..b2d5a38 100644 --- a/.machine_readable/bot_directives/methodology.a2ml +++ b/.machine_readable/bot_directives/methodology.a2ml @@ -55,7 +55,7 @@ perfective = 10 # % for SPDX headers, doc updates, formatting, style # Customise this per project — the template default is generic. [methodology.unique-strength] -description = "Pure-Julia SMT-LIB 2 frontend with one API across four solvers (Z3, CVC5, Yices, MathSAT): constraint building, model retrieval and incremental sessions with no FFI and no code generation, degrading gracefully to :unknown when no solver is present" +description = "Pure-Julia SMT-LIB 2 frontend with one API across four solvers (Z3, CVC5, Yices, MathSAT): constraint building, model retrieval and incremental sessions with no FFI and no code generation, requiring an installed solver" deepen-not-broaden = true # ============================================================================ From bd59686b8e32a0ec826c651739f7643cf466290b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:38:03 +0000 Subject: [PATCH 8/9] =?UTF-8?q?fix:=20address=20CodeRabbit=20review=20?= =?UTF-8?q?=E2=80=94=20jq-encode=20the=20boj=20payload,=20correct=20claims?= =?UTF-8?q?,=20restore=20links?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - boj-build.yml: pass github.repository/github.ref_name through env and build the JSON with jq --arg (CWE-78 hardening; values are never interpolated into the shell). - methodology.a2ml: the no-solver path raises ErrorException at SMTContext construction; :unknown is a check-sat status. Wording corrected. - ULTRAPLAN-ISSUE-43.adoc: restore the issue/PR cross-references that lost their link targets (dangling ']'), and record the post-change green CI run 38044880793 with the Z3 install sentinel and solver-backed tests executing on the ubuntu legs. - SMTLIB-AXIOM-PARITY-CHECKLIST.adoc: the docs-build entry pointed at the retired docs/make.jl; it now names the supported casket-pages.yml site build, and notes Z3-on-ubuntu landed with #62. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/boj-build.yml | 14 ++++++++++++-- .../bot_directives/methodology.a2ml | 2 +- SMTLIB-AXIOM-PARITY-CHECKLIST.adoc | 6 ++++-- ULTRAPLAN-ISSUE-43.adoc | 19 +++++++++++++------ 4 files changed, 30 insertions(+), 11 deletions(-) diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index 2850aec..9ac7357 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -12,11 +12,21 @@ jobs: - name: Checkout uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - name: Trigger BoJ Server (Casket/ssg-mcp) + env: + REPOSITORY: ${{ github.repository }} + REF_NAME: ${{ github.ref_name }} run: | - # Send a secure trigger to boj-server to build this repository + # Send a secure trigger to boj-server to build this repository. + # Values pass through env and are JSON-encoded with jq --arg, never + # interpolated into the shell or the payload by string pasting. + payload="$(jq -n \ + --arg repo "$REPOSITORY" \ + --arg branch "$REF_NAME" \ + --arg engine "casket" \ + '{repo: $repo, branch: $branch, engine: $engine}')" curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke" \ -H "Content-Type: application/json" \ - -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\"}" + -d "$payload" # by-design: best-effort trigger to the internal boj-server; the # service may be absent on a runner and that must not fail CI. This is # an advisory step, not a suppressed gate (TOOLING-VERSION-INTEGRITY R4). diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml index 0dc1122..cff9f4c 100644 --- a/.machine_readable/bot_directives/methodology.a2ml +++ b/.machine_readable/bot_directives/methodology.a2ml @@ -55,7 +55,7 @@ perfective = 10 # % for SPDX headers, doc updates, formatting, style # Customise this per project — the template default is generic. [methodology.unique-strength] -description = "Pure-Julia SMT-LIB 2 frontend with one API across four solvers (Z3, CVC5, Yices, MathSAT): constraint building, model retrieval and incremental sessions with no FFI and no code generation, degrading gracefully to :unknown when no solver is present" +description = "Pure-Julia SMT-LIB 2 frontend with one API across four solvers (Z3, CVC5, Yices, MathSAT): constraint building, model retrieval and incremental sessions with no FFI and no code generation, and solver discovery that selects among the installed solvers at run time (a missing solver raises a clear install-it error at construction)" deepen-not-broaden = true # ============================================================================ diff --git a/SMTLIB-AXIOM-PARITY-CHECKLIST.adoc b/SMTLIB-AXIOM-PARITY-CHECKLIST.adoc index c54e446..b0e9427 100644 --- a/SMTLIB-AXIOM-PARITY-CHECKLIST.adoc +++ b/SMTLIB-AXIOM-PARITY-CHECKLIST.adoc @@ -58,9 +58,11 @@ Bring `SMTLib.jl` to the same release/readiness posture as `Axiom.jl` for JuliaH == INTEND (Strongly recommended for operational parity) 1. CI expansion toward Axiom breadth - Keep current Julia matrix and add: -- docs build verification (`docs/make.jl`). +- docs build verification (`casket-pages.yml` site build; the Documenter + `docs/make.jl` path was retired in #60 and no supported Documenter build exists). - package install smoke from clean temp environment. -- optional solver-backed integration job(s) with explicit Z3/CVC5 installs. +- optional solver-backed integration job(s) with explicit Z3/CVC5 installs + (Z3 on the ubuntu legs landed with #62; CVC5 still optional). - artifact upload for solver capability report and test evidence. 2. Diagnostics and failure ergonomics diff --git a/ULTRAPLAN-ISSUE-43.adoc b/ULTRAPLAN-ISSUE-43.adoc index cf75235..26dc611 100644 --- a/ULTRAPLAN-ISSUE-43.adoc +++ b/ULTRAPLAN-ISSUE-43.adoc @@ -6,13 +6,13 @@ == 0. Scope and authority -*Primary issue:* ] — +*Primary issue:* https://github.com/hyperpolymath/SMTLib.jl/issues/43[#43] — _Triage: 9 red checks surfaced by the citation PR #41_ (open, `research`). Its standing rule: a red check is *an issue with acceptance criteria, never a merge blocker*, and each check must end up *fixed*, *retired*, or *accepted with a documented exemption* — "it may not stay undetermined". -*Secondary issue:* ] — the 12 test +*Secondary issue:* https://github.com/hyperpolymath/SMTLib.jl/issues/47[#47] — the 12 test failures (closed 2026-10-09 via PR #49). Included here only to *verify* its acceptance criteria actually hold after the fix landed. @@ -98,26 +98,26 @@ pre-existing, not caused by the citation PR. |=== | PR | Merge commit | What it fixed -| ] +| https://github.com/hyperpolymath/SMTLib.jl/pull/45[PR #45] | `93305d82` | Matrix arch dimension dropped — setup-julia picks the runner arch (macOS legs). *This renamed the checks* (see §1.3). -| ] +| https://github.com/hyperpolymath/SMTLib.jl/pull/48[PR #48] | `487c7ab4` | (a) `math.jl:42` parse error (module loaded at all), (b) duplicate `FPSort`/`RegLan` structs (precompile rejected), (c) *the pin*: `julia-runtest` re-pinned to `d0c4f093badade621cd041bba567d1e832480ac2` (tag `v1.10.0`, resolved via `git ls-remote`). -| ] +| https://github.com/hyperpolymath/SMTLib.jl/pull/49[PR #49] | `14da03a7` | The 12 test failures tracked by #47, fixed at root cause in `src/` or by correcting tests that called APIs that never existed (`declare_const` / `to_smtlib_script` → `declare` / `SMTLib.build_script`). No test skipped, deleted or loosened. #47 closed. -| ] / ] +| https://github.com/hyperpolymath/SMTLib.jl/pull/50[PR #50] / https://github.com/hyperpolymath/SMTLib.jl/pull/51[PR #51] | `126ced1` (current `main` HEAD) | Release workflow fix; version bump to 0.2.2. |=== @@ -375,6 +375,13 @@ the merged tree). Remaining open: #56 (mirror) and #57 (Pages) await the owner's fix/retire ruling; umbrella #53 closes when they are determined (its AC2–AC4). +Post-change verification (this PR's own CI, run `38044880793` on `fb1d6d1`): +the `Install Z3 (ubuntu)` step is green with its `z3 --version` execution +sentinel on all three ubuntu legs (1.10, 1.11, nightly), `Run tests` is green +on all 9 matrix legs — so the solver-gated tests (including the #47 unsat-core +path) executed with Z3 on PATH rather than skipping — and every governance, +CodeQL, Hypatia and secret-scan check is green. + _Note on this document: it is the plan and its execution record. Recon clones of `standards` and `rsr-template-repo` were read from GitHub and live outside this repository._ From 6325d53db6b6f1549dcce345f27f146c4eb75303 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 10 Oct 2026 10:39:04 +0000 Subject: [PATCH 9/9] docs: restore the standards#994 cross-reference in the ultraplan Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- ULTRAPLAN-ISSUE-43.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ULTRAPLAN-ISSUE-43.adoc b/ULTRAPLAN-ISSUE-43.adoc index 26dc611..51185d4 100644 --- a/ULTRAPLAN-ISSUE-43.adoc +++ b/ULTRAPLAN-ISSUE-43.adoc @@ -28,7 +28,7 @@ acceptance criteria actually hold after the fix landed. acceptance criteria, never a blocker on stopping." Working state = default branch green and the thing runs. -| `standards` ] (and the #43 body) +| https://github.com/hyperpolymath/standards/issues/994[standards#994] (and the #43 body) | triage determinations | For every red: one determination — *fix* / *retire the gate* / *accept with a documented exemption*. "Repair or retire; never mute." No `continue-on-error`,