diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 65c47a25..3a152e54 100644 --- a/.claude/skills/elfuse-conventions/SKILL.md +++ b/.claude/skills/elfuse-conventions/SKILL.md @@ -1,6 +1,6 @@ --- name: elfuse-conventions -description: elfuse conventions that are not guessable from the code - the seven-rule commit message style, ASCII-only source comments, kebab-case filenames, the type and return conventions at the ABI boundary, the untracked root working docs, and the rule that a tool checked out for evaluation never becomes a build dependency. Use when drafting a commit message or PR description, adding a new file or a new type, or wiring the build to anything a fresh clone would not have. +description: elfuse conventions that are not guessable from the code: the seven-rule commit message style, ASCII-only source comments, kebab-case filenames, the type and return conventions at the ABI boundary, the untracked root working docs, and the rule that a tool checked out for evaluation never becomes a build dependency. Use when drafting a commit message or PR description, adding a new file or a new type, or wiring the build to anything a fresh clone would not have. --- # elfuse conventions @@ -18,27 +18,74 @@ reads as authoritative. ## Working docs -The repo root carries per-developer working docs that are deliberately -untracked: `CLAUDE.md`, `spec.md`, and a few others alongside them. Never -`git add`, commit, stage, gitignore, or delete any of them. They stay -untracked but visible in `git status`. This applies to `CLAUDE.md` itself. - -`spec.md` holds the full coding conventions and wins where it and this file -disagree, but it does not survive a fresh clone. That is why the load-bearing -subset is duplicated below rather than referenced: on a clean checkout, `docs/` -and these skills are all a contributor gets. +A contributor may keep untracked working docs at the repo root or under +`.claude/`; which ones exist differs per clone. Never `git add`, commit, +stage, gitignore, or delete another person's: untracked but visible in +`git status` is deliberate. None of them survive a fresh clone, so nothing +here defers to one; the load-bearing conventions are written out below, +because on a clean checkout `docs/` and these skills are all a contributor +gets. ## Style -Source comments and commit messages are ASCII only, no markdown syntax: no em -dashes, no inline backticks, no non-ASCII arrows. Use `-`, `--`, or `:` -instead of an em dash. Write code, path, and symbol references as plain text -(EPOLL_CTL_MOD, tests/foo.c). - -This rule covers `src/` comments, `tests/` comments, and commit messages. -Markdown files are exempt and use normal GitHub Markdown: the working docs, -`AGENTS.md`, and these skill files. Do not strip backticks out of a `.md` file -in the name of this rule. +Source comments and commit messages are ASCII only, with no markdown syntax: +no inline backticks, no non-ASCII arrows. Write code, path, and symbol +references as plain text (EPOLL_CTL_MOD, tests/foo.c). Markdown files are +exempt and use normal GitHub Markdown, so do not strip backticks out of a +`.md` file in its name. + +The em dash (U+2014) is banned on every surface, markdown included: comments, +commit messages, `docs/`, these skill files, PR bodies, and review replies. +In an otherwise-ASCII tree it is the clearest mark of machine-written prose, +rejected on sight (PR#209). The stand-in is ` -- ` (spaced double hyphen), +used sparingly: reword first (commas, a period, or a colon usually serve), +and more than one in a paragraph means restructure. Write the character as +its codepoint, never the glyph, so `grep -rnP '\x{2014}'` stays a clean +check; `-P` with the codepoint is required, since `grep $'\u2014'` +matches nothing and reports a false all-clear. + +The rest of the machine register is banned on the same surfaces. State the +fact and stop: + +- Describe the thing, not the change: no "previously", "now we", "we + refined", or "fixed", and no history of prior attempts or review rounds. + A decision that still matters is present-tense rationale. +- Inflation words ("delve", "seamless", "robust", "leverage") and empty + pivots ("it's worth noting"): a sentence that survives deleting the phrase + never needed it. +- Coined vocabulary, figurative accounting, and anthropomorphism: every + noun for a mechanism is an identifier in the tree or the standard term + from a man page, ELF or FUSE clause, or kernel source, and a value is + computed, cached, discarded, or re-derived. Name the flag or function + carrying the fact; a coined word cannot be grepped later. +- Trailing "-ing" glosses (", ensuring ..."): the tail names a checkable + mechanism or goes. +- Negative parallelism ("not X, but Y"): say Y. Copula avoidance ("serves + as", "acts as"): write "is". +- Rule-of-three padding, stacked transitions ("Moreover"), wrap-ups ("In + conclusion"), hedge stacking ("could potentially"): cut; one hedge at + most, for real uncertainty. +- Signposting, prompt echo, and the closing verdict: no announcement of what + the text is about to do ("This commit will", "Below we describe"), no + first line restating the subject or the PR title, and no closing sentence + grading the change ("this makes the code more maintainable"). The last + sentence carries a fact. +- Effort and flattery: "carefully reviewed", "comprehensive", "thoroughly + tested", "Great catch", "You're absolutely right". Effort is not a + finding; name what ran and what it reported. +- Formatting as emphasis in docs and PR text: bolded bullet-header runs + where a paragraph belongs, decorative rules, emoji. +- Machine artifacts, defects on sight: zero-width and bidi characters, + homoglyphs, non-standard spaces, unfilled placeholders, leaked citation + markup. Legitimate Unicode lives in `docs/` (the casefold tables), so scan + the invisible class only, with a planted positive: + + ``` + grep -rnP '[\x{00A0}\x{200B}-\x{200F}\x{202A}-\x{202F}\x{2060}\x{FEFF}]' src/ tests/ docs/ + ``` + +Every class above binds every surface, so the sections below name only +their own instance of one. Comments and commit messages are third-person: name the subject (the caller, this function) or use imperative phrasing. @@ -87,6 +134,57 @@ module. New C tests are `tests/test-.c` and use the shared harness macros rather than rolling their own reporting. +## Comments + +Brevity is part of correctness. Default to no comment; a survivor is cut to +its rationale, usually one to a few dense lines. A block growing toward a +paragraph stack is rejected even when every sentence is true ("Avoid long +comments!", PR#290, on a 28-line test header; "Shorten the comments +slightly.", PR#254, PR#261). An unrequested comment, log line, defensive +check, or restructuring is a defect to remove, not a favor. + +A comment earns its place only for what the code cannot say: rationale, an +invariant, a boundary condition, a unit, a citation. Delete anything +restating the statement below it. + +- Bad: `slot->refcount = 1; /* set refcount to 1 */` +- Good: `slot->refcount = 1; /* held by the /dev/fuse fd itself */` + +Cite the authority at the point of use: the kernel path, the man page with +its section, the ELF or FUSE clause, the macOS or glibc behavior forcing a +host workaround. Code that looks wrong says why it is not, the highest-value +comment here. Never comment around bad code; rewrite it. Contracts, +invariants, and lock ordering live once in the owning `.h`; call sites cite +them. `sigwait()` returns on SIGUSR2 and no "doorbell" rings: a thread, +flag, or helper is named for its operation, not the manner. + +Not in `src/`: attribution, dates, commented-out code, issue-tracker numbers +(barred from `docs/` and README prose too, PR#40, PR#223; they belong in a +commit trailer), or `TODO`/`FIXME`; incomplete work belongs in the commit +message or PR. Editing part of a comment re-opens all of it: re-read the +block and rewrite what no longer reads cleanly. + +Mechanics: `/* */` only in `.c`, `.h`, and `.S`, no `//`, no Doxygen tags; +multi-line blocks align on ` * `, close with `*/` on its own line, indented +to the body; American English; `@name` references a parameter in prose. A +new file opens with title, copyright, SPDX identifier, a blank `*` line, +then one prose paragraph on what the module is for (`src/syscall/signal.h` +is the model). `#` comments in shell, Python, and Make obey the same rules. +Update or delete a comment in the commit that changes its code: a stale +comment is worse than none, because it is believed. A comment asserting a +number or a guarantee is the case that rots silently, so recompute it before +carrying it into an edit; `elfuse-refactor` reads the same rule from the +reviewer's side. + +## docs/ + +`docs/` describes how the system works now, for a reader who has never seen +it, as settled fact, and a past decision that still matters reads as +present-tense rationale ("paths are translated in one place so ..."). No +workflow reads markdown, so nothing checks any of this against the code; a +docs claim is only as true as the last person who read it against the +source. + ## Vendored tools checked out for evaluation A third-party tool checked out into an untracked directory to be tried out is @@ -141,27 +239,56 @@ no area tag, no ticket number in the subject. The subject is a sentence about behavior. A commit that removes something says what stops happening; a commit that adds a proof says what is now proved. -The body is where the reasoning goes, and it is expected to be substantial for -anything non-mechanical: what the old code claimed, why that was wrong, what -breaks if you do it the obvious other way. Some commits label body paragraphs -(`Verified:`, `Coverage:`, `Concurrency:`) when a specific claim needs to be -findable later. Issue references go at the end as `Fixes #187`, `Closes #156`, -or the full URL form. - -The ASCII and third-person rules above apply here too: no backticks around -symbol names, no em dashes, no non-ASCII arrows. +The body is where the reasoning goes: what the old code claimed, why that +was wrong, what breaks if you do it the obvious other way. Substantial is +not the same as long: the target is the shortest faithful account, no +restating of the diff, no padding to look thorough. Two to four sentences +carry most commits; a body past roughly 50 lines is the signal to split the +commit, not to write more. Some commits label body paragraphs (`Verified:`, +`Coverage:`, `Concurrency:`) when a claim needs to be findable later. Issue +references go at the end as `Fixes #187`, `Closes #156`, or the URL form. + +Subject and body name code objects and mechanisms, so every claim is +checkable against the diff: "Remove unread probe outputs and unreachable +arms", never "Drop dead weight from the probe". A diagram replaces prose +rather than joining it, so interleaved actors, a race window, or a +byte-layout off-by-one earn a small ASCII diagram inside 72 columns with +real names, the prose it replaces cut. Verify it as rendered. + +The Style rules above bind here: the register classes, ASCII with no +backticks around symbol names, no em dashes or non-ASCII arrows, and third +person throughout. Merge commits keep git's generated subject and are exempt. +## Pull requests + +A PR thread is human collaboration, and agent-shaped artifacts are rejected +on sight: no pasted walkthroughs or summaries ("We are humans. Don't copy +agent-specific reply here.", PR#116), no severity or status tables ("We're +here to discuss and improve the software together, not to act as task +trackers.", PR#90), no re-summarizing the diff git already shows. Close +addressed threads with "Resolve conversation"; a reply carries the +correction, the measurement, or nothing. A concise what and why belongs in +the commit body, not the thread. + +The body is intent plus reproduction and commands: for a bug, a minimal +reproduction with host macOS and SDK version, hardware, and `make check` +status (PR#21, PR#41); for a performance claim, A/B benchmarks on a named +machine, same binary with and without the change, median over runs (PR#203). +Rebase on latest `main` (PR#58). One issue per bug (PR#135); validate +against a real application, not only a unit smoke test (PR#191). + ## Layout All source under `src/`, artifacts under `build/`. The build passes `-Isrc`, so headers are included as `core/guest.h`, `syscall/internal.h`, `proved/gva.h`. -Reports and analyses go in `claudedocs/` (ignored via `.git/info/exclude`, -which is local to the clone, so never `git add` it), tests in `tests/`, -scripts in `scripts/`. +Tests in `tests/`, scripts in `scripts/`. Reports and analyses stay out of +the tree: keep them in a scratch directory or in a repo-root directory the +clone excludes through `.git/info/exclude`, never through `.gitignore`, which +would push one person's habit onto everybody. Build and toolchain requirements are in `docs/testing.md`, section "Build Requirements". They belong to a machine, not to this convention set. diff --git a/mk/help.mk b/mk/help.mk index f24445ce..3a796a0c 100644 --- a/mk/help.mk +++ b/mk/help.mk @@ -4,7 +4,7 @@ ## Display this help message help: - @printf "$(BLUE)elfuse — aarch64-linux ELF executor on macOS Apple Silicon$(RESET)\n\n" + @printf "$(BLUE)elfuse: aarch64-linux ELF executor on macOS Apple Silicon$(RESET)\n\n" @printf "$(GREEN)Usage:$(RESET) make [SIGN_IDENTITY=\"...\"]\n\n" @printf "$(GREEN)Targets:$(RESET)\n" @awk '/^[a-zA-Z\-\_0-9%:\\]+:/ { \ diff --git a/mk/tests.mk b/mk/tests.mk index 83bb1d66..a500dc72 100644 --- a/mk/tests.mk +++ b/mk/tests.mk @@ -7,7 +7,7 @@ # src/elfuse-limits.h. ELFUSE_HOST_NOFILE_MIN ?= $(shell bash "$(CURDIR)/tests/test-config.sh" --host-nofile) -.PHONY: test-hello test-all check check-syscall-coverage test-gdbstub test-coreutils test-busybox \ +.PHONY: test-hello test-all check check-syscall-coverage check-skill-refs test-gdbstub test-coreutils test-busybox \ test-static-bins \ test-dynamic test-dynamic-coreutils test-glibc-dynamic \ test-glibc-coreutils test-perf \ @@ -68,6 +68,11 @@ test-mremap-tail-emfile: $(ELFUSE_BIN) $(BUILD_DIR)/test-mremap-tail-emfile check-syscall-coverage: @python3 scripts/check-syscall-coverage.py +## Verify every path, target, and section the skills name still resolves +check-skill-refs: + @python3 scripts/check-skill-refs.py --self-test + @python3 scripts/check-skill-refs.py + define RUN_OPTIONAL_SKIP77 @set -e; \ rc=0; \ @@ -201,7 +206,7 @@ check-sanitizer: $(ELFUSE_BIN) $(TEST_DEPS) $(CHECK_HOST_UNIT_BINS) $(CHECK_SHARED_LANES) ## Run the unit test suite plus busybox applet validation -check: $(ELFUSE_BIN) $(TEST_DEPS) check-syscall-coverage test-config \ +check: $(ELFUSE_BIN) $(TEST_DEPS) check-syscall-coverage check-skill-refs test-config \ $(CHECK_HOST_UNIT_BINS) @bash tests/driver.sh -e $(ELFUSE_BIN) -d $(TEST_DIR) -v $(CHECK_SHARED_LANES) diff --git a/scripts/check-skill-refs.py b/scripts/check-skill-refs.py index 5a48e4ec..1203305d 100755 --- a/scripts/check-skill-refs.py +++ b/scripts/check-skill-refs.py @@ -1,62 +1,52 @@ #!/usr/bin/env python3 """Fail when a skill file points at something that no longer exists. -The files under .claude/skills/ are working summaries. Every one of them says -so, and every one closes by naming the tracked file that wins when the two -disagree. That structure only works while the pointers resolve: a reference to -a renamed source file, a deleted make target, or a docs section that has been -retitled does not read as stale, it reads as authoritative and sends the -reader somewhere that does not exist. - -This is the failure mode a careful read does not catch. The reference that -prompted this script named src/syscall/sidecar.c, which had been split into -casefold.c and casefold-walk.c; the sentence around it was still true, the -file name was not, and it survived review by a human and by two agents. -Nothing else in the tree checks it, because the skills are documentation and -documentation has no compiler. +The files under .claude/skills/ are documentation, so nothing else in the +tree checks them, and a rotted pointer does not read as stale, it reads as +authoritative. The reference that prompted this script named +src/syscall/sidecar.c long after that file was split into casefold.c and +casefold-walk.c, and it survived review. What is checked, per file: 1. Frontmatter: name matches the directory, description is non-empty. - 2. Backticked path-like tokens resolve: exactly one file in the tree ends - with the path as written. Two files ending that way is a failure too, - because the reference is ambiguous and wants a longer path. + 2. Backticked paths resolve, to exactly one file in the tree or one + beside the skill itself, which is how references/*.md is written. Two + matches fails as well, since the reference is ambiguous and wants a + longer path. A path inside a fenced block carries no backticks, so it + needs a directory component to be recognized. 3. "make " names a target the makefiles define, including the - verify- targets that mk/analysis.mk instantiates from a template. - 4. A quoted section name attached to the word "section" exists as a heading - in the docs file nearest it. - 5. A cross-reference to a sibling skill names a skill that exists. - -Only typeset references are checked: a path in backticks, a make command in -backticks or in a fenced block. A file named in running prose, or in the -frontmatter description, is invisible here by design, because the alternative -is guessing which words are meant to be paths. - -Three more things are deliberately not checked. Whether the prose is true: a -pointer that resolves can still describe behavior that changed, and this -catches only the mechanical half, which is the half that rots silently. A bare -markdown name at the repo root, which may be a per-developer working doc that -no clone carries; see unverifiable() for why that stays out of the script -rather than becoming a list of somebody's private filenames. - -The compact "fd.c/h" shorthand for a pair of files is rejected rather than -ignored. Nothing here can resolve it, so allowing it would leave a reference -that looks checked and is not. - -The skills are per-developer files today and may be absent. A missing -.claude/skills/ is not a failure, it is a clone that does not carry them, and -this exits 0 with a note so the check can be wired into a build without -becoming a dependency on untracked files. + verify- targets mk/verify.mk instantiates from a template. + 4. A quoted section name attached to the word "section" exists as a + heading in the docs file nearest it. + 5. A named sibling skill exists. + +Only typeset references count: a path in backticks, a make command in +backticks or in a fenced block. Guessing which words in running prose are +meant to be paths costs more than it catches. + +Two things stay unchecked on purpose: whether the prose is true, since only +the mechanical half rots silently, and a bare markdown name at the repo +root, which may be a per-developer working doc (see unverifiable()). The +"fd.c/h" shorthand for a file pair is rejected rather than ignored, since +allowing it would leave a reference that looks checked and is not. + +A missing .claude/skills/ exits 0 with a note, so a build can call this +without depending on files a clone may not carry. Usage: check-skill-refs.py [file ...] check-skill-refs.py --self-test -Every file under .claude/skills/ is checked. Any extra file named on the -command line is checked the same way, which is how a local routing document -that points at the skills gets covered without this script having to know it -exists. --self-test asserts this script still rejects each class of stale -reference; see self_test() for why that is not optional. +Every SKILL.md and references/*.md under .claude/skills/ is checked, plus +any file named on the command line, which is how a local routing document +gets covered without this script knowing it exists. + +--self-test reads no skill file at all. It writes synthetic skills whose +references are known broken and requires check_file() to reject each one. +Nothing else separates "nothing is stale" from "nothing is checked": a +pattern that has stopped matching prints the same clean line as a tree where +everything resolves. make check-skill-refs runs both modes, self-test first. """ import functools @@ -69,9 +59,8 @@ ROOT = pathlib.Path(__file__).resolve().parent.parent SKILL_DIR = ROOT / ".claude" / "skills" -# Directories that hold no source this tree owns. externals/ is vendored for -# evaluation and gitignored; a reference resolving into it would be a false -# pass on a machine that happens to have it checked out. +# externals/ is gitignored, so a reference resolving into it would pass on the +# machine that has it checked out and fail everywhere else. PRUNE = {".git", "build", "externals", "node_modules", ".claude", ".agents"} PATH_EXTS = ("c", "h", "S", "md", "tbl", "py", "sh", "mk", "yml") @@ -79,41 +68,51 @@ # elfuse-prefixed names that are test-matrix lanes rather than skills. LANES = {"elfuse-aarch64", "elfuse-x86_64"} -# Headers the macOS SDK or the compiler supplies. The skills name them as the -# things Frama-C cannot model, so they must not resolve in tree. The shape is -# narrow on purpose: exempting everything under sys/ would wave through a -# stale sys/anything.c as well. +# Headers the SDK supplies, named by the skills as what Frama-C cannot model, +# so they must not resolve in tree. Narrow on purpose: exempting all of sys/ +# would wave through a stale sys/anything.c too. SYSTEM_HEADER_RE = re.compile(r"^(?:sys|Hypervisor)/[A-Za-z0-9_-]+\.h$") -# The leading dot matters: dot directories carry real references, .github for -# the CI job that enforces the proof targets and .claude for the skills -# themselves, and a pattern anchored on an alphanumeric first character skips -# exactly the references that break when either one moves. The trailing group -# drops a shell-function suffix such as test-runner.sh::run. +# The leading dot matters: .github and .claude carry real references, and a +# pattern anchored on an alphanumeric would skip exactly those. The trailing +# group drops a shell-function suffix such as test-runner.sh::run. PATH_RE = re.compile( r"`(\.?[A-Za-z0-9_][A-Za-z0-9_./+-]*\.(?:" + "|".join(PATH_EXTS) + r"))(?:::[A-Za-z_][A-Za-z0-9_]*)?`" ) -# A make target is only a reference when it is typeset as one: backticked -# inline, or a command line inside a fenced block. Plain prose says things like -# "no make target may reference it", and treating that as a target name is how -# a checker earns the reputation that gets it disabled. +# A make target counts only where it is typeset: backticked, or a command line +# in a fenced block. Prose says things like "no make target may reference it", +# and reading that as a target name is how a checker gets switched off. Both +# fenced patterns tolerate any leading whitespace, since a fence inside a +# numbered step is indented to that step's content column, and further still +# one list deeper. MAKE_RE = re.compile(r"`make ([a-z][a-z0-9-]*)") -MAKE_FENCED_RE = re.compile(r"^make ([a-z][a-z0-9-]*)", re.M) -FENCE_RE = re.compile(r"^```.*?^```", re.M | re.S) +MAKE_FENCED_RE = re.compile(r"^[ \t]*make ([a-z][a-z0-9-]*)", re.M) +FENCE_RE = re.compile(r"^[ \t]*```.*?^[ \t]*```", re.M | re.S) + +# Fenced paths carry no backticks, so PATH_RE cannot see them. Requiring both a +# directory component and a known extension keeps this off ordinary words and +# off build/elfuse. +FENCED_PATH_RE = re.compile( + r"(? from a template, so those names - exist only after make expands it. print-verify-targets is the list make - itself reports, which is what CI consumes. + mk/verify.mk instantiates verify- from a template, so those exist + only after make expands it; print-verify-targets is the list make reports. """ names = set() for mk in [ROOT / "Makefile"] + sorted((ROOT / "mk").glob("*.mk")): @@ -238,9 +224,7 @@ def make_targets(): def headings_of(doc): """Heading text of a docs file, backticks stripped, or None if absent. - Cached because a docs file is cited from several sentences and several - skills, and re-reading internals.md per citation is the only part of this - script that would notice. + Cached because one docs file is cited from many sentences and many skills. """ path = ROOT / doc if not path.exists(): @@ -252,8 +236,8 @@ def headings_of(doc): def check_frontmatter(path, raw): """A skill's declared name has to match the directory that carries it. - Claude Code loads a skill by directory; a drifted name means the file is - silently not the skill it says it is, which no reader would notice. + Claude Code loads a skill by directory, so a drifted name means the file + is silently not the skill it says it is. """ if path.name != "SKILL.md": return [] @@ -270,8 +254,26 @@ def check_frontmatter(path, raw): return messages -def check_paths(text, paths): - """Every backticked path names exactly one file in the tree.""" +def local_bases(path): + """Directories a skill's own pointers resolve against. + + A skill writes references/x.md from SKILL.md and from a sibling under + references/, so both the file's directory and the skill root are tried. + The skills directory is third, which is what lets one skill cite + elfuse-verify/SKILL.md. + """ + parent = path.parent + root = parent.parent if parent.name == "references" else parent + return [parent, root, SKILL_DIR] + + +def check_paths(text, raw, paths, bases): + """Every typeset path names exactly one file in the tree. + + @bases are the directories a skill's own references/*.md pointers resolve + against. .claude stays pruned from the tree walk, so nothing unrelated can + satisfy one by accident. + """ messages = [] for token in sorted(set(SHORTHAND_RE.findall(text))): names = token.split("/") @@ -279,20 +281,25 @@ def check_paths(text, paths): spelled = " and ".join(f"`{stem}.{ext}`" for ext in [names[0][-1]] + names[1:]) messages.append(f"writes {token}, which nothing resolves; write {spelled}") - for token in sorted(set(PATH_RE.findall(text))): - if unverifiable(token) or (ROOT / token).exists(): + tokens = set(PATH_RE.findall(text)) + for block in FENCE_RE.findall(raw): + tokens.update(FENCED_PATH_RE.findall(block)) + + # is_file(), not exists(): resolve() matches tree_paths(), which is files + # only, so a directory named like a reference must not satisfy one here. + for token in sorted(tokens): + if unverifiable(token) or (ROOT / token).is_file(): + continue + if any((b / token).is_file() for b in bases): continue - # A reference has to identify one file. Accepting "something in the - # tree ends this way" would pass a deleted src/a/foo.c because an - # unrelated src/b/foo.c survived, which is the exact failure this - # script exists to catch. Two matches is not a pass either: the - # reference is ambiguous and wants a longer path. + # Exactly one match. A deleted src/a/foo.c would otherwise pass on an + # unrelated src/b/foo.c, and two matches means the reference is + # ambiguous and wants a longer path. matches = resolve(token, paths) if len(matches) == 1: continue - # Consulted after resolution so a stub the tree really does carry, - # like the Hypervisor header under frama-c-stubs/, is verified rather - # than waved through by the exemption. + # After resolution, so a stub the tree does carry, like the Hypervisor + # header under frama-c-stubs/, is verified rather than exempted. if system_header(token): continue if len(matches) > 1: @@ -314,8 +321,8 @@ def check_targets(text, raw, targets): messages = [] for target in sorted(named): - # "make verify-" is a form, not a target: the capture stops at - # the angle bracket and leaves a trailing hyphen no real rule has. + # "make verify-" is a form: the capture stops at the angle + # bracket, leaving a trailing hyphen no real rule has. if target.endswith("-"): continue if target not in targets: @@ -326,10 +333,8 @@ def check_targets(text, raw, targets): def check_sections(text): """Every quoted section name is a heading in the docs file it cites. - The match is exact once the heading's backticks are stripped: accepting a - prefix would pass "Validation Strategy" for a section actually titled - "Validation Strategy By Change Type", which is the kind of near-miss that - sends a reader to the wrong table. + Exact match once backticks are stripped: a prefix would pass "Validation + Strategy" for a heading titled "Validation Strategy By Change Type". """ messages = [] for sentence in text.split(". "): @@ -346,7 +351,7 @@ def check_sections(text): def check_skill_refs(text, skills): """Every sibling skill named in prose exists as a skill directory.""" messages = [] - for ref in sorted(set(SKILLREF_RE.findall(text))): + for ref in sorted(set(SKILLREF_RE.findall(INLINE_PATH_RE.sub(" ", text)))): if ref in LANES or ref in skills: continue messages.append(f"refers to skill {ref}, which does not exist") @@ -363,18 +368,15 @@ def check_file(path, paths, targets, skills, errors): except ValueError: rel = path - # Prose wrapped at 79 columns splits references across lines: `make\n - # check-format` and a section name broken mid-title are the same reference - # a reader sees, so every pass below runs on the text with runs of - # whitespace collapsed. Checking the raw text instead silently skips any - # reference unlucky enough to land on a line boundary, which is most of - # them in a file this shape. Frontmatter stays raw because its regexes are - # line-anchored, and the fenced-block scan needs real line starts. + # Prose wrapped at 79 columns splits references across lines, so every + # pass below runs on whitespace-collapsed text; the raw text would skip + # any reference landing on a line boundary. Frontmatter and the fenced + # scan stay raw, since their patterns are line-anchored. text = re.sub(r"\s+", " ", raw) messages = ( check_frontmatter(path, raw) - + check_paths(text, paths) + + check_paths(text, raw, paths, local_bases(path)) + check_targets(text, raw, targets) + check_sections(text) + check_skill_refs(text, skills) @@ -412,7 +414,48 @@ def check_file(path, paths, targets, skills, errors): "Helpers in `fd.c/h` classify it.", "write `fd.c` and `fd.h`", ), + ( + "sibling reference file that is missing", + "Load `references/gone.md` at step 3.", + "does not exist", + ), + ("path in a fenced block", "```sh\npython3 scripts/nope.py\n```", "does not exist"), + ( + "path in a fenced block inside a numbered step", + "1. Run it:\n\n ```sh\n python3 scripts/nope.py\n ```", + "does not exist", + ), + ( + "make target in a fenced block inside a numbered step", + "1. Run it:\n\n ```sh\n make check-fmt\n ```", + "check-fmt", + ), + ( + "sibling reference that resolves to a directory", + "Load `references/dirlike.md` at step 3.", + "does not exist", + ), ("valid repo path", "See `src/core/guest.c`.", None), + ( + "sibling reference file beside the skill", + "Load `references/fixture.md` at step 3.", + None, + ), + ( + "valid path in a fenced block", + "```sh\npython3 scripts/check-mutants.py\n```", + None, + ), + ( + "valid path in a fenced block inside a numbered step", + "1. Run it:\n\n ```sh\n python3 scripts/check-mutants.py\n ```", + None, + ), + ( + "repo path that looks like a skill name", + "The Go `cmd/elfuse-container` CLI.", + None, + ), ("valid include-style path", "Include it as `core/guest.h`.", None), ("valid system header", "Frama-C cannot model `sys/mount.h`.", None), ("valid line-wrapped target", "Run `make\ncheck-format` first.", None), @@ -439,22 +482,21 @@ def check_file(path, paths, targets, skills, errors): def self_test(): """Assert this script still rejects each class of stale reference. - Every case here is a bug this script shipped with at some point. Two of - them are the reason it exists in this form: a reference broken across a - line boundary was invisible to every pass, and a section name that was a - prefix of a real heading passed as a match. Both were found by mutating a - file by hand, which is not a thing the next person will think to do. - - The negative cases matter as much as the positive ones. A checker that - starts flagging valid prose gets switched off, and then it protects - nothing at all. + Every case is a bug this script shipped with: a reference broken across + a line boundary was invisible to every pass, a section name that was a + prefix of a real heading passed as a match. The negative cases carry the + same weight, since a checker that flags valid prose gets switched off and + then protects nothing. """ paths, targets, skills = tree_paths(), make_targets(), {"elfuse-syscall"} failures = [] with tempfile.TemporaryDirectory() as tmp: skill_dir = pathlib.Path(tmp) / "elfuse-syscall" - skill_dir.mkdir() + (skill_dir / "references").mkdir(parents=True) + (skill_dir / "references" / "fixture.md").write_text("fixture\n") + # A directory named like a reference, for the is_file() case. + (skill_dir / "references" / "dirlike.md").mkdir() fixture = skill_dir / "SKILL.md" for label, body, expect in SELF_TEST_CASES: @@ -467,8 +509,17 @@ def self_test(): elif expect is not None and expect not in found: failures.append(f"{label}: expected {expect!r}, got: {found or 'none'}") - # Frontmatter drift needs its own directory: the name is checked - # against the directory the file sits in. + # A reference file cites siblings from one directory deeper, so it + # needs a fixture that sits there. + sibling = skill_dir / "references" / "sibling.md" + sibling.write_text("See `references/fixture.md`.\n") + errors = [] + check_file(sibling, paths, targets, skills, errors) + if errors: + failures.append(f"reference sibling: expected no error, got: {errors}") + + # Frontmatter drift needs its own directory, since the name is checked + # against the one the file sits in. other = pathlib.Path(tmp) / "elfuse-other" other.mkdir() drift = other / "SKILL.md" @@ -478,7 +529,7 @@ def self_test(): if not any("frontmatter name" in e for e in errors): failures.append("frontmatter drift: expected a name mismatch, got none") - total = len(SELF_TEST_CASES) + 1 + total = len(SELF_TEST_CASES) + 2 if failures: print( f" {len(failures)} of {total} self-test case(s) failed:", file=sys.stderr @@ -500,13 +551,13 @@ def main(): skills, files = set(), [] if SKILL_DIR.is_dir(): skills = {d.name for d in SKILL_DIR.iterdir() if (d / "SKILL.md").is_file()} - files = sorted(SKILL_DIR.glob("*/SKILL.md")) + files = sorted(SKILL_DIR.glob("*/SKILL.md")) + sorted( + SKILL_DIR.glob("*/references/*.md") + ) - # A routing file that points at the skills gets checked the same way, but - # only when its owner names it. Whether one exists, and what it is called, - # is local to a working copy and not this script's business. A named file - # is checked even in a clone with no skills directory, because that is - # where its references are most likely to have gone stale. + # A routing file is checked the same way, but only when its owner names + # it: whether one exists is local to a working copy. It is checked even in + # a clone with no skills directory, where its references rot fastest. for extra in sys.argv[1:]: path = pathlib.Path(extra) if not path.is_absolute():