Skip to content

rsr: declare the capabilities and remove the vestigial modules (WO 3.2) - #75

Merged
hyperpolymath merged 2 commits into
mainfrom
claude/mathesis-wo-3-2-capabilities
Nov 11, 2026
Merged

hyperpolymath merged 2 commits into
mainfrom
claude/mathesis-wo-3-2-capabilities

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

Work order WO 3.2 (ruling D-3 (a)).

  • Declares agda, formal-proofs, bash, docs-site, governance-tier and reproducible-build in (rsr-profile :capabilities), written with scripts/deed-clause.sh.
  • Removes the modules the canon checker reported as vestigial: src/interface/ (ffi, Abi, generated, abi.ipkg, README), benches/, build/container/Containerfile, .github/workflows/rust-ci.yml, .github/workflows/release.yml.
  • Removes what belonged only to them: their actions.lock records (and the four dependency records they orphaned), the bench-check recipe, the template-bench part of tests/run_proven_suite_test.sh, the src/interface directory clause and the Containerfile file entry in the deed (ply).
  • build/just/validate.just is now the template's file (rsr-template-repo main). The seam is required only when src/interface/ exists (template fb4f67e). No local variant, no template issue opened.
  • scripts/run-proven-suite.sh: the Zig lane skips when src/interface/ffi is absent. --require-zig still fails without zig.
  • Deed (variant (paths)): :removed lists the removed paths. :diverged lists the four files changed locally.
  • Regenerated: CLAUDE.md (no change), coapt receipt, docs/architecture/REPOSITORY-MAP.adoc.

Owner decision

rust-ci.yml was the only CI that ran tests/workflows/archetype_lock_merge_test.sh and compiled scripts/*.rs. The owner chose to remove it (selector answer: remove). merge-actions-lock.rs is used by the mint recipe and now has no CI check. The other two Rust tools are still tested by mint_cleanup_test.sh in estate-rules.yml.

Required contexts

scripts/check-required-contexts.sh passes. The only required context is scan / gitleaks (secret-scanner.yml), which is untouched. No removed job is required.

Results observed in this session

just 1.56.0 and Nickel 1.18.0 came from release archives. The just archive matched the SHA-256 in mise.lock. The Nickel binary matched 9cba4dd6...8318cb.

Check Result
Canon checker (standards main e2a03dc), check-rsr-profile.sh No VESTIGIAL rows left. Baseline rows satisfied. The final live-Actions step failed with HTTP 403 from the proxy, so the script's exit status is an error, not a pass.
just validate-rsr PASS
Deed lint (STANDARDS_DIR=<standards> bash .github/hooks/validate-deed.sh) passed, 0 failing
just validate-state valid
just validate-claude-md OK
just validate-coapt OK (band green)
just validate-repo-map up to date
just census-test PASS
tests/workflows/deed_clause_test.sh PASS
scripts/check-lock-sync.sh in sync, no unreferenced records
tests/run_proven_suite_test.sh, tests/proven_suite_test.sh (130 passed), validate_workflows_test.sh, container_kyaml_test.sh, runtime_policy_fold_test.sh, squabble_gate_test.sh, check_root_shape_test.sh pass

Not run: just check-proofs (no Guix and no provers in this container; CI only). Other CI workflows were not run locally.

Left in place on purpose (doctrine 7)

  • scripts/check-bench-regression.sh, compute-bench-baseline.sh, bench-stats.jq: the checker did not name them, and tests/proven_suite_test.sh tests them on their own.
  • The rest of build/container/ (compose, stapeln). compose.yaml still names build/container/Containerfile as its dockerfile. The owner may want to remove or fix that.
  • verification/proofs/idris2/ and tlaplus/ (WO 4.1). The Idris2 ABI directory there is the template example proof. The ABI-1 to ABI-5 obligations in PROOF-NEEDS.adoc and PROOF-STATUS.adoc were not removed: they belong to those example proofs, not only to the removed seam. Please decide in WO 3.4 or 4.1.
  • References in prose and tooling to the removed paths: .machine_readable/configs/eclexiaiser.toml sources, scripts/validate-template.sh, docs/developer/ABI-FFI-README.adoc, .cursorrules and similar agent files, docs/status/TEST-NEEDS.adoc, the Zig entry in the deed's :allowed list, and .hypatia-ignore.
  • validate.just now also carries the template's two other upstream changes (canonical-name check, closed phase and level sets). They pass here.

Generated by Claude Code

Declare agda, formal-proofs, bash, docs-site, governance-tier and
reproducible-build in (rsr-profile :capabilities). Remove the seven modules
the canon checker reported as vestigial: src/interface/, benches/,
build/container/Containerfile, rust-ci.yml and release.yml, with their
actions.lock records, the bench-check recipe and the bench lane test.

Port the validate-rsr seam block from rsr-template-repo (re-converge with
upstream): the Idris2/Zig seam is required only when src/interface/ exists.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZomaRdNhtZ12Bx8KZi
@coderabbitai

coderabbitai Bot commented Nov 11, 2026 •

Copy link
Copy Markdown

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

Commits

Reviewing files that changed from the base of the PR and between b2cf524 and ad568ab.

Files ignored due to path filters: 3

  • .github/workflows/actions.lock is excluded by !**/*.lock
  • src/interface/generated/README.adoc is excluded by !**/generated/**
  • src/interface/generated/abi/README.adoc is excluded by !**/generated/**
Files selected for processing: 25

  • .github/workflows/release.yml
  • .github/workflows/rust-ci.yml
  • Justfile
  • benches/baseline.json
  • benches/template_bench.sh
  • build/container/Containerfile
  • build/just/validate.just
  • docs/architecture/REPOSITORY-MAP.adoc
  • mathesis_chora.deed
  • scripts/run-proven-suite.sh
  • src/interface/Abi/Foreign.idr
  • src/interface/Abi/Layout.idr
  • src/interface/Abi/README.adoc
  • src/interface/Abi/Types.idr
  • src/interface/README.adoc
  • src/interface/abi.ipkg
  • src/interface/ffi/README.adoc
  • src/interface/ffi/build.zig
  • src/interface/ffi/src/README.adoc
  • src/interface/ffi/src/main.zig
  • src/interface/ffi/test/README.adoc
  • src/interface/ffi/test/integration_test.zig
  • tests/ffi_strings_test.sh
  • tests/proven_suite_test.sh
  • tests/run_proven_suite_test.sh
  • 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

tests/ffi_strings_test.sh copied src/interface/ffi, which WO 3.2 removed.
CI has zig, so the proven-suite lane failed. Remove the test and its call in
tests/proven_suite_test.sh. Record both in (variant (paths)).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZomaRdNhtZ12Bx8KZi
@sonarqubecloud

Copy link
Copy Markdown

@hyperpolymath
hyperpolymath marked this pull request as ready for review November 11, 2026 17:01
@chatgpt-codex-connector

Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

@hyperpolymath
hyperpolymath merged commit ac6c3f8 into main Nov 11, 2026
46 checks passed
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.

3 participants