fix: repair allTake proof break; MPL-2.0 licensing; Markdown README; reconcile counts (125/68/0.4.7) by hyperpolymath · Pull Request #256 · hyperpolymath/boj-server

hyperpolymath · 2026-06-25T08:51:36Z

Summary

Three independent fixes — split for review — that lift BoJ's Glama grades and repair a real proof break that was sitting in main.

1. `fix(abi)` — duplicate `allTake` proof (`daf8129a`)

src/abi/Boj/SafetyLemmas.idr defined allTake twice (a merge artifact; both clauses prove the identical proposition, differing only in implicit-arg order), so the core boj.ipkg failed to type-check. Removed the redundant copy. Proof gate: PASS=104 FAIL=1 → PASS=105 FAIL=0; trusted base unchanged (5 sanctioned class-(J) axioms).

2. `chore(license,packaging)` — MPL-2.0, Markdown README, npm hygiene (`04cdf2fa`)

Restore MPL-2.0 in package.json (the published 0.4.7 is already MPL; the working-tree AGPL-3.0-or-later was a regression) and switch 6 sub-manifests AGPL→MPL (elixir/mix.exs, coord-tui/tray Cargo.toml, three tools/* packages). cartridges/idaptik-admin-mcp intentionally left AGPL.
Rewrite README.md as real GitHub-Flavored Markdown — it was AsciiDoc markup in a .md file, which renders garbled on GitHub/npm/Glama.
Add a files whitelist (npm tarball ~10.5 MB → ~0.9 MB); fix the main.js shebang (deno run → node) so npx runs; add .gitattributes linguist overrides so the repo stops being detected as "Zig".

3. `docs(metadata)` — reconcile counts to one source of truth (`14a43ee6`)

125 cartridges (= cartridge.json count = live boj_menu), 68 tools (45 boj_* + 23 coord_*), v0.4.7. Completed the smithery tools: table 18 → 68 (generated from the live tools/list); replaced the inflated "1041 Tools" with the honest 68; synced versions. Dated 2026-04-30 measurement snapshots, ADRs, and code line-counts were left untouched on purpose.

Verification

scripts/check-trusted-base.sh ✓ (5 axioms) · idris2 --check Boj/SafetyLemmas.idr ✓
scripts/typecheck-proofs.sh → PASS=105 FAIL=0
JS: dispatch 15/15, http_transport 26/26, path_claims 11/11 · boot_smoke ✓ on node/bun/deno (68 tools)

Notes

Docs are tagged MPL-2.0 to satisfy the repo's current single-licence pre-commit hook. Moving prose to CC-BY-SA-4.0 needs a hook + .reuse/dep5 change (tracked as a follow-up).
A pre-existing, unrelated elixir/boj-rest.service working-tree change was deliberately excluded from these commits.

🤖 Generated with Claude Code

`allTake` was defined twice in src/abi/Boj/SafetyLemmas.idr (a merge artifact); both clauses prove the identical proposition `allRec p xs = True -> allRec p (take n xs) = True`, differing only in implicit-argument order. The duplicate made the core `boj.ipkg` fail to type-check ("Boj.SafetyLemmas.allTake is already defined"), so scripts/typecheck-proofs.sh reported PASS=104 FAIL=1. Removed the redundant second copy; callers use `allTake prf` with inferred implicits, so argument order is irrelevant. The full proof gate is now PASS=105 FAIL=0, the trusted base is unchanged (5 sanctioned class-(J) axioms in SafetyLemmas), JS tests pass 52/52, and boot_smoke passes on node, bun, and deno. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

… hygiene - License: restore MPL-2.0 in package.json (the published 0.4.7 is already MPL-2.0; the AGPL-3.0-or-later in the working tree was a regression) and switch the sub-component manifests from AGPL to MPL-2.0: elixir/mix.exs, coord-tui/Cargo.toml, tray/Cargo.toml, and the three tools/* packages. (cartridges/idaptik-admin-mcp is intentionally left AGPL.) - README.md: rewrite as true GitHub-Flavored Markdown. It was AsciiDoc markup saved in a .md file, which renders garbled on GitHub/npm/Glama. Marked CC-BY-SA-4.0 (docs). README.adoc is retained as the AsciiDoc source. - package.json: add a `files` whitelist (mcp-bridge/, README.md, LICENSE, NOTICE) so the npm tarball drops from ~10.5 MB to ~0.9 MB. - mcp-bridge/main.js: shebang `deno run ...` -> `node` so the documented `npx` install actually runs under Node. - .gitattributes: linguist overrides (vendor cartridges/ and ffi/, mark docs) so GitHub stops detecting the repo as "Zig". Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

… of truth Single source of truth: 125 cartridges (= the cartridge.json count and what the live boj_menu reports), 68 MCP tools (45 boj_* + 23 coord_*), v0.4.7. - Cartridge count -> 125 across: jsr.json, smithery.yaml, ai-plugin.json, openapi.yaml, CITATION.cff, site/index.md, .github/settings.yml, Intentfile.a2ml, README.adoc, mcp-bridge/lib/offline-menu.js, and docs/{glama/CAPABILITIES,glama/RESOURCES,EXPLAINME,quickstarts/USER, developer/llm-warmup-dev,developer/llm-warmup-user,index.html}. - smithery.yaml: complete the static `tools:` table from 18 entries to all 68 (generated from the live tools/list). - docs/glama/CAPABILITIES.md: replace the inflated "1041 Tools" with the honest "68 MCP Tools" framing. - Version -> 0.4.7: smithery.yaml, mcp-bridge/lib/version.js, CITATION.cff, openapi.yaml, docs/specification/openapi.yaml. Dated 2026-04-30 measurement snapshots (ROADMAP/architecture/TEST-NEEDS), ADR records, and the "115 lines" code line-counts are intentionally left untouched (they need re-measurement, not a number swap). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

#257) The Proofs Gate is path-filtered (the `changes` job skips the heavy Idris2 type-check unless a PR/push touches `src/abi/**` etc.), so a proof break already in `main` is never re-detected — off-path PRs skip the typecheck and it reports success. This adds a weekly `schedule` trigger; on a schedule event the detect step leaves `run=true`, so the full core + every-cartridge type-check runs unconditionally against `main` and catches drift. Motivated by the duplicate `allTake` in `SafetyLemmas.idr` that sat in `main` with a green gate (fixed in #256). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…cts) - README.md: kept the pre-existing MPL-2.0 header + the branch title; dropped main's standardization-sweep duplicate (a second // CC-BY-SA-4.0 header that collided with the file's existing MPL-2.0 header and the PR's MPL-2.0 intent). - site/index.md: honoured main's deletion (#233 replaced it with the new site/index.html website). Branch's only change there was a cartridge-count bump, carried as a flag (see PR comment) rather than into the deleted file. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

hyperpolymath · 2026-06-25T09:24:34Z

Conflict resolved (merged main, pushed). Two judgment calls I made — flagging for your review:

README licence: main's standardization sweep had added a second header to README.md — // SPDX-License-Identifier: CC-BY-SA-4.0 — colliding with the file's existing  header and this PR's stated MPL-2.0 intent. I kept MPL-2.0 (the pre-existing header + the PR title) and dropped main's malformed // duplicate. If boj-server's README should actually be CC-BY-SA-4.0 per doc-policy, say so and I'll flip it — licence calls are yours.
Cartridge count (125 vs 139): this PR reconciles to 125, but main's newer website (site/index.html, added in boj-server.net website: install configurator + cartridge catalogue #233 after this branch) says 139 in 3 places. I did not force either — site/index.md was honoured-deleted (per boj-server.net website: install configurator + cartridge catalogue #233), so README now reads 125 while the site reads 139. Which is canonical? Tell me the true count and I'll make README + site agree.

- README.md + site/index.html: SonarCloud quality-gate badge. - site/.well-known/security.txt (the served one): Expires 2027, Canonical -> boj-server.net, drop bogus Hiring link (matches the root fix in #258). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The served site/.well-known/ had only security.txt; add humans.txt and ai.txt to match the repo-root set. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…render on Glama/community-health) (#260) **Fixes the raw-AsciiDoc rendering** on https://glama.ai/mcp/servers/hyperpolymath/boj-server (and GitHub community-health). The README was AsciiDoc (`README.adoc` + a `README.md` carrying raw asciidoc syntax) → consumers that render Markdown show literal `= boj-server`, `:toc:`, `[source,bash]`, `image:[]`, `link:[]`. Converts the source to GFM via pandoc (badges → clickable `[![alt](src)](link)`), keeps the CC-BY-SA-4.0 SPDX header as an HTML comment, removes the duplicate `README.adoc`. Count (115) carried verbatim; the 115/125/139 reconciliation is separate (#256). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Wires SonarCloud (SonarQube Cloud) CI analysis for boj-server. - `.github/workflows/build.yml` — the SonarCloud setup-wizard workflow (SHA-pinned `actions/checkout` + `SonarSource/sonarqube-scan-action@v8.1.0`), runs on push to `main` and PRs. Added a top-level `permissions: contents: read` for Scorecard. - `sonar-project.properties` — org `hyperpolymath`, key `hyperpolymath_boj-server`, with `sonar.exclusions` so only the analysable JS bridge + scripts are scanned (Idris2/Zig/Elixir have no SonarCloud analyser; vendored/generated/build/proof/dep trees excluded). **Prereqs (done/needed):** `SONAR_TOKEN` repo secret (added ✓); the project imported on SonarCloud with **CI-based** analysis selected (disable Automatic Analysis, or SonarCloud errors that both are running). The quality-gate badge is added to the README in #256. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-25T18:43:22Z

🔍 Hypatia Security Scan

Findings: 221 issues detected

Severity	Count
🔴 Critical	15
🟠 High	129
🟡 Medium	77

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "pages-deploy.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in pages-deploy.yml",
    "type": "missing_timeout_minutes",
    "file": "pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in push-email-notify.yml",
    "type": "missing_timeout_minutes",
    "file": "push-email-notify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

… conflict main converged on a Markdown-only README (deleted README.adoc, rewrote README.md — the Glama-crawler-driven clean-Markdown direction); the PR branch had independently kept README.adoc and rewritten README.md. Resolution: - README.adoc: accept main's deletion (Markdown-only is the intended end state). - README.md: take main's newer/fuller rewrite as the canonical body, with two fixes: * malformed licence badge URL `MPL_2.0--3.0--or--later` -> `MPL_2.0` (no such licence; `-or-later` is estate-banned). * header SPDX CC-BY-SA-4.0 -> MPL-2.0 (owner decision) to satisfy this repo's pre-commit hook (still strict MPL-2.0) and match the PR's "MPL-2.0 licensing" purpose. NB: the estate docs=CC-BY-SA split is not yet rolled into boj's hook. OPEN (pending owner notes): main's README.md says "115 cartridges" / no 0.4.7, vs the PR's reconciled 125 / 68 / 0.4.7. Left as main's values — owner to settle. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-25T19:20:31Z

🔍 Hypatia Security Scan

Findings: 222 issues detected

Severity	Count
🔴 Critical	15
🟠 High	129
🟡 Medium	78

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "pages-deploy.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in build.yml",
    "type": "missing_timeout_minutes",
    "file": "build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in pages-deploy.yml",
    "type": "missing_timeout_minutes",
    "file": "pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in push-email-notify.yml",
    "type": "missing_timeout_minutes",
    "file": "push-email-notify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

sonarqubecloud · 2026-06-25T19:21:16Z

Quality Gate failed

Failed conditions
0.0% Coverage on New Code (required ≥ 80%)

See analysis details on SonarQube Cloud

github-actions · 2026-06-25T20:08:06Z

🏁 path-claims bench

Commit f7aa483

Numbers

path-claims bench  (node v22.23.0)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    183 ms      3.67 µs/op    272.6k ops/s
  register: 100 active claims, 3 new paths              20000 iters    327 ms     16.36 µs/op     61.1k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    929 ms    185.80 µs/op      5.4k ops/s
  register: 100 active claims, 20 new paths              5000 iters    359 ms     71.98 µs/op     13.9k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    154 ms     154.3 ns/op     6.48M ops/s
  pathsOverlap: short prefix match                    1000000 iters    132 ms     132.9 ns/op     7.52M ops/s

  refresh (existing claim)                             100000 iters     11 ms     115.2 ns/op     8.68M ops/s
  list (100 active claims)                              50000 iters    273 ms      5.46 µs/op    183.1k ops/s

  (Bench numbers depend on host; use deltas across commits, not absolute values.)

Host-dependent — compare deltas across commits, not absolute values.

hyperpolymath and others added 3 commits June 25, 2026 09:21

hyperpolymath mentioned this pull request Jun 25, 2026

ci(proofs): weekly schedule so the proof gate re-checks main for drift #257

Merged

hyperpolymath enabled auto-merge (squash) June 25, 2026 09:19

hyperpolymath mentioned this pull request Jun 25, 2026

ci(sonar): SonarCloud scan workflow + project config #259

Merged

hyperpolymath and others added 2 commits June 25, 2026 10:42

chore(site): complete served .well-known set (humans.txt, ai.txt)

7d9591f

The served site/.well-known/ had only security.txt; add humans.txt and ai.txt to match the repo-root set. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

hyperpolymath mentioned this pull request Jun 25, 2026

docs(readme): convert README.adoc -> real Markdown (fix raw-asciidoc render on Glama/community-health) #260

Merged

hyperpolymath disabled auto-merge June 25, 2026 18:37

hyperpolymath enabled auto-merge (squash) June 25, 2026 18:38

hyperpolymath merged commit f914ee2 into main Jun 25, 2026
14 checks passed

hyperpolymath deleted the fix/glama-license-tables-proof branch June 25, 2026 18:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

fix: repair allTake proof break; MPL-2.0 licensing; Markdown README; reconcile counts (125/68/0.4.7)#256

fix: repair allTake proof break; MPL-2.0 licensing; Markdown README; reconcile counts (125/68/0.4.7)#256
hyperpolymath merged 7 commits into
mainfrom
fix/glama-license-tables-proof

hyperpolymath commented Jun 25, 2026

Uh oh!

hyperpolymath commented Jun 25, 2026

Uh oh!

github-actions Bot commented Jun 25, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 25, 2026

Uh oh!

sonarqubecloud Bot commented Jun 25, 2026

Uh oh!

github-actions Bot commented Jun 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented Jun 25, 2026

Summary

1. fix(abi) — duplicate allTake proof (daf8129a)

2. chore(license,packaging) — MPL-2.0, Markdown README, npm hygiene (04cdf2fa)

3. docs(metadata) — reconcile counts to one source of truth (14a43ee6)

Verification

Notes

Uh oh!

hyperpolymath commented Jun 25, 2026

Uh oh!

github-actions Bot commented Jun 25, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented Jun 25, 2026

🔍 Hypatia Security Scan

Uh oh!

sonarqubecloud Bot commented Jun 25, 2026

Quality Gate failed

Uh oh!

github-actions Bot commented Jun 25, 2026

🏁 path-claims bench

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

1. `fix(abi)` — duplicate `allTake` proof (`daf8129a`)

2. `chore(license,packaging)` — MPL-2.0, Markdown README, npm hygiene (`04cdf2fa`)

3. `docs(metadata)` — reconcile counts to one source of truth (`14a43ee6`)