chore(release): bump to 0.2.2 by hyperpolymath · Pull Request #51 · hyperpolymath/SMTLib.jl

hyperpolymath · 2026-10-09T10:49:47Z

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 test: 12 pre-existing test failures surfaced once the package loads (get_statistics, evaluate &&/||, Z3 unsat core, declare_const) #47, which landed in fix: make the test suite pass (12 failures tracked by #47) #49;
  - the release workflow fix (fix(ci): make the release workflow build, attest and publish #50).
- A new [0.2.1] section holds what the v0.2.1 tag tree already contains:
  - the UUIDv8 re-mint (fix(pkg)!: re-mint UUID as v8, bump to 0.2.1 #46), marked Breaking;
  - the load fix (fix: make SMTLib load (math.jl swap, duplicate structs) and repin julia-runtest #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 (fix(pkg)!: re-mint UUID as v8, bump to 0.2.1 #46); this PR only records it.
🕳️ Soundness fix: not applicable.
📖 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 test: 12 pre-existing test failures surfaced once the package loads (get_statistics, evaluate &&/||, Z3 unsat core, declare_const) #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 = 05a805f3….
- That is the tree of 487c7ab, the commit the v0.2.1 tag points at. fix(pkg)!: re-mint UUID as v8, bump to 0.2.1 #46's merge tree (047a2e8d…) is different.
- So 0.2.1 contains both fix(pkg)!: re-mint UUID as v8, bump to 0.2.1 #46 and fix: make SMTLib load (math.jl swap, duplicate structs) and repin julia-runtest #48.
Tests: not run locally, because no source file changes. CI runs the test (*) matrix on this PR. The suite passed 9/9 on fix: make the test suite pass (12 failures tracked by #47) #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

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.
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.
Docs are updated, and no public claim now overstates what the code does:
- The 0.2.2 release-workflow line describes fix(ci): make the release workflow build, attest and publish #50's workflow: tarballs, sbom.json, checksums.txt and provenance attestation.
- It becomes true only once fix(ci): make the release workflow build, attest and publish #50 is merged, which is why this PR is a draft.
I have not introduced a soundness hole.

Notes for reviewers

Order of steps:
1. fix: make the test suite pass (12 failures tracked by #47) #49 is merged (14da03a, 2026-10-09 10:46Z).
2. Merge fix(ci): make the release workflow build, attest and publish #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 fix(ci): make the release workflow build, attest and publish #50 is merged and main says 0.2.2. Without the first check, a tag pushed before fix(ci): make the release workflow build, attest and publish #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.ai/code/session_016XJoh8YA2sCWQmq93CF8RX

- Project.toml: version 0.2.1 -> 0.2.2. - CHANGELOG.adoc: [0.2.2] takes the test-suite fixes (#47, via #49) and 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), the load fix (#48), and the Added/Changed lines from 0.2.0, which was registered under the old UUID but never tagged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX

coderabbitai · 2026-10-09T10:49:58Z

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 53 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: b557f65b-be74-4df3-b311-a1ff47bb5707

📥 Commits

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

📒 Files selected for processing (2)

CHANGELOG.adoc
Project.toml

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

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

## 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. - The `refs/tags/` prefix matters because checkout tries a bare name as a branch before a tag (`src/ref-helper.ts:52-57` at the pinned SHA). - Commit `72f3d5b` adds the prefix, after CodeRabbit raised it on the twin hyperpolymath/Causals.jl#69. - **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 - [x] 🐛 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. - [x] 🔧 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 - [x] 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. - [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 the existing attestation step supports. - [x] I have not introduced a soundness hole. ## Notes for reviewers - **No red checks remain.** The 12 `Build Package (*)` and `test (*)` contexts that were deferred to #47 on `72f3d5b` are green on `a30f268`, now that #49 is in `main`. - **There will be no Release for v0.2.1. The first Release will be v0.2.2 (owner decision, 2026-10-09).** - Why not v0.2.1: its tag tree (`487c7ab`) contains the failing tests, so building from the tag fails. Building v0.2.1 from `main` after #49 would ship source that matches neither the tag nor the tree JPR registered. - Order of steps: 1. #49 is merged (`14da03a`). 2. The version-bump PR, #51, is merged (`87b5cad`). It landed before this PR, so `main`'s CHANGELOG already names this workflow's Release. That is true only once this PR merges. 3. Merge this PR. 4. Push a signed `v0.2.2` tag. 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.2` is only a fallback. 5. Register v0.2.2 in JPR. - 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>

## 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>

hyperpolymath mentioned this pull request Oct 9, 2026

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

Merged

6 of 12 tasks

hyperpolymath marked this pull request as ready for review October 9, 2026 10:53

hyperpolymath merged commit 87b5cad into main Oct 9, 2026
30 of 31 checks passed

hyperpolymath deleted the chore/bump-0.2.2 branch October 9, 2026 10:53

hyperpolymath mentioned this pull request Oct 9, 2026

feat(registry): register SMTLib 0.2.2 hyperpolymath/julia-professional-registry#113

Merged

7 of 12 tasks

hyperpolymath mentioned this pull request Oct 10, 2026

fix: address the CodeRabbit review leftovers from #63 (boj payload hardening, checklist + ultraplan corrections) #64

Merged

Navigation Menu

Repository navigation

chore(release): bump to 0.2.2 - #51

chore(release): bump to 0.2.2#51
hyperpolymath merged 1 commit into
mainfrom
chore/bump-0.2.2

hyperpolymath commented Oct 9, 2026

Uh oh!

coderabbitai Bot commented Oct 9, 2026 •

edited

Loading

Review limit reached

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Oct 9, 2026

Summary

Type of change

📌 New pins

How has this been verified?

Checklist

Notes for reviewers

Uh oh!

coderabbitai Bot commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

coderabbitai Bot commented Oct 9, 2026 •

edited

Loading