Repository navigation
feat(formal): measure Quint style and enforce two caps - #234
Merged
Merged
Conversation
`node formal/tools/check-style.mjs --report` prints the readability measurements #220 tracks, from the sources, so progress is reproducible: lines over 120 characters by area, module header lengths, comment and guide sentence lengths, definitions with six or more parameters or two adjacent booleans, and the free-text exclusion reasons in execution.json. Today: 658 long lines (171 models, 180 kernel, 307 fixtures), longest header 25, 247 of 1,719 comment sentences over 40 words, 93 of 2,221 guide sentences, 54 wide definitions, 5 with adjacent booleans, 531 free-text exclusion reasons. Without arguments it enforces the two rules guidance alone did not hold: a Quint line is at most 120 characters and a module header at most 25 comment lines, over every file under formal/models not named for that rule in formal/catalogs/style-allowlist.json. The allowlist names the 60 files that break the line cap today and no file for the header cap; it carries no counts and only shrinks, because an entry whose file is clean fails the check. The check is a step of `make audit`. AUTHORING.md states the two caps beside the conventions they enforce; the catalogs and tools indexes name the allowlist and the tool. Tests cover the fake-tree cases (unlisted offender, stale entry, missing file, header counting, report shape) and the committed tree.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #234 +/- ##
=======================================
Coverage 93.73% 93.73%
=======================================
Files 78 78
Lines 11357 11357
Branches 656 656
=======================================
+ Hits 10645 10646 +1
+ Misses 642 641 -1
Partials 70 70
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
… metrics with #220 Review follow-up on the style checker. The header cap counted only the comment block after the `module` line, and every kernel fixture writes its header before it: sixteen files scored zero and two (held-remote.qnt, payload-classes.qnt) exceed the cap, which was also a bypass. The header is now the comment block beside the `module` line on either side, the two offenders are allowlisted for the header rule, and the test pins the leading-block case and a stale header entry. The comment-sentence metric no longer counts section banner lines as sentence text (they glued neighbouring sentences into 98 of the 247 reported long ones), and both sentence rows report the over 40, 60 and 100 word counts, the longest and the average, as #220 tracked. The boolean-parameter metric counts definitions with two or more boolean parameters anywhere in the signature, actions included, with the parameter list scanned to its matching parenthesis, so shadow::newJob, one of C2's four targets, appears and an operator-typed parameter is one parameter; the wide-definition count is given per area. The tool header states every measurement's definition. AUTHORING defines the header, names the scope and says the allowlist grows only as a reviewed exception; the tools index heading names the audit lane correctly.
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
2 participants
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.
Phase 3 of #220, item B1. One commit, base
main. Independent of #233.What
node formal/tools/check-style.mjs --reportprints the readability measurements #220 tracks, computed from the sources so progress is reproducible:Those are reported, not enforced; the editorial guidance for them stays in AUTHORING "Writing conventions".
Without arguments the tool enforces the two rules guidance alone did not hold (AUTHORING already asked for lines without horizontal scrolling, and the Quint sources broke that 658 times): a Quint line is at most 120 characters and a module header is at most 25 comment lines. The header is the
//comment block beside themoduleline, before it or after it, up to the first import or definition, so the kernel fixtures' headers written abovemodulecount too. Enforcement covers every.qntunderformal/modelsnot named for that rule informal/catalogs/style-allowlist.json. The allowlist names the 60 files that break the line cap today and the two fixtures (held-remote.qnt,payload-classes.qnt) whose headers exceed 25 lines; it carries no counts and may only shrink: an entry whose file has become clean fails the check, so cleaning a file means deleting its line, and adding one is a reviewed exception. The check runs inmake audit.Why now
#231 brought every kernel header under the cap; without an enforced rule that regresses the first time someone pastes a paragraph. The line cap starts as a ratchet over 22 clean files and tightens as files are wrapped (Quint 0.32.0 has no formatter, so wrapping stays manual and is separate work). Review follow-up (second commit): the header is counted on both sides of the
moduleline, banner lines no longer inflate the sentence metric, boolean parameters are counted anywhere in a signature with actions included, and the report carries the over 60 and over 100 columns #220 tracked.Tests
formal-style.test.ts: on a fake tree, an unlisted long line fails namingpath:line, an unlisted tall header fails whether written before or aftermodule, a stale entry for either rule and a file outside the scope fail, a file listed for one rule and offending the other reports both, header counting stops at the first import or definition, definitions are scanned to the matching parenthesis, and the report renders every row; on the committed tree the check passes, exactly two headers exceed the cap (both allowlisted), and the audit plan contains the step.Verification
make auditgreen with the new step;vitest run test/formal-style test/formal-validationpass;tsc --noEmitclean;node scripts/check-docs.mjsgreen. AUTHORING re-keyed with--refresh.🤖 Generated with Claude Code