Repository navigation
chore: upgrade to the current RSR template (840ac25), then instantiate - #21
Merged
Merged
Conversation
occupancy-types was cut from template 05bf1b9 (tree a6fcc53, the repo's first commit tree; two blobs of that commit are absent from the read-only template clone, so the base was exported from the repo's own first commit) and never minted. Three-way upgrade: base = that tree, theirs = a fresh mint of template main 840ac25 (slug occupancy-types, identity and clade UNASSIGNED), ours = main. - Repo-authored work (Agda OccupancyTypes modules, src/julia, src/occ, src/stackcert, examples/session_ir, tests/reject, ULTRAPLAN.md, PROOF-STATUS.adoc, docs it wrote, its three workflows, scripts) is byte-identical to main. - Files the repo never changed take the current minted template, including its deletions: every old-era template .a2ml file is gone and none is created (the repo carried no .a2ml of its own). occupancy-types_chora.deed carries (canon) 2.1.5 and (provenance) main@840ac25 / tree a7e2cb8, :parent-pin = 840ac25. - Merged by hand: CITATION.cff (ORCID kept), root-allow.txt (ULTRAPLAN, PROOF-STATUS, agda-lib entries re-added), README.adoc (own text plus the template's K9 badge), Justfile (own test recipe and check/check-ir kept), CHANGELOG.adoc, .gitignore, docs/EXPLAINME.adoc, check-no-md-in-docs.sh, both proof MANIFESTs (CostStateSeparation entry kept), and the Dependabot bumps re-applied on the current workflows and actions.lock (smtp-notify 0.5.1, action-gh-release 3.0.4, sonarqube-scan 8.4.1; entries added for the repo's three workflows). - Not carried: the repo's codeql 4.38.3 bump (the template already pins 4.39.1), its standards-reusable pin bumps (the current workflows no longer call them), and julia = "1.10" in mise.toml (mise.toml is now rendered from detected languages; Julia is not detected). - LICENSE and LICENSES/ unchanged; LICENSE.adoc added byte-identical to the template's. - (variant (paths)) declares the repo's additions and divergences. - CLAUDE.md and the repository map regenerated with the current recipes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZohGxQnA5cbBZyi8Wp
The template upgrade rendered mise.toml from detected languages, and detection only finds a Project.toml at depth 1; this repo's is at src/julia/. That dropped the repo's own `julia = "1.10"`. The owner chose to keep it here and fix detection in rsr-template-repo; until that lands scripts/check-mise-language.sh reports julia as declared for no detected language. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZohGxQnA5cbBZyi8Wp
Contributor
|
Important Review skippedToo many files! This PR contains 418 files, which is 318 over the limit of 100. To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch. Upgrade to a paid plan to raise the limit. Usage-priced reviews support at most 300 files.
 |
Owner
Author
|
Expected red checks on this PR. Each one comes from a file the repo wrote, and
Any other red check is new, and I will investigate it. Generated by Claude Code |
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
|
|
||
| This Source Code Form is subject to the terms of the Mozilla Public | ||
| License, v. 2.0. If a copy of the MPL was not distributed with this | ||
| file, You can obtain one at http://mozilla.org/MPL/2.0/. |
Owner
Author
There was a problem hiding this comment.
This is not fixed here, on purpose. LICENSE.adoc line 360 is the MPL-2.0 Exhibit A text ("You can obtain one at http://mozilla.org/MPL/2.0/"), copied byte for byte from the template. Licence text is owner-only (doctrine 6), and an inline pragma would also change the licence file. The same alert appears in every repo that carries the template's LICENSE.adoc (for example czech-file-knife#15). The fix at source is for Hypatia's http_in_docs rule to skip licence files. This thread is left open for the owner's decision.
Generated by Claude Code
|
hyperpolymath
marked this pull request as ready for review
November 12, 2026 16:41
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
2 tasks done
hyperpolymath
added a commit
that referenced
this pull request
Nov 12, 2026
) ## Summary Follow-up to #21. That PR merged before its last commit arrived. This PR carries that commit, plus the gate fixes in the owner's files that the owner approved (selector, 2026-11-12: "Fix in a follow-up PR"). ## Changes 1. `chore: move the template pin to rsr-template-repo 2f54c7b` (the commit that missed #21): - Applies template commits 6c845c9 (the session-start hook) and 2f54c7b (the Sonar fixes from hyperpolymath/rsr-template-repo#343). This removes the template Sonar findings on main. - Moves `:parent-pin` and `:template-commit` to 2f54c7b, and `:template-tree` to match. - Declares `mise.toml` as diverged (it carries `julia = "1.10"`). 2. `fix: make the owner-file gates pass`: - JCS for `examples/session_ir/manifest.json` and `src/stackcert/lake-manifest.json`. - `docs/EXPLAINME.adoc`: one level-0 title. The project title replaces the template title, and "RSR template claims" becomes a level-1 section. - `docs/recon/ULTRA-PLAN-2026-10-04.adoc`: remove a stray `|===` that closed a table one row early. - `PROOF-STATUS.adoc`: name the README placeholder without the literal `{{...}}` token. No content in these files changes meaning. The edits are layout and serialisation only. ## RSR Quality Checklist ### Required - [x] No gate weakened or skipped. ### As Applicable - [x] Template pin and drift declaration updated. ## Testing All run locally on this branch: - `scripts/check-ijson-jcs.sh --enforce`: 18 of 18 canonical. - `scripts/check-adoc-renders.sh` (asciidoctor 2.0.26): all 177 tracked .adoc files render clean. - `scripts/check-no-placeholders.sh`: PASS. - `scripts/check-mint-drift.sh` against rsr-template-repo 2f54c7b: PASS, identical to a replay of the mint modulo declared variant paths. The `mise.toml` Julia line still needs hyperpolymath/rsr-template-repo#345 (Julia detection below the root) before `check-mise-language.sh` passes here. ## Screenshots Not applicable. --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZohGxQnA5cbBZyi8Wp)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
occupancy-types was cut on 2026-09-27 from template commit
05bf1b97and never minted. That template era used.a2mlmetadata and a deed with no(canon)or(provenance). The owner chose "upgrade, then instantiate" (selector, 2026-11-12). This is the same three-way upgrade as hyperpolymath/czech-file-knife#15:05bf1b97.840ac25.main.Changes
main(86 files the repo added):src/OccupancyTypes,src/julia,src/occandsrc/stackcertexamples/session_ir,tests/reject, and the repo's own scripts and testsULTRAPLAN.md,PROOF-STATUS.adoc, the agda-lib file andCostStateSeparation.leandocs/recon,docs/statusanddocs/reportslean4-manifest,proofsandsession-irworkflowsactions.lockgains records for the repo's own workflows andsetup-julia.README.adockeeps the repo's sections.Justfilekeeps the repo'stest,checkandcheck-irrecipes.CITATION.cffkeeps the ORCID.root-allow.txtkeeps the repo's entries..a2mlfiles are removed, including the repo's edited CLADE,rsr-profileand CLADE template. No.a2mlfile is created.mise.toml(commit a2e0a8d): keeps the repo'sjulia = "1.10". The template detects Julia only from a rootProject.toml, and this repo's is insrc/julia/. The owner chose to fix detection in rsr-template-repo. Until that lands,scripts/check-mise-language.shreports julia as declared for no detected language.occupancy-types_chora.deed.(canon)is 2.1.5.(provenance)and:parent-pinname840ac25(treea7e2cb8).(variant (paths))declares the repo's additions and divergences.LICENSEandLICENSES/are unchanged.LICENSE.adocis added byte-identical to the template's copy (MPL-2.0). The owner approved this file for this repo in the selector.RSR Quality Checklist
Required
As Applicable
CLAUDE.mdand the repository map are regenerated by the current recipes.Testing
Run locally after
git add -A. These pass:check-lock-sync.shcheck-root-shape.shjust validate-claude-mdjust verifycheck-mint-drift.shagainst 840ac25: "identical to a replay of the mint"use_template_mint_test.sh,chain_mint_test.shand the other estate-rules bash stepstests/scan_postulates_test.shThese still fail on the repo's own files, and
mainfails them too. The owner chose to fix them in a follow-up PR after this one:check-no-placeholders.sh: a literal{{PROJECT_NAME}}inPROOF-STATUS.adoc.check-adoc-renders.sh:docs/EXPLAINME.adocanddocs/recon/ULTRA-PLAN-2026-10-04.adoc.check-ijson-jcs.sh:examples/session_ir/manifest.jsonandsrc/stackcert/lake-manifest.json.check-mise-language.sh: the julia line, until the template fix lands.Not run, because julia, lean, idris2 and agda are not installed here: the Julia, Idris, Lean and Agda checks.
Screenshots
Not applicable.
Generated by Claude Code