Repository navigation
fix(ci): make the release workflow build, attest and publish - #50
Conversation
The release workflow has never produced a Release. Fixed here: - The SBOM step loaded JSON, which is not a dependency, from an uninstantiated project, and named components by UUID. It now instantiates the project, reads the direct dependencies by name, then loads JSON from a temporary environment. - AcceleratorGate is registered only in the hyperpolymath registry. The build and SBOM jobs now add it alongside General. - "Package artifacts" had no shell, so windows-latest ran it in pwsh. The build job now defaults to bash. A manual run now checks out the requested tag, so the artefacts match the tagged tree. The version is passed through env (it was inlined into the script), must match vX.Y.Z, and must already exist as a tag. Any committed manifest is ignored, so the release is tested the way users install it. Top-level permissions drop to read; the release job keeps its own write grants. A pull_request trigger on this file runs the build and SBOM jobs at review. The build job runs Pkg.test(), so this workflow cannot go green until the test failures in #47 are fixed (PR #49). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configuration
📒 Files selected for processing (1)
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review. 📜 Recent review details⏰ Context from checks skipped due to timeout. (26)
🔇 Additional comments (1)
📝 SummarySummary by CodeRabbit
WalkthroughThe release workflow adds pull-request validation, updates build and SBOM dependency preparation, and checks the version and tag before release creation. It also changes checksum generation and adds an attestation verification command to the release instructions. ChangesRelease workflow
Priority: ➖ Normal Estimated code review effort: 3 (Moderate) | ~20 minutes Change: Bug fix
|
actions/checkout resolves an unqualified ref to a branch of that name before a tag (src/ref-helper.ts:52-57 at the pinned SHA). If a branch named like the tag existed, a manual run would package that branch, while the release job only confirms that the tag exists. Both checkouts now pass refs/tags/<version> on a manual run, and an empty ref (the triggering ref) on push and pull_request runs, as before. Raised by CodeRabbit on hyperpolymath/Causals.jl#69. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX
## Summary This fixes the 12 test failures that #47 tracks. Each fix is in `src/` at the root cause, or in a test that called an API that never existed. No test is skipped, deleted or loosened. | # | Failure | Root cause | Fix | |---|---|---|---| | 1 | Statistics Parsing / Parse numeric statistics, `runtests.jl:876–881` (3 fail + 3 `KeyError`) | `parse_statistics` matched only a single-pair list `(:key value)` that closes at once. Solver statistics come as one list of many pairs, and Z3 prints it over several lines. | It now finds each `(:` keyword list and reads every `:key value` pair in it. Quoted strings are consumed first, so a `(:…)` inside an error message is not read as a list. Against real Z3 4.13.3 `(get-info :all-statistics)` output it returns 13 entries. | | 2 | evaluate / Boolean logic, `runtests.jl:931–932` | Julia parses `p && q` and `p \|\| q` as `Expr(:&&)` / `Expr(:\|\|)`, not as calls. The `:call` branch never ran, so the substituted `Expr` came back. | `evaluate` computes `&&` and `\|\|` once every operand is a `Bool`. If any operand is still unknown, it returns the substituted `Expr`. | | 3 | Unsat core extraction (Z3), `runtests.jl:1153` | Two defects. First, `set_option!(ctx, :produce_unsat_cores, true)` sent the option name with underscores, which is not the SMT-LIB name (cvc5 1.1.2 answers `unsupported`). Second, plain `check_sat(ctx)` never sent `(get-unsat-core)`, even with the option on. | The `Symbol` method of `set_option!` maps `_` to `-`. `check_sat`'s `get_unsat_core` now defaults to the context's `produce-unsat-cores` option. An explicit `get_unsat_core=true/false` behaves as before. Z3 now returns `[:pos, :neg]`. | | 4 | e2e `declare → assert → check_sat`, `e2e_test.jl:23`; e2e `to_smtlib_script`, `e2e_test.jl:41`; property `assert!` count, `property_test.jl:31` (3 `UndefVarError`) | **These tests were wrong.** `declare_const` and `to_smtlib_script` have never existed in `src/`. Commit `ed8eff1` added them only as calls, in the tests and in `benches/benchmarks.jl`. | The tests and benches now use the exported, documented API: `declare(ctx, name, sort)` (README: "`declare(ctx, name, sort)` — Declare a constant or function") and `SMTLib.build_script(ctx, get_model)`. The "Script Building" testset already exercises `build_script`. | **Why fix 4 changes the tests rather than adding `declare_const`.** #47 leaves the choice open. Adding the two functions would give the package a second name for `declare` and a public wrapper around an internal function, and only test code from a single commit would use them. Keeping `declare` as the one public way to declare a constant is the simpler choice. The alternative, adding and exporting `declare_const(ctx, name, ::Symbol)` and `to_smtlib_script`, is easy to do if the owner prefers it. **No assertion is weakened, and two are stronger:** - *"unknown sort raises an error"* passed vacuously before. The `UndefVarError` for `declare_const` satisfied `@test_throws Exception`. The test now asserts that an unmapped type (`Vector{Int}`) raises a `MethodError` and that no declaration is recorded. I checked that `declare(ctx, :z, Vector{Int})` really throws `MethodError: no method matching smt_type(::Type{Vector{Int64}})`. - The pipeline test now also checks that exactly three `(assert` forms are emitted, as its own comment says. `CHANGELOG.adoc` gains a `=== Fixed` section under `[Unreleased]`. **Second commit (`318efef`), from CodeRabbit's review.** A quoted string that is not a pair's value could leak a false pair. On `6604a9c`, `(:a 1 "stray :time 99")` gave `time => 99`; I reproduced this. CodeRabbit's own example, `(:reason "message :time 99")`, was already parsed correctly, because there the string is a value and is consumed whole. The pair search now consumes any stray string whole as well. The commit adds 9 regression tests: - Z3's multi-line layout; - quoted values containing parentheses and `:key value` text; - the stray string; - an error message containing `(:foo bar)`; - a keyword value. It also replaces the tautological `isempty(stats) || !isempty(stats)` in "Empty output" with `isempty(stats)`. **Third commit (`a6c6bc6`): make the CI matrix able to run the tests.** #47's last acceptance criterion is *"`Pkg.test()` passes on the CI matrix (1.10, 1.11, nightly × ubuntu/macos/windows)"*. Two things stopped that, on `main` and on this branch before this commit: - Every `test (*)` job stopped at **Build package** with `expected package AcceleratorGate [59f742c7] to be registered`. `julia-buildpkg` adds only General, and AcceleratorGate is in `hyperpolymath/julia-professional-registry`. `CI.yml` now passes that registry to `julia-buildpkg` through its existing `localregistry` input; the test step reuses the same depot. The registry needs no credentials: #50's Release run passed its "Add registries" step on a hosted runner. - CI installs neither z3 nor cvc5. Four testsets (the three e2e `SMTContext` testsets and the property `assert!` count) only build SMT-LIB text, but they called `SMTContext()`, which looks a solver up on `PATH` and raises `No SMT solver found. Install z3 or cvc5.` These calls were already on `main`. They now pass `SMTContext` a solver record that is never run (`SMTSolver(:z3, "/nonexistent/z3", "never run")`). `declare`, `assert!` and `build_script` never read the context's solver; only `run_solver` does. The first of them is titled "(no solver)" and its comment says it "must not error even without a solver installed", so this makes the test do what it says. Closes #47. All nine `CI / test (*)` jobs on this head (`a6c6bc6`) are green: run 37912491992. Eight passed on the first attempt. `test (nightly, macos-latest)` first failed at **Setup Julia**, before any package code ran, with `getaddrinfo ENOTFOUND julialangnightlies-s3.julialang.org`. That is a runner DNS failure; the host resolved and answered 200 from here. The job was re-run unchanged and passed (job 113764403648, 2026-10-09T09:50Z). 1.11, nightly, macOS and Windows are verified by CI alone; I ran 1.10 and 1.12 on Linux. ## Type of change - [x] 🐛 Bug fix (non-breaking change that fixes an issue) - [ ] ✨ New feature (non-breaking change that adds functionality). No new public function. - [ ] 💥 Breaking change (would change existing behaviour). There are two small behaviour changes, both towards SMT-LIB-correct output. A `Symbol` option key now has `_` mapped to `-`; the old underscore name was not a valid SMT-LIB option name. Plain `check_sat` now requests the unsat core when the context already enables `produce-unsat-cores`. String keys and explicit keyword arguments are unchanged. - [ ] 🕳️ Soundness fix. Not a checker or proof false-negative. - [ ] 📖 Documentation. The only doc changes are docstrings and the CHANGELOG entry. - [ ] 🧹 Refactor / tech debt - [ ] ⚡ Performance - [x] 🔧 Build / CI / tooling. `CI.yml`: `julia-buildpkg` gains the `localregistry` input (third commit). ## 📌 New pins Head SHA: **a6c6bc6effde7ddb5cd5b4f8d173bd671e69a4c4** No pins added or changed. The `julia-buildpkg` pin (`e3eb439f…`, v1.7.0) is unchanged; only its `with:` input is new. There are no `actions.lock` changes (the repo has none) and no `Project.toml` compat changes. `Manifest.toml` is gitignored. `CI.yml` stays in block YAML, because this repo's gates do not yet meet the KYAML preconditions. ## How has this been verified? I ran `Pkg.test()` from a throwaway depot (General plus `hyperpolymath/julia-professional-registry`), with z3 4.13.3 and cvc5 1.1.2 on `PATH`, so the solver-dependent testsets, including the Z3 unsat-core test, actually ran: | Julia | `main` @ 487c7ab | 6604a9c (first commit) | **318efef (second commit)** | |---|---|---|---| | 1.12.6 | 818 pass / 6 fail / 6 error (830) | 864 pass (864) | **873 pass** (873) | | 1.10.10 | 818 pass / 6 fail / 6 error (830) | 864 pass (864) | **873 pass** (873) | | 1.11 | not run, not installed on this machine | not run | not run | From `main` to the first commit, the total rises by 34: - The property test now runs all 30 iterations instead of erroring on the first (+29). - The e2e pipeline testset runs 4 checks instead of 1 error, including the new assert count (+3). - The e2e `build_script` testset runs 2 checks instead of 1 error (+1). - The unknown-sort testset gains the "no declaration recorded" check (+1). The second commit adds 9 tests to "Statistics Parsing" (864 → 873). They are described below. I also checked `parse_statistics` directly against these inputs: - real Z3 multi-line statistics (13 keys; `time` → `0.0`, `max-memory` → `17.82`, `num-allocs` → `35972`); - the test string; - a quoted value containing parentheses (`(:name "Z3 (x)")`); - a keyword value (`(:reason-unknown :incomplete)`); - an error message containing `(:foo bar)`, which correctly yields nothing. The new `check_sat` default has one path that no test covers. When `produce-unsat-cores` is on and the problem is satisfiable, plain `check_sat` now also sends `(get-unsat-core)`. I ran this case directly on both solvers: - **z3:** `status=sat`, model `x => 6`, followed by `(error "… unsat core is not available")`. - **cvc5:** `status=sat`, model `x => 6`, followed by `(error "Cannot get unsat core unless in unsat mode.")`. In both cases the status and the model parse correctly. **The CI condition: no solver on `PATH`.** For the third commit I also ran `Pkg.test()` with a `PATH` that has neither z3 nor cvc5 (`command -v z3 cvc5` finds nothing; `Sys.which` is the package's lookup): | Julia, no solver | 318efef | **a6c6bc6 (head)** | |---|---|---| | 1.10.10 | 718 pass / 4 error (722), rc=1 | **757 pass** (757), rc=0 | | 1.12.6 | not run | **757 pass** (757), rc=0 | The 4 errors were the `SMTContext()` calls described above. 757 = 718 + 39: the four testsets now run their 5 + 2 + 2 + 30 checks. With z3 and cvc5 on `PATH`, the head still gives **873 pass** (873) on 1.10.10, the same as `318efef`. CI note: the solver-dependent testsets ("Solver Integration", the Z3 optimisation and unsat-core tests) log `No SMT solver found, skipping …` and run only where a solver is on `PATH`, so CI does not exercise them. Installing a solver in CI is a separate change. ## Checklist - [x] My commits are **signed**. All three commits are SSH-signed: `git log --format=%G?` gives `G` for each. GitHub reported `verified: true` (`valid`) for the first two, and the GraphQL commit `signature` reports `VALID` (signer `hyperpolymath`) for the third. - [x] I ran the project's own checks/tests locally and they pass. `Pkg.test()` passes on 1.12.6 and 1.10.10, with and without solvers, as above. 1.11 was not run. `actionlint` passes on `CI.yml`. - [ ] New files carry the correct `SPDX-License-Identifier`. No new files; every touched file keeps its existing header. - [x] Docs are updated, and no public claim now overstates what the code does. The docstrings for `parse_statistics`, `evaluate`, `check_sat` and both `set_option!` methods describe the new behaviour. The two `set_option!` methods had no docstring before. - [x] I have not introduced a soundness hole (or I have flagged where I might have). The `check_sat` default only adds a `(get-unsat-core)` request when the user has turned unsat cores on. ## Notes for reviewers - **Decision for the owner:** #47 offers two paths for fix 4. This PR keeps `declare` as the only public way to declare a constant (see above). Say if you want `declare_const` added instead. - **Findings, not fixed here (out of scope):** - CI installs no SMT solver, so the solver-dependent testsets are skipped there (see the CI note). - `parse_unsat_core` reads one line. cvc5 1.1.2 prints the core one label per line (`(` / `pos` / `neg` / `)`), so cvc5 cores come back empty. The test is Z3-only, so this is not one of the 12 failures. - cvc5's statistics format, `(:all-statistics (("name" v) …))`, is a nested list. `parse_statistics` deliberately skips it rather than producing wrong values. - The estate docstring scanner (`standards/.githooks/docstring-scan.sh`) skips `.jl` files, so it reported no verdict (`skipped=4`). I checked the docstrings by hand. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> ## Summary **Draft until #50 merges.** This is step 2 of the v0.2.2 release plan in #50: bump the version, and record what 0.2.2 contains. v0.2.2 will be the first tag that produces a GitHub Release. - **`Project.toml`:** `version = "0.2.1"` → `"0.2.2"`. No other tracked file contains the version string (`git grep 0.2.1` on `main`). - **`CHANGELOG.adoc`:** - **`[0.2.2] - 2026-10-09`** contains only what is new since the v0.2.1 tag: - the test-suite fixes for #47, which landed in #49; - the release workflow fix (#50). - **A new `[0.2.1]` section** holds what the v0.2.1 tag tree already contains: - the UUIDv8 re-mint (#46), marked **Breaking**; - the load fix (#48); - the Added/Changed lines that sat under `[Unreleased]`. These were already in `ef7ba57`, the 0.2.0 commit, so leaving them under 0.2.2 would claim they are new. - 0.2.0 was registered in JPR under the old placeholder UUID, and never tagged. A one-line note under `[0.2.1]` says so. - `[Unreleased]` is left empty. No issue tracks the bump. The release plan is in #50's description. ## Type of change - [ ] 🐛 Bug fix: no code changes. - [ ] ✨ New feature: no. - [ ] 💥 Breaking change: no. The breaking UUID change shipped in 0.2.1 (#46); this PR only records it. - [ ] 🕳️ Soundness fix: not applicable. - [x] 📖 Documentation (CHANGELOG) - [ ] 🧹 Refactor / tech debt: no. - [ ] ⚡ Performance: no. - [ ] 🔧 Build / CI / tooling: no workflow changes. The version bump is release metadata. ## 📌 New pins Head SHA: **`73271c483a1ca8944d24cf8b83785ecb87517921`** None. This PR changes only `Project.toml`'s `version` and `CHANGELOG.adoc`. ## How has this been verified? - **`Project.toml` parses:** - Command: `julia -e 'import TOML; TOML.parsefile("Project.toml")'` (Julia 1.12.6). - Result: `SMTLib 0.2.2 01a11d29-d89a-86da-8e3a-553d114a3537`. The UUID is unchanged. - **Which lines belong to 0.2.1:** - Method: for each line that sat under `[Unreleased]`, find the commit that added it (`git log -S`), then test whether that commit is an ancestor of `v0.2.1` (`git merge-base --is-ancestor`). - The five Added/Changed lines came from `ef7ba57`, which is in v0.2.1. - The seven #47 lines came from `14da03a`, which is not in v0.2.1. - **What JPR registered as 0.2.1:** - JPR's `S/SMTLib/Versions.toml` lists only `0.2.1`, with `git-tree-sha1 = 05a805f…`. - That is the tree of `487c7ab`, the commit the `v0.2.1` tag points at. #46's merge tree (`047a2e8d…`) is different. - So 0.2.1 contains both #46 and #48. - **Tests:** not run locally, because no source file changes. CI runs the `test (*)` matrix on this PR. The suite passed 9/9 on #49's head. **Horizon:** the version bump and the changelog. The release path is verified only by #50's CI and, in the end, by the tag push. ## Checklist - [x] My commits are **signed** (`git commit -S`). `git log --format=%G?` shows `G` (SSH). - [ ] I ran the project's own checks/tests locally and they pass. Not run: no source change. CI runs them. - [x] New files carry the correct `SPDX-License-Identifier`: there are no new files. `CHANGELOG.adoc` keeps its `CC-BY-SA-4.0` header, and `Project.toml` keeps `MPL-2.0`. - [x] Docs are updated, and no public claim now overstates what the code does: - The 0.2.2 release-workflow line describes #50's workflow: tarballs, `sbom.json`, `checksums.txt` and provenance attestation. - It becomes true only once #50 is merged, which is why this PR is a draft. - [x] I have not introduced a soundness hole. ## Notes for reviewers - **Order of steps:** 1. #49 is merged (`14da03a`, 2026-10-09 10:46Z). 2. Merge #50. 3. Mark this PR ready, and merge it. 4. Push the signed tag with the command below. The tag push runs the fixed `release.yml` from the tagged tree, which publishes the Release. 5. Register v0.2.2 in JPR. - **Tag command:** - It refuses unless #50 is merged and `main` says 0.2.2. Without the first check, a tag pushed before #50 would run the old, broken workflow. - `d=/home/hyperpolymath/developer/hyper-repos/LANG/julia/SMTLib.jl; gh pr view 50 -R hyperpolymath/SMTLib.jl --json state -q .state | grep -qx MERGED && git -C "$d" fetch origin main && git -C "$d" show origin/main:Project.toml | grep -q '^version = "0.2.2"' && git -C "$d" tag -s v0.2.2 -m v0.2.2 origin/main && git -C "$d" push origin v0.2.2` - **Release date:** the `[0.2.2]` date is 2026-10-09, on the assumption that the tag is pushed today. If it is pushed later, change the date before tagging. - Nothing is set to auto-merge. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> ## Summary Tag `v0.1.1` (`2cc3088`) has no GitHub Release, because `release.yml` was the unfilled scaffold. Its build step only echoed `"Build your artifacts here"`, so the SLSA job attested an empty subject list. It also downloaded git-cliff from `releases/latest/download/git-cliff-x86_64-unknown-linux-gnu.tar.gz`, which returns **404** today; git-cliff's asset names now carry the version. This PR replaces it with a workflow that tests the package, packages it, and publishes a Release. This is the same release-path fix as hyperpolymath/Causals.jl#69 and hyperpolymath/SMTLib.jl#50, adapted to this repo. No issue tracks it. ## Changes - **Build job:** - Runs on Julia 1.10. - Adds General and `hyperpolymath/julia-professional-registry` (JPR). Causals, ZeroProb, Cliodynamics and their dependency AcceleratorGate are registered in JPR, not in General. - Removes any committed `Manifest.toml`, so the package is resolved fresh from `[compat]`, the way users install it. - Runs `Pkg.instantiate(); Pkg.build(); Pkg.test()`. - Packages `src/`, `Project.toml`, `README.adoc` and `LICENSE`. - `timeout-minutes: 45`, matching `ci.yml:30`, because a cold install of this dependency closure is slow. - **SBOM:** the build job writes a CycloneDX 1.4 `sbom.json`. It reads the direct dependencies by name from the resolved environment, then loads JSON from a temporary environment, because JSON is not a dependency of this package. - **Changelog:** `orhun/git-cliff-action` v4.9.1, with git-cliff pinned to v2.14.2 instead of "latest". It uses the repo's existing `cliff.toml` with `--latest --strip header`. - **Provenance:** `actions/attest-build-provenance` v4.2.2 attests the actual release files (`release/*`, including `checksums.txt`). It replaces the SLSA generator, whose reusable workflow calls nested actions that cannot be pinned by SHA. - **A manual run releases an existing tag.** `workflow_dispatch` takes `version`. Both checkouts use `ref: ${{ inputs.version && format('refs/tags/{0}', inputs.version) || '' }}`, so the artefacts and changelog come from the tagged tree. The `refs/tags/` prefix is needed because checkout tries a bare name as a branch before it tries a tag (`src/ref-helper.ts:52-57` at the pinned SHA). It was added in `238d922`, after CodeRabbit raised the issue on the twin PR hyperpolymath/Causals.jl#69. The release job then checks the version: - it is passed through `env:`, not inlined into the script; - it must match `^v[0-9]+\.[0-9]+\.[0-9]+(-[0-9A-Za-z.]+)?$`; - it must already exist as a tag (`git ls-remote --exit-code`). So a typo cannot make `action-gh-release` create a new tag on `main`. A `-pre` suffix marks the Release as a prerelease. - **Least privilege.** The top-level permissions are `contents: read`. Only the release job gets `contents: write`, `id-token: write` and `attestations: write`. - **The workflow tests itself.** A `pull_request` trigger on this file runs the build and changelog jobs on this PR. The release job is skipped on PRs (`if: github.event_name != 'pull_request'`). - The unused `full-CHANGELOG.md` artefact is dropped, because nothing consumed it. ## 📌 New pins Head SHA: **`238d922e711577f97b67ee613ee91525432a4351`** Each new or changed pin below was resolved from its tag to the same commit with a GraphQL `ref(qualifiedName:)` lookup: | Action | Pin | Tag | Change | |---|---|---|---| | `julia-actions/setup-julia` | **`fa02766e078afaaf09b14210362cee14137e6a32`** | v3.0.2 | new | | `julia-actions/cache` | **`9353db09a0f2bbbdec6f41791918c75d37391b36`** | v3.5.0 | new | | `actions/upload-artifact` | **`043fb46d1a93c77aae656e7c1c64a875d1fc6a0a`** | v7.0.1 | was `ea165f8d…` (v4.6.2) | | `orhun/git-cliff-action` | **`a9a95522b26fe6403f7bb24031f21fb573d0f5ff`** | v4.9.1 | new; its `version:` input pins git-cliff **v2.14.2** | | `actions/download-artifact` | **`3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c`** | v8.0.1 | new (was only a commented-out v4 line) | | `actions/attest-build-provenance` | **`4d101475d8b20a2381f78447822ac1eab6504dd8`** | v4.2.2 | new | Unchanged: `actions/checkout@8e8c483d…` (v6.0.1) and `softprops/action-gh-release@a06a81a0…` (v2). Removed: `slsa-framework/slsa-github-generator/…/generator_generic_slsa3.yml@f7dd8c54…` (v2.1.0). This repo has no `actions.lock`. The workflow stays in block YAML, because this repo's gates do not yet meet the KYAML preconditions. ## RSR Quality Checklist ### Required - [x] Tests pass (`just test` or equivalent). `Pkg.test()` passes on the `v0.1.1` tree, which is this PR's parent commit; see Testing. This PR changes only `release.yml`. - [ ] Code is formatted (`just fmt` or equivalent). Not applicable: no Julia source changes. actionlint is the check that applies to the workflow. - [x] Linter is clean (no new warnings or errors). `actionlint .github/workflows/release.yml` exits 0. - [x] No banned language patterns (no TypeScript, no npm/bun, no Go/Python). The change is YAML with inline bash and Julia. - [ ] No `unsafe` blocks without `// SAFETY:` comments. Not applicable: no Rust or Zig code. - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`). None introduced. - [x] SPDX license headers present on all new/modified source files. `release.yml` keeps its `MPL-2.0` header; no new files. - [x] No secrets, credentials, or `.env` files included. The workflow reads no secrets; `action-gh-release` uses the job's `GITHUB_TOKEN`. ### As Applicable - [ ] `.machine_readable/STATE.a2ml` updated. Not applicable: no project-state change. (The estate also no longer writes `.a2ml` files.) - [ ] `.machine_readable/ECOSYSTEM.a2ml` updated. Not applicable, for the same reason. - [ ] `.machine_readable/META.a2ml` updated. Not applicable, for the same reason. - [ ] Documentation updated for user-facing changes. Not applicable: no user-facing change. Each Release body is the git-cliff changelog. - [ ] `TOPOLOGY.md` updated. Not applicable. - [ ] `CHANGELOG` or release notes updated. Not ticked: release notes are generated per tag by git-cliff, and no changelog file is edited. - [x] New dependencies reviewed for license compatibility. These are CI actions, not package dependencies: setup-julia, cache, upload-artifact, download-artifact and attest-build-provenance are MIT, and git-cliff-action is Apache-2.0 (GitHub `licenseInfo`). - [ ] ABI/FFI changes validated. Not applicable. ## Testing I ran the build job's steps locally, in a throwaway depot, on the `v0.1.1` tree (`git archive v0.1.1`), with Julia **1.10.10** on Linux x64: - **Registries:** General and JPR added. - **No manifest:** the tag tracks no `Manifest.toml`, and `rm -f Manifest.toml` ran anyway. - **Test:** `Pkg.instantiate(); Pkg.build(); Pkg.test()` gave `InvestigativeJournalism.jl` **174/174**, `E2E Pipeline Tests` **28/28** and `Property-Based Tests` **870/870**. That is 1072 passed, 0 failed, 0 errored, rc=0. - **SBOM:** the SBOM script, taken verbatim from the workflow, gave rc=0. `sbom.json` parses as CycloneDX 1.4, with metadata `InvestigativeJournalism 0.1.1` and 18 direct-dependency components by name (Causals, Cliodynamics, ZeroProb, DataFrames, HTTP, …). Other checks: - `actionlint .github/workflows/release.yml`: rc=0, before and after `238d922`. - `238d922` (qualified tag ref): I read the branch-before-tag order from `src/ref-helper.ts` in `actions/checkout` at the pinned SHA `8e8c483d`. This PR's runs exercise only the empty-ref path. The manual-run path is first exercised by the post-merge `gh workflow run`. That run publishes a Release, so I did not trigger it from the PR branch. - The tag tree contains every path the workflow reads: `cliff.toml`, `README.adoc`, `LICENSE`, `Project.toml` and `src/`. - `git-cliff --latest` (local 2.13.1) on this tree produces the changelog, but warns that **15 commits were skipped due to parse errors**. One commit message contains a literal `\n\n`, which shows as-is. Both are `cliff.toml`/commit-history issues that predate this PR, not workflow defects; see Notes. **Horizon:** Linux, Julia 1.10.10 and git-cliff 2.13.1, locally. CI on this PR runs the build and changelog jobs on the hosted runner. The release job, which checks the version, attests and publishes, cannot run on a PR. It is first exercised by the manual run after merge. ## Screenshots Not applicable. ## Notes for reviewers - **Publishing v0.1.1 after merge.** A manual run uses the workflow from `main` and checks out the tag, so the tag's old `release.yml` does not matter: `gh workflow run release.yml -R hyperpolymath/InvestigativeJournalism.jl -f version=v0.1.1` - **Two dependency sources.** This workflow resolves Causals/ZeroProb/Cliodynamics from JPR, as users do. `ci.yml` installs them from git. The two can drift; this PR does not change `ci.yml`. - **`cliff.toml` follow-up (not fixed here):** run `git-cliff -vv --latest` to list the 15 skipped commits, then widen `commit_parsers` or add a catch-all. - **Deferred red check: `governance / Validate Hypatia Baseline`. Tracked in #80.** - It is red on `main` too (`2cc3088`, run 37864612160). There, 28 findings are not covered by `.hypatia-baseline.json`. - This PR removes the two findings in `release.yml`, leaving 26, and adds none (job 113764445362). - It is not a required check. The only required context is `scan / gitleaks`. - Nothing is set to auto-merge. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
<!--
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
## Summary
The release workflow has failed on every tag. Run 37866715740 (tag
`v0.2.1`) failed, so Causals.jl has no GitHub Release. This PR fixes the
four defects behind that and hardens the workflow. A second, separate
commit stops tracking `Manifest.toml`; drop it on review if you prefer
to keep the file tracked.
**Commit 1: `fix(ci): make the release workflow build, attest and
publish`**
| Defect | Fix |
|---|---|
| Both upload steps pinned
`actions/upload-artifact@ea165f8d65b6db9a8b71b5c2d1a090c0daf9c8bb`, a
commit that does not exist. It is a corrupted copy of v4.6.2's
`ea165f8d65b6e75b540449e92b4886f43607fa02`. | Pinned to v7.0.1, which
SMTLib.jl already uses. |
| "Package artifacts" had no `shell:`, so `windows-latest` ran `mkdir
-p` and `tar` in pwsh. | The build job defaults to `bash`. |
| The SBOM step ran `using Pkg, JSON`. JSON is not a dependency and the
project was never instantiated. | Instantiate, read the direct
dependencies, then load JSON from a temporary environment. |
| The tracked `Manifest.toml` was written by Julia 1.13.0-alpha2
(manifest_format 2.1, with Causals listed as a path dependency of
itself). On 1.10, `Pkg.build()` fails with "Could not locate the source
code for the StyledStrings package". | Both jobs delete any committed
manifest and resolve from `[compat]`, which is how users install the
package. |
Hardening in the same commit:
- **A manual run builds the tag, not `main`.** In the build and SBOM
jobs, `actions/checkout` takes `ref: ${{ inputs.version &&
format('refs/tags/{0}', inputs.version) || '' }}`, so the tarballs match
the tagged tree that JPR registered.
- The ref is qualified as `refs/tags/` because checkout tries a bare
name as a branch before it tries a tag (`src/ref-helper.ts:52-57` at the
pinned SHA). Without the prefix, a branch with the same name as the tag
would be packaged instead.
- CodeRabbit raised this; it is fixed in commit 3 (`e536fcf`).
- On tag pushes and PRs, `inputs.version` is empty, so the ref is empty
and checkout uses the triggering ref.
- **The version is validated.** It is passed through `env:` rather than
inline `${{ }}`, must match `^v[0-9]+\.[0-9]+\.[0-9]+$`, and must
already exist as a tag (`git ls-remote --exit-code`). A typo cannot make
`action-gh-release` mint a new tag on `main`.
- **Least-privilege permissions.** `contents: read` at the top level.
The release job alone gets `contents: write`, `id-token: write` and
`attestations: write`.
- **Build provenance.** `actions/attest-build-provenance` v4.2.2 attests
`release/*`, matching SMTLib.jl's workflow.
- **The workflow tests itself at review.** A `pull_request` trigger on
this file runs the build and SBOM jobs. The release job is skipped on
PRs.
- `sha256sum -- *` (shellcheck SC2035, reported by actionlint).
**Commit 2: `chore: stop tracking Manifest.toml`**
`.gitignore:40` already lists `/Manifest.toml`, but the file has been
tracked since the first commit (`7fef2be`). CI on `main` is green only
because its `Pkg.add(url=…AcceleratorGate…)` step re-resolves the
manifest. I measured this: after that step `julia_version` reads 1.10.10
and the self-entry is gone. `STATE.a2ml` and `Dustfile.a2ml` still
describe the manifest drift. I left them as they are, because A2ML is
retired and is not edited.
No issue was open for this. I found it while checking why `v0.2.1` has
no Release.
**Commit 3: `fix(ci): check out refs/tags/<version> on a manual release
run`**
This commit qualifies the checkout ref in the build and SBOM jobs; the
first bullet under "Hardening" above explains why. CodeRabbit raised it
in review. The same fix is in hyperpolymath/SMTLib.jl#50 and
hyperpolymath/InvestigativeJournalism.jl#79.
## Type of change
- [x] 🐛 Bug fix (non-breaking change that fixes an issue)
- [ ] ✨ New feature: none. The `pull_request` trigger and attestation
serve the release path; they add no package functionality.
- [ ] 💥 Breaking change: the package source and `Project.toml` are
untouched. Commit 2 removes `Manifest.toml` from the index only.
- [ ] 🕳️ Soundness fix: not applicable, no checker or proof is involved.
- [ ] 📖 Documentation: no docs changed.
- [ ] 🧹 Refactor / tech debt: the manifest untrack is the nearest fit,
but it changes what Pkg resolves for a fresh clone, so it is not
behaviour-preserving.
- [x] 🔧 Build / CI / tooling
## 📌 New pins
**Head SHA: `e536fcf82a1709c45178547b45d874b2dbd8ed47`**
- **`actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a`**
(v7.0.1), used twice. It replaces the missing
`ea165f8d65b6db9a8b71b5c2d1a090c0daf9c8bb`.
-
**`actions/attest-build-provenance@4d101475d8b20a2381f78447822ac1eab6504dd8`**
(v4.2.2), new.
- Unchanged: checkout `3d3c42e5…`, setup-julia `fa02766e…` (v3.0.2),
julia-actions/cache `9353db09…` (v3.5.0), download-artifact `3e5f45b2…`
(v8.0.1), action-gh-release `efb35369…`.
I resolved all 14 `uses:` SHAs across this workflow and SMTLib.jl's and
InvestigativeJournalism.jl's release workflows through the GraphQL
`object(oid:)` lookup. 13 resolved to Commit objects. The 14th,
`ea165f8d65b6db9a…`, returned null, which is the positive control that
the lookup reports a missing SHA. This repo has no `actions.lock`, and
the workflow stays in block YAML: the KYAML preconditions in the
estate's AGENTS.md §2a are not met.
## How has this been verified?
- **`actionlint .github/workflows/release.yml`** passes (rc=0) after the
SC2035 fix, and again after commit 3.
- **Commit 3 (`e536fcf`, qualified tag ref).** I read the
branch-before-tag order from `src/ref-helper.ts` in `actions/checkout`
at the pinned SHA `3d3c42e5`. This PR's runs exercise only the empty-ref
path. The manual-run path is first exercised by the post-merge `gh
workflow run`, which publishes a Release, so I did not trigger it from
the PR branch.
- **Build and test on Julia 1.10.10, Linux x64**, from a fresh depot
with `Manifest.toml` removed. `Pkg.build(); Pkg.test()` passes,
including the 674 property tests. With the committed manifest, the same
command fails at `Pkg.build()` with the StyledStrings error above.
- **The SBOM script** run locally on 1.10.10 against the same tree
writes a CycloneDX 1.4 `sbom.json` with metadata Causals 0.2.1 and
components Graphs 1.15.0, Statistics 1.10.0, LinearAlgebra "stdlib",
Distributions 0.25.131 and StatsBase 0.34.13. The old `using Pkg, JSON`
form fails on an uninstantiated project.
- **This PR's own `Release` run** is the check for what I could not run
locally: the bash shell on `windows-latest`, macOS, and the pinned
actions resolving. The release job is skipped on it by design.
**Horizon:** I ran the Julia steps on Linux only, on 1.10.10. The
Windows and macOS legs, attestation, and Release creation are verified
only by CI, and Release creation only once a tag push or manual run
happens after merge.
## Checklist
- [x] My commits are **signed** (`git commit -S`). Both show `G`
locally.
- [x] I ran the project's own checks/tests locally and they pass
(1.10.10, Linux, manifest removed; see above).
- [x] New files carry the correct `SPDX-License-Identifier`: there are
no new files. `release.yml` keeps its `MPL-2.0` header.
- [x] Docs are updated, and no public claim now overstates what the code
does. The Release body now gives `gh attestation verify`, which this
workflow supports from this PR on. The stale A2ML notes are described
above.
- [x] I have not introduced a soundness hole.
## Notes for reviewers
- **After merge, publishing v0.2.1** is a manual run: `gh workflow run
release.yml -R hyperpolymath/Causals.jl -f version=v0.2.1`. It builds
the `v0.2.1` tag tree (`3bd2bac`), the same tree JPR registered.
- **Commit 2 is separable.** Without it, the workflow still works,
because it deletes the manifest before resolving. Local work on
1.10/1.11 keeps failing until the file is untracked.
- **Same broken template elsewhere.** The `using Pkg, JSON` SBOM step
appears in six other local repos (SMTLib, PolyglotFormalisms,
KnotTheory, HackenbushGames, Exnovation, BowtieRisk). SMTLib.jl gets its
own PR; the rest are recorded in `dev-notes/inbox/findings.md` for the
owner to triage, not filed as issues.
- Nothing is set to auto-merge.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX
---------
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 --> ## Summary Registers **SMTLib 0.2.2** (`01a11d29-d89a-86da-8e3a-553d114a3537`). This is the first SMTLib version with a GitHub Release. - **Tag:** `v0.2.2` on hyperpolymath/SMTLib.jl is a signed annotated tag on `126ced1`. That commit is the squash merge of hyperpolymath/SMTLib.jl#50. - **Release:** https://github.com/hyperpolymath/SMTLib.jl/releases/tag/v0.2.2, published 2026-10-09T11:35:27Z. - It carries three platform tarballs, `sbom.json` and `checksums.txt`, with build-provenance attestations. - **What is new since 0.2.1:** - the test-suite fixes for hyperpolymath/SMTLib.jl#47 (hyperpolymath/SMTLib.jl#49); - the release-workflow fix (hyperpolymath/SMTLib.jl#50); - the version bump and CHANGELOG (hyperpolymath/SMTLib.jl#51). ## Type of change Registry: a new version of a package that is already registered. No new package, no workflow change, no change to any other package. ## 📌 New pins Head SHA: **`dd12493d2745fa8bf60f4a19ccbb938f0eac6f63`** - **`S/SMTLib/Versions.toml` → `["0.2.2"] git-tree-sha1 = "ac26d7107a5e379908388f4db0a1c21cdff1d581"`.** - This is the tree of `126ced152cacc9b72f47c77c9a4ea6bd0f06d735`, the commit `v0.2.2` peels to. - Read with `git rev-parse v0.2.2^{tree}` and cross-checked with `git ls-remote … refs/tags/v0.2.2^{}`. - No action pins, `actions.lock` entries or lockfiles change. ## Changes - `S/SMTLib/Versions.toml`: add the `["0.2.2"]` entry. It is three lines; nothing else changes. - **Why no other registry file changes:** - `Deps.toml`, `Compat.toml` and `WeakDeps.toml` are each keyed `[0]`, so they already cover 0.2.2. - Between v0.2.1 and v0.2.2, `Project.toml` differs only in `version`. - `Package.toml` and `Registry.toml` are per-package, not per-version, and are unchanged. ## RSR Quality Checklist ### Required - [x] No banned language patterns: the change is three lines of TOML. - [x] SPDX headers: no new source files. `Versions.toml` is registry data and carries no header, as with every other package in this registry. - [x] No secrets, credentials or `.env` files. - [ ] CI is green: not ticked yet. CI runs on this head after the push. I will re-read the checks before calling this done. ### As Applicable — Registry Changes - [x] `Registry.toml` index: not applicable. SMTLib is already indexed (line 42), and a version entry does not touch the index. - [x] Per-package files consistent. `ci/validate.jl` passes (see Testing). - [x] Upstream package meets the quality bar: - the v0.2.2 tag push ran the release workflow on the tagged tree: Build on ubuntu, macos and windows, then SBOM; - `main` CI on `126ced1` passed all nine `test (*)` legs (Julia 1.10, 1.11 and nightly × three OSes). - [x] Upstream tag exists and matches the registered version: `v0.2.2` → `126ced1`, whose `Project.toml` says `version = "0.2.2"`. The tag signature verifies (`git verify-tag`, SSH ED25519). ### As Applicable — Documentation / Infra Changes - [ ] `.machine_readable/6a2/*.a2ml`: not applicable. A2ML is retired estate-wide, and this PR changes no project state. - [ ] `TOPOLOGY.md`: not applicable; no architecture change. - [ ] `CHANGELOG.md`: not applicable. The release notes are in SMTLib.jl's `CHANGELOG.adoc` (`[0.2.2]`). - [ ] Wiki: not applicable. ## Testing - **`julia ci/validate.jl <worktree>`** (Julia 1.12.6, RegistryCI in a throwaway depot): `VALIDATION PASSED`. - 0 custom-check errors and 0 warnings; 158 dependency pairs across 41 packages were checked. - Layer 1 reports the documented `expected_general_gap`, because the General-deps step was off. CI runs that step as best-effort. - **End-to-end install** from this branch's registry, in a fresh depot: ```julia Pkg.Registry.add("General") Pkg.Registry.add(Pkg.RegistrySpec(path=<copy of this branch>)) Pkg.activate(; temp=true) Pkg.add(name="SMTLib", version="0.2.2") using SMTLib ``` - Result: `pkgversion = 0.2.2` and installed `tree_hash = ac26d7107a5e379908388f4db0a1c21cdff1d581`. - SMTLib and AcceleratorGate precompiled and loaded. - **Release artefacts**, downloaded with `gh release download v0.2.2`: - `sha256sum -c checksums.txt` gave OK for all four files. - `gh attestation verify` returned rc=0 for each of the three tarballs. - A tampered control file returned rc=1, so the check can fail. - **Release run 37923943616:** - Attempt 1 failed at "Attest build provenance" with `error fetching tlog entry … network timeout at rekor.sigstore.dev`, a transient Sigstore outage. No Release was created. - Attempt 2, which re-ran only the failed job, succeeded. **Horizon:** I ran the validator and the install on Julia 1.12.6. This repo's CI runs the validator on 1.10, and SMTLib's own CI covers 1.10, 1.11 and nightly. Nothing is set to auto-merge. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…rdening, checklist + ultraplan corrections) (#64) ## Summary Follow-up to #63 (merged by the owner while this branch was mid-review): the three CodeRabbit review fixes that landed on the branch *after* the merge snapshot (`5c0c375`). PR #63's `CHANGES_REQUESTED` review is addressed here; nothing else changes. The methodology.a2ml wording fix is **not** included — the owner already applied their preferred wording in `5c0c375`, which is in `main` via the #63 squash. ## Changes 1. **`.github/workflows/boj-build.yml`** — CodeRabbit's Major/CWE-78 finding: `github.repository` / `github.ref_name` were interpolated into the `run:` script. They now pass through `env:` and the JSON payload is built with `jq --arg`, so no expression expansion reaches the shell or the payload string. (The `by-design:` R4 rationale from #59 is preserved.) 2. **`SMTLIB-AXIOM-PARITY-CHECKLIST.adoc`** — the INTEND "docs build verification (`docs/make.jl`)" entry pointed at the Documenter script retired in #60. It now names the supported `casket-pages.yml` site build, and records that Z3-on-ubuntu landed with #62 (CVC5 remains optional). 3. **`ULTRAPLAN-ISSUE-43.adoc`** — restore the issue/PR cross-references whose link targets were lost (#43, #47, standards#994, PRs #45/#48/#49/#50/#51), and record the post-change verification the review asked for: CI run `38044880793` with `Install Z3 (ubuntu)` green (incl. the `z3 --version` sentinel) and `Run tests` green on all 9 matrix legs — the solver-gated tests executed with Z3 on PATH rather than skipping. ## Review threads addressed - `boj-build.yml:19` (Major) — serialise refs via env + jq ✅ - `methodology.a2ml:58` (Minor) — no-solver wording ✅ (owner's `5c0c375` supersedes; `SMTContext` raises `ErrorException`, `:unknown` is a check-sat status) - `ULTRAPLAN-ISSUE-43.adoc:9` (Minor) — dangling `]` references ✅ - `ULTRAPLAN-ISSUE-43.adoc:372` (Minor) — stale `docs/make.jl` reference in the parity checklist ✅ - `ULTRAPLAN-ISSUE-43.adoc:374` (Minor) — post-change green CI run with Z3 ✅ ## Verification - No `{{…}}` template tokens, no conflict markers, `check-lock-sync` still in sync (no `uses:` changes in this PR). - `boj-build.yml` payload construction now has no string-interpolated expressions in the shell. Refs #53 (umbrella). No issue-closing keywords here — #43 closed with #63; the remaining wave items (#56 mirror, #57 Pages) await the owner's ruling. --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Summary
Ready. This was a draft until #49 merged, because the build job runs
Pkg.test()and the tests onmainfailed (#47). #49 merged at 2026-10-09 10:46Z (14da03a). The version bump, #51, merged at 10:53Z (87b5cad). This branch was then updated withmainagain (a30f268). On that head, everyReleaseandCIjob is green, and the build and SBOM now run against version 0.2.2.The release workflow has never produced a Release. Run 37866743716 (tag
v0.2.1) failed, and the repo has no Releases. This PR fixes the workflow's own defects, so that once the tests pass, a tag produces a Release.using Pkg, JSONon an uninstantiated project. JSON is not a dependency, and components were named by UUID.shell:, sowindows-latestranmkdir -pandtarin pwsh.bash.${{ github.event.inputs.version }}.env:, matched against^v[0-9]+\.[0-9]+\.[0-9]+$, and required to exist as a tag (git ls-remote --exit-code), so a typo cannot makeaction-gh-releasemint a tag onmain.Also in this PR:
main.actions/checkouttakesref: ${{ inputs.version && format('refs/tags/{0}', inputs.version) || '' }}, so the tarballs match the tagged tree that JPR registered.refs/tags/prefix matters because checkout tries a bare name as a branch before a tag (src/ref-helper.ts:52-57at the pinned SHA).72f3d5badds the prefix, after CodeRabbit raised it on the twin fix(ci): make the release workflow build, attest and publish Causals.jl#69.rm -f Manifest.toml; this repo tracks none today), so the release is tested the way users install it.contents: write, id-token: writetocontents: read. The release job keeps its own grants for attestation.pull_requesttrigger on this file runs the build and SBOM jobs at review. The release job is skipped on PRs.sha256sum -- *(shellcheck SC2035, reported by actionlint).This is the same fix as hyperpolymath/Causals.jl#69. The files differ only in names, the
julia-actions/cachepin, and the registry step.Type of change
pull_requesttrigger serves the release path only.Project.tomlare untouched.📌 New pins
Head SHA:
a30f268840a6759f3871a4f979ad81ca62498acd. This is a merge ofmain(87b5cad, #51) intod1e513c, which in turn merged14da03a(#49) into72f3d5b. Both merges were created by "Update branch" and signed by web-flow.No pins were added or changed. The workflow already used
actions/upload-artifact@043fb46d…(v7.0.1) andactions/attest-build-provenance@4d101475…(v4.2.2). All of its pins resolve to real commits through the GraphQLobject(oid:)lookup. The same lookup reported Causals.jl'sea165f8d65b6db9a…as missing, which shows it can detect a missing SHA. This repo has noactions.lock, and the workflow stays in block YAML: the KYAML preconditions in the estate's AGENTS.md §2a are not met.How has this been verified?
actionlint .github/workflows/release.ymlpasses (rc=0), both before and after72f3d5b.72f3d5b, the qualified tag ref.src/ref-helper.tsinactions/checkout, at the pinned SHA3d3c42e5.gh workflow run. That run publishes a Release, so I did not trigger it from the PR branch.sbom.jsonwith metadata SMTLib 0.2.1 and components SHA 0.7.0 and AcceleratorGate 0.1.0.a30f268:a30f268itself (head_sha), starting at 10:53:46Z or later. The two skipped runs areCreate Release, which is skipped on PRs by design, andgovernance / Validate Hypatia Baseline.Build Package (ubuntu|macos|windows-latest, 1.10),Generate SBOM, and all ninetest (*)legs.--paginate) at 10:56Z. CodeRabbit issuccessand approved; Codeac, which is not required, was still pending.Horizon: this PR's runs cover the build, SBOM and test jobs on a PR. The release job, which verifies the tag, attests and publishes, runs only on the v0.2.2 tag push.
Checklist
git commit -S). The commit showsGlocally.a30f268; see above.SPDX-License-Identifier: there are no new files.release.ymlkeeps itsMPL-2.0header.gh attestation verify, which the existing attestation step supports.Notes for reviewers
Build Package (*)andtest (*)contexts that were deferred to test: 12 pre-existing test failures surfaced once the package loads (get_statistics, evaluate &&/||, Z3 unsat core, declare_const) #47 on72f3d5bare green ona30f268, now that fix: make the test suite pass (12 failures tracked by #47) #49 is inmain.487c7ab) contains the failing tests, so building from the tag fails. Building v0.2.1 frommainafter fix: make the test suite pass (12 failures tracked by #47) #49 would ship source that matches neither the tag nor the tree JPR registered.14da03a).87b5cad). It landed before this PR, somain's CHANGELOG already names this workflow's Release. That is true only once this PR merges.v0.2.2tag. The push runs this workflow from the tagged tree, which by then contains the fixed workflow, and publishes the Release.gh workflow run release.yml -f version=v0.2.2is only a fallback.🤖 Generated with Claude Code
https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX