Skip to content

Commit dffe78c

Browse files
Bring arithmon.com under the ledger
The overseer reaches every repo by cloning, so the one surface it could not see was the one most readers meet first: the deployed page, which is uploaded rather than committed. It now fetches each entry in SITES and flattens it to text under a pseudo-repo, which lets every existing check apply unchanged instead of being rewritten for HTML. Link targets survive the flattening so the old-namespace link check reaches the page too. Declared as the claim surface `arithmon-com.md`. Verified against the live page: seven count-shaped claims and the frozen delta_CP assertions are now read and matched against the ledger. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 parent 9753726 commit dffe78c

2 files changed

Lines changed: 68 additions & 3 deletions

File tree

LEDGER.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@
4848
},
4949
"claim_surfaces": [
5050
"README.md",
51+
"arithmon-com.md",
5152
"profile/README.md",
5253
"CITATION.md",
5354
"CITATION.cff",

scripts/arithmon-consistency-check.py

Lines changed: 67 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,10 @@
88
one README, a DOI cited nowhere else, a root module left a version behind.
99
This script clones the org's repos and checks the invariants that span them.
1010
11+
The deployed pages listed in SITES are fetched and flattened to text so that
12+
the same checks reach them. Without this, the program's most-read claim
13+
surface would be the only one nothing audits.
14+
1115
Source of truth: program/LEDGER.json (see EMBEDDED_LEDGER for the schema).
1216
If that file is absent the embedded fallback is used and a warning is emitted.
1317
@@ -23,19 +27,28 @@
2327
from __future__ import annotations
2428

2529
import argparse
30+
import html
2631
import json
2732
import os
2833
import re
2934
import shutil
3035
import subprocess
3136
import sys
3237
import tempfile
38+
import urllib.request
3339
from collections import defaultdict
3440
from dataclasses import dataclass, field, asdict
3541

3642
ORG = "arithmon"
3743
REPOS = [".github", "program", "atlas", "sieve", "lean", "k7", "k7-lean"]
3844

45+
# The program's front door is uploaded, not committed, so cloning cannot reach
46+
# it. Each entry is fetched and flattened to text under a pseudo-repo, which
47+
# lets every claim check below apply to the served page unchanged. Skipped
48+
# under --no-network. The rendered filename is what LEDGER.claim_surfaces
49+
# must list for the page to count as a claim surface.
50+
SITES = {"site": ("https://arithmon.com/", "arithmon-com.md")}
51+
3952
# Paths whose content is historical by design and must never trigger drift errors.
4053
HISTORICAL = re.compile(r"(^|/)(legacy|archive)/|CHANGELOG|/\.git/|/\.lake/|/build/")
4154

@@ -74,7 +87,7 @@
7487
# Files where a number is a *headline claim* rather than a local subsection
7588
# count. Drift checks run here only: this is what keeps the report readable.
7689
"claim_surfaces": [
77-
"README.md", "profile/README.md", "CITATION.md", "CITATION.cff",
90+
"README.md", "arithmon-com.md", "profile/README.md", "CITATION.md", "CITATION.cff",
7891
"STRUCTURE.md", "INDEX.md", "CONFRONTATIONS.md",
7992
"docs/wiki/Home.md", "docs/wiki/Home.fr.md",
8093
"docs/GIFT_EXEC_SUMMARY.md", "docs/GIFT_EXEC_SUMMARY.fr.md",
@@ -151,6 +164,48 @@ def clone_all(workdir, quiet=True):
151164
return paths
152165

153166

167+
BLOCK_TAGS = "p|div|li|tr|h[1-6]|section|article|dt|dd|blockquote|br"
168+
169+
170+
def render_page_text(src):
171+
"""Flatten a served HTML page to one line per block element.
172+
173+
Link targets are kept inline so that the link checks see them; everything
174+
else becomes plain text, because the claim checks are line-based and a
175+
number wrapped in markup would otherwise never match.
176+
"""
177+
src = re.sub(r"(?is)<(script|style)\b.*?</\1>", " ", src)
178+
src = re.sub(r'(?i)<a\b[^>]*href="([^"]+)"[^>]*>', r" \1 ", src)
179+
src = re.sub(r"(?i)<(%s)\b[^>]*>" % BLOCK_TAGS, "\n", src)
180+
src = re.sub(r"(?i)</(%s)>" % BLOCK_TAGS, "\n", src)
181+
src = re.sub(r"<[^>]+>", " ", src)
182+
src = html.unescape(src)
183+
lines = (re.sub(r"[ \t ]+", " ", ln).strip() for ln in src.splitlines())
184+
return "\n".join(ln for ln in lines if ln)
185+
186+
187+
def materialize_sites(workdir, quiet=True):
188+
"""Fetch each deployed page into a pseudo-repo. Returns {key: path}."""
189+
paths = {}
190+
for key, (url, fname) in SITES.items():
191+
dest = os.path.join(workdir, key)
192+
try:
193+
req = urllib.request.Request(
194+
url, headers={"User-Agent": "arithmon-consistency-check"})
195+
with urllib.request.urlopen(req, timeout=30) as r:
196+
raw = r.read().decode("utf-8", errors="replace")
197+
except Exception as exc:
198+
print(f" ! could not fetch {url}: {exc}", file=sys.stderr)
199+
continue
200+
os.makedirs(dest, exist_ok=True)
201+
with open(os.path.join(dest, fname), "w", encoding="utf-8", newline="\n") as fh:
202+
fh.write(render_page_text(raw))
203+
paths[key] = dest
204+
if not quiet:
205+
print(f" fetched {url}")
206+
return paths
207+
208+
154209
def resolve_local(workdir):
155210
"""Map repo names onto an existing directory of clones."""
156211
paths = {}
@@ -594,16 +649,25 @@ def main():
594649
tmp = None
595650
try:
596651
if args.local:
597-
paths = resolve_local(args.local)
652+
workdir = args.local
653+
paths = resolve_local(workdir)
598654
if not paths:
599-
print(f"no clones found under {args.local}", file=sys.stderr)
655+
print(f"no clones found under {workdir}", file=sys.stderr)
600656
return 2
601657
else:
602658
tmp = tempfile.mkdtemp(prefix="arithmon-audit-")
659+
workdir = tmp
603660
if not args.quiet:
604661
print("cloning org repos...")
605662
paths = clone_all(tmp, quiet=args.quiet)
606663

664+
if args.no_network:
665+
report.warn("coverage", "-",
666+
"deployed pages not audited (--no-network): "
667+
+ ", ".join(url for url, _ in SITES.values()))
668+
else:
669+
paths.update(materialize_sites(workdir, quiet=args.quiet))
670+
607671
missing = [r for r in REPOS if r not in paths]
608672
if missing:
609673
report.warn("coverage", "-", f"repos not available for audit: {', '.join(missing)}")

0 commit comments

Comments
 (0)