Skip to content

fix(census): count Ada as SPARK only when it opts in; catalogue the template's own proofs; rerun the census - #44

Closed
hyperpolymath wants to merge 3 commits into
mainfrom
claude/lucid-hopper-wvkv5e
Closed

fix(census): count Ada as SPARK only when it opts in; catalogue the template's own proofs; rerun the census#44
hyperpolymath wants to merge 3 commits into
mainfrom
claude/lucid-hopper-wvkv5e

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Nov 9, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Summary

A proof review on 2026-11-09 found two defects in the census that produce the catalogue.

  1. Plain Ada was listed as SPARK. Every .ads/.adb in a repository with a .gpr counted as SPARK, which affected 36 rows. Example: hyperpolymath/contractiles. None of its Ada sets SPARK_Mode; it has only twelve Pre/Post aspects, which nothing proves (corrected there in fix(proofs): stop claiming SPARK proofs that do not exist; make the proof scaffold compile and fail closed contractiles#74).
  2. The template's proofs were catalogued nowhere. Files the RSR template ships are set aside as boilerplate everywhere, including in hyperpolymath/rsr-template-repo itself. Its Coaptation core proof (fix(proofs): content-bearing coaptation witness; proof scaffold to PROOF-POLICY rsr-template-repo#310) therefore appeared in no row.

Tracker: metadatastician/standards#1399.

Changes

  • scripts/census/census-repo.sh:
    • An .ads/.adb file is kept only if it contains SPARK_Mode, or if the repository has an .adc configuration pragma file that sets it.
    • A .gpr is kept only when the repository has some SPARK_Mode.
    • .adc files are now census candidates.
  • scripts/census/build-rows.sh: the template exclusion no longer applies to the template itself. This covers file, hole and declaration counts.
  • scripts/census/summarise.sh: .adc counted under SPARK.
  • scripts/census/render-catalogue.sh and README.adoc: both rules are stated.
  • Regenerated from a full census run on 2026-11-09:
    • docs/catalogue/catalogue.adoc;
    • docs/catalogue/census/catalogue-rows.json and unreachable.json;
    • docs/atlas/generated/*.

Effect on the catalogue:

  • 239 rows, as before.
  • Rows listing SPARK: 36 → 23.
  • New row for hyperpolymath/rsr-template-repo: 16 files, 101 declarations, 1 policy candidate (Properties.agda has no --safe pragma on main).
  • Other rows moved because their repositories changed since the 2026-10-26 run.

RSR Quality Checklist

Required

  • Tests pass: catalogue-check and atlas-check both pass (commands under Testing).
  • Code is formatted: not applicable, there is no formatter for these scripts.
  • Linter is clean: bash -n passes on all census scripts.
  • No banned language patterns.
  • No unsafe blocks.
  • No banned functions.
  • SPDX headers: unchanged.
  • No secrets.

As Applicable

  • Documentation updated (README.adoc).

Testing

  • The full census ran on 2026-11-09 over the 462 cloneable repositories in repos.json; 36 were unreachable.
  • Both checks pass:
    • catalogue-check: render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
    • atlas-check: bun scripts/atlas/census-atlas.mjs check
  • Spot checks:
    • contractiles no longer lists SPARK.
    • Before the fix, rsr-template-repo's row had 0 files.
    • Repositories that set SPARK_Mode (for example metadatastician/cerro-torre and hyperpolymath/ambientops) keep their SPARK counts.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Rp1Fti9phnCG3qrvQJkYEh

claude added 2 commits November 9, 2026 14:47
@claude
fix(census): count Ada as SPARK only when it opts in; catalogue the t…
352af98 
…emplate's own proofs

- census-repo.sh: an .ads/.adb is kept only if it contains SPARK_Mode or
  the repo has an .adc configuration pragma file that sets it; a .gpr only
  when the repo has some SPARK_Mode. Previously any Ada file in a repo with
  a .gpr counted as SPARK (36 rows affected), e.g. contractiles, whose Ada
  has no SPARK_Mode and no contract aspects.
- build-rows.sh: the template-path exclusion no longer applies to
  hyperpolymath/rsr-template-repo itself, so the template's proofs (among
  them the Coaptation core) are catalogued in its own row instead of
  nowhere.
- summarise.sh: .adc counted under SPARK.
- README: documents both rules.

The regenerated catalogue follows in a separate commit once the full
census run completes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rp1Fti9phnCG3qrvQJkYEh
@claude
chore(catalogue): rerun the census with the SPARK and template fixes
f765383 
Full census of the 462 cloneable repositories on 2026-11-09 (36
unreachable), regenerated with `run-census.sh`'s steps, then
`catalogue` and `atlas-build`; `catalogue-check` and `atlas-check` pass.

- SPARK rows: 36 -> 23. Repos whose Ada never sets SPARK_Mode (among
  them contractiles) no longer list SPARK.
- hyperpolymath/rsr-template-repo now has its own row (16 files, 101
  declarations). build-rows.sh also applies the template exception to
  the holes and declaration counts, which still dropped them.
- render-catalogue.sh: the header states both rules.

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

coderabbitai Bot commented Nov 9, 2026 •
edited
Loading

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 15 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 a3dbe73 and 41dc551.

Files ignored due to path filters: 4

  • docs/atlas/generated/az.adoc is excluded by !**/generated/**
  • docs/atlas/generated/classes.adoc is excluded by !**/generated/**
  • docs/atlas/generated/index.json is excluded by !**/generated/**
  • docs/atlas/generated/organisations.adoc is excluded by !**/generated/**
Files selected for processing: 9

  • README.adoc
  • docs/architecture/REPOSITORY-MAP.adoc
  • docs/catalogue/catalogue.adoc
  • docs/catalogue/census/catalogue-rows.json
  • docs/catalogue/census/unreachable.json
  • scripts/census/build-rows.sh
  • scripts/census/census-repo.sh
  • scripts/census/render-catalogue.sh
  • scripts/census/summarise.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

@hyperpolymath hyperpolymath mentioned this pull request Nov 9, 2026
Open
23 tasks
@hyperpolymath
hyperpolymath marked this pull request as ready for review November 9, 2026 15:34
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 9, 2026

Copy link
Copy Markdown
Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ❌ Failed 2026-11-09T15:34:46.986683Z
We couldn’t complete this review. Comment @codex review to try again.		 f765383 Draft marked ready
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 9, 2026

Copy link
Copy Markdown

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

@claude
chore(docs): regenerate REPOSITORY-MAP.adoc (stale on main)
41dc551 
estate-rules failed on this PR with "committed REPOSITORY-MAP.adoc is
stale". The same check fails on main at a3dbe73: applied-systems/ was
added without regenerating the map. Regenerated with
scripts/gen-repo-map.sh; tests/shape/repo_map_determinism_test.sh now
passes (byte-identical across locales, committed copy current).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rp1Fti9phnCG3qrvQJkYEh
@hyperpolymath Claude

hyperpolymath commented Nov 9, 2026

Copy link
Copy Markdown
Owner Author

estate-rules failed on f765383 with "committed REPOSITORY-MAP.adoc is stale". The cause is not this PR: the same check fails on main (a3dbe73), because applied-systems/ was added there without regenerating the map.

I've carried the fix here in 41dc551: the map regenerated with scripts/gen-repo-map.sh. Locally, tests/shape/repo_map_determinism_test.sh and check-root-shape.sh both pass. The fix becomes a no-op once main regenerates its own map.

Generated by Claude Code

@sonarqubecloud

sonarqubecloud Bot commented Nov 9, 2026

Copy link
Copy Markdown

Quality Gate Passed Quality Gate passed

Issues
3 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

hyperpolymath pushed a commit that referenced this pull request Nov 10, 2026
@claude
fix(census): land the scanner fixes from the open pull requests (WO 0…
c8e1806 
….1, A)

Carries the kept code of seven open pull requests onto main, as the owner
approved row by row on 2026-11-10 (ruling D-6 (a)). Row data, repository
maps and reruns from those pull requests are not carried: main has a newer
full census. The catalogue text that describes the new rules changes at the
next full census, so it never describes rules that did not make the rows.

- build-rows.sh reads each list with FILENAME==ARGV[1]. On main an empty
  template list dropped every row (#25, a16daa7).
- Template boilerplate is a file whose (path, blob) the template shipped,
  so a repository that rewrote a template file keeps it as its own
  (design of #26, 185e6cb; test of #20, c24d989, adapted). The template
  repository owns its own files (#44, 352af98). template-blobs.tsv is
  regenerated from rsr-template-repo today (56 pairs).
- proof-holes.sh blanks comments and strings before it matches, and reports
  Idris2 signatures without clauses as axiom candidates (#27, ec833bc,
  2f0f75e).
- The census sees Rust proofs: Creusot with Pearlite, and Verus (#31,
  7b1e096, cc2bdaa), with the assume_specification rule of #34 (d35fce4).
- Ada counts as SPARK only where SPARK_Mode is on for the file or a .adc
  file (#44, 352af98).
- Status documents keep the order of main (PROOF-STATUS, proof-debt,
  PROOF-NEEDS) in one mechanism, not two; a document nested two
  directories deep ranks after every shallow one (#31).
- CI runs every tests/census/*.sh and the catalogue currency check (the CI
  step of #17, c8fc593). just census-test runs the same tests.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM
@hyperpolymath hyperpolymath mentioned this pull request Nov 10, 2026
Merged
4 tasks done
@hyperpolymath Claude

hyperpolymath commented Nov 10, 2026

Copy link
Copy Markdown
Owner Author

Closed by the owner-approved triage of WO 0.1 (2026-11-10). The SPARK opt-in rule and the template's own row landed in #51. The row data is not carried: the next full census applies the rule.

Generated by Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

Copilot code review Copilot

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hyperpolymath @claude