Skip to content

fix(ci): make the release workflow build, attest and publish - #50

Merged
hyperpolymath merged 4 commits into
mainfrom
fix/release-workflow
Oct 9, 2026
Merged

hyperpolymath merged 4 commits into
mainfrom
fix/release-workflow

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Oct 9, 2026 •

Copy link
Copy Markdown
Owner

Summary

Ready. This was a draft until #49 merged, because the build job runs Pkg.test() and the tests on main failed (#47). #49 merged at 2026-10-09 10:46Z (14da03a). The version bump, #51, merged at 10:53Z (87b5cad). This branch was then updated with main again (a30f268). On that head, every Release and CI job 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.

Defect Fix
The SBOM step ran using Pkg, JSON on an uninstantiated project. JSON is not a dependency, and components were named by UUID. Instantiate, read the direct dependencies by name, then load JSON from a temporary environment.
AcceleratorGate is registered only in the hyperpolymath registry (JPR), so a fresh runner cannot resolve the project from General alone. The build and SBOM jobs add General and JPR.
"Package artifacts" had no shell:, so windows-latest ran mkdir -p and tar in pwsh. The build job defaults to bash.
The dispatch version was inlined into the script as ${{ github.event.inputs.version }}. Passed through 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 make action-gh-release mint a tag on main.

Also in this PR:

  • A manual run builds the tag, not main. actions/checkout takes ref: ${{ inputs.version && format('refs/tags/{0}', inputs.version) || '' }}, so the tarballs match the tagged tree that JPR registered.
  • Any committed manifest is ignored (rm -f Manifest.toml; this repo tracks none today), so the release is tested the way users install it.
  • Least privilege. Top-level permissions drop from contents: write, id-token: write to contents: read. The release job keeps its own grants for attestation.
  • The workflow tests itself. A pull_request trigger 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/cache pin, and the registry step.

Type of change

  • 🐛 Bug fix (non-breaking change that fixes an issue)
  • ✨ New feature: none. The pull_request trigger serves the release path only.
  • 💥 Breaking change: package source and Project.toml are untouched.
  • 🕳️ Soundness fix: not applicable.
  • 📖 Documentation: no docs changed.
  • 🧹 Refactor / tech debt: not behaviour-preserving, since the workflow now succeeds where it failed.
  • 🔧 Build / CI / tooling

📌 New pins

Head SHA: a30f268840a6759f3871a4f979ad81ca62498acd. This is a merge of main (87b5cad, #51) into d1e513c, which in turn merged 14da03a (#49) into 72f3d5b. 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) and actions/attest-build-provenance@4d101475… (v4.2.2). All of its pins resolve to real commits through the GraphQL object(oid:) lookup. The same lookup reported Causals.jl's ea165f8d65b6db9a… as missing, which shows it can detect 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), both before and after 72f3d5b.
  • 72f3d5b, the 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 only exercise the empty-ref path.
    • The manual-run path first runs in the post-merge gh workflow run. That run publishes a Release, so I did not trigger it from the PR branch.
  • The SBOM script, run locally on Julia 1.10.10 (Linux x64, fresh depot, General plus JPR), writes a CycloneDX 1.4 sbom.json with metadata SMTLib 0.2.1 and components SHA 0.7.0 and AcceleratorGate 0.1.0.
  • Build and test are green on a30f268:
    • 32 check runs succeeded. Each one ran on a30f268 itself (head_sha), starting at 10:53:46Z or later. The two skipped runs are Create Release, which is skipped on PRs by design, and governance / Validate Hypatia Baseline.
    • The 32 include Build Package (ubuntu|macos|windows-latest, 1.10), Generate SBOM, and all nine test (*) legs.
    • Read with the REST check-runs endpoint (--paginate) at 10:56Z. CodeRabbit is success and approved; Codeac, which is not required, was still pending.
  • The Causals.jl twin (#69) exercises the shared parts (the bash shell on Windows, macOS, and action resolution) on a package whose tests pass.

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

  • My commits are signed (git commit -S). The commit shows G locally.
  • I ran the project's own checks/tests locally and they pass. Not ticked: I ran only the SBOM script locally. The tests pass in CI on a30f268; see above.
  • New files carry the correct SPDX-License-Identifier: there are no new files. release.yml keeps its MPL-2.0 header.
  • Docs are updated, and no public claim now overstates what the code does. The Release body now gives gh attestation verify, which the existing attestation step supports.
  • I have not introduced a soundness hole.

Notes for reviewers

🤖 Generated with Claude Code

https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX

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
@coderabbitai

coderabbitai Bot commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Review in Change Stack →

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration
  • Configuration used: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: 78a152e0-9462-40c7-bc75-a833156dccfb

📥 Commits

Reviewing files that changed from the base of the PR and between 14da03a and d1e513c.


📒 Files selected for processing (1)
  • .github/workflows/release.yml

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)
  • GitHub Check: scan / rust-secrets
  • GitHub Check: scan / gitleaks
  • GitHub Check: hypatia / Hypatia Neurosymbolic Analysis
  • GitHub Check: governance / Trusted-base reduction policy
  • GitHub Check: governance / Code quality + docs
  • GitHub Check: governance / Licence consistency
  • GitHub Check: governance / Language / package anti-pattern policy
  • GitHub Check: governance / Check Workflow Staleness
  • GitHub Check: governance / Security policy checks
  • GitHub Check: governance / Well-Known (RFC 9116 + RSR)
  • GitHub Check: governance / Guix primary / Nix fallback policy
  • GitHub Check: governance / Workflow security linter
  • GitHub Check: analyze (actions)
  • GitHub Check: Build Package (windows-latest, 1.10)
  • GitHub Check: Build Package (macos-latest, 1.10)
  • GitHub Check: test (nightly, windows-latest)
  • GitHub Check: test (1.11, macos-latest)
  • GitHub Check: Build Package (ubuntu-latest, 1.10)
  • GitHub Check: test (1.10, windows-latest)
  • GitHub Check: test (1.10, macos-latest)
  • GitHub Check: test (nightly, ubuntu-latest)
  • GitHub Check: test (1.11, windows-latest)
  • GitHub Check: test (1.10, ubuntu-latest)
  • GitHub Check: test (1.11, ubuntu-latest)
  • GitHub Check: test (nightly, macos-latest)
  • GitHub Check: semgrep-cloud-platform/scan

🔇 Additional comments (1)
.github/workflows/release.yml (1)

7-12: LGTM!

Also applies to: 16-16, 19-19, 29-31, 33-37, 39-40, 45-52, 54-54, 71-72, 76-78, 81-82, 84-85, 87-96, 108-108, 121-121, 130-151, 161-161, 183-183





📝 Summary

Summary by CodeRabbit

  • Chores
    • Release builds now validate version tags before publishing and include updated dependency details in software bills of materials.
    • Release checksums exclude directory entries, and release instructions now include a step for verifying attestations.
    • Manual releases require an existing tag with a version in the expected format.

Walkthrough

The 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.

Changes

Release workflow

Layer / File(s) Summary
Workflow triggers and build inputs
.github/workflows/release.yml
The workflow adds pull-request path filtering, changes workflow-level permissions, and updates build checkout and registry setup.
SBOM dependency collection
.github/workflows/release.yml
The SBOM job resolves dependencies and uses package names and versions when building its component list.
Release validation and instructions
.github/workflows/release.yml
The release job skips pull requests and validates the version and remote tag. Checksum generation and release instructions are also updated.

Priority: ➖ Normal

Estimated code review effort: 3 (Moderate) | ~20 minutes

Change: Bug fix


Merge Risk

Merge Risk: ⚪ Minimal · up to d1e51

No actionable risk introduced by this change was established. The build and test remain unconfirmed pending the separately reported prerequisite fix.

Security Architecture Review

Security architecture risk: 🔵 Low · up to d1e51

The workflow reduces credential exposure and makes manual releases more constrained. No introduced security vulnerability was established. Release-tag protection, exact provenance source binding, and recovery from concurrent or partially completed publication remain unverified.

Retained concerns
No architecture-level concerns identified.

Security review details

Security Blast Radius

  • observed — The visible privileged scope is this repository’s contents, release assets, provenance records, and OIDC issuance. The release job retains the same permission grants as the base. No external cloud-role assumption or explicit secret input appears in the workflow; external OIDC trust policies were not available.

Trust Boundaries and Controls

  • observed — Qualified tag refs prevent branch-name ambiguity during manual checkout. Environment-based input handling, version validation, and remote tag-existence checks constrain the publication target. These checks do not establish tag immutability or carry a checkout commit SHA through to publication.

Resilience and Maintainability Implications

  • observed — Build/test execution and dependency preparation have lower token authority than in the base, while publication remains separately gated. This limits the credential exposure of code executed during validation without removing the release job’s existing authority.

Hardening Proposals

  • proposed — Consider resolving the requested tag once to an immutable commit, carrying that identity through build and SBOM production, and checking publication and provenance against it. Verify the manual-dispatch provenance source identity and repository tag protections before relying on attestations as proof of the tagged source tree.



🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Docstring Coverage Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0…
Linked Issues check Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check Passed Check skipped because no linked issues were found for this pull request.
Title check Passed The title clearly and concisely summarises the main change: fixing the CI release workflow to build, attest, and publish releases.
Description check Passed The description is directly related to the workflow changes. It explains the defects, fixes, verification results, release behaviour, and planned tag-based publication.


  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

A rabbit checks the tag at dawn,
Then hops where build and tests are run.
The package names line up just right,
A checksum guards the files tonight.
The release notes show proof in sight.

Comment @coderabbitai help to get the list of available commands.

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
hyperpolymath added a commit that referenced this pull request Oct 9, 2026
## 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>
@hyperpolymath hyperpolymath mentioned this pull request Oct 9, 2026
5 of 13 tasks
@hyperpolymath
hyperpolymath marked this pull request as ready for review October 9, 2026 10:51
hyperpolymath added a commit that referenced this pull request Oct 9, 2026
<!--
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>
hyperpolymath added a commit to hyperpolymath/InvestigativeJournalism.jl that referenced this pull request Oct 9, 2026
<!--
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>
hyperpolymath added a commit to hyperpolymath/Causals.jl that referenced this pull request Oct 9, 2026
<!--
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>
@hyperpolymath
hyperpolymath merged commit 126ced1 into main Oct 9, 2026
35 of 36 checks passed
@hyperpolymath
hyperpolymath deleted the fix/release-workflow branch October 9, 2026 11:09
hyperpolymath added a commit to hyperpolymath/julia-professional-registry that referenced this pull request Oct 9, 2026
<!-- 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>
hyperpolymath added a commit that referenced this pull request Oct 10, 2026
…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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant