| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I7 (final-review.md, 2026-08-25-colitur-of-phases-3-5): OF Sundays and
solemnities shipped without the Second reading, and the lectionary
data header called the First reading an "Epistle" -- EF vocabulary.
The sole blocker was Validate's own kernel-hardcoded assertion that a
well-formed day's sorted citation parts are exactly [First; Gospel];
Citation.part already carried Second.
Rite.t gains citation_shapes : Citation.part list list, the fourth
EF-shaped kernel misfit (after Preface.t, Mass_formulary.source,
transfer_target's strictly-later contract) and the first fixed rather
than only documented. EF supplies its one shape unchanged; OF supplies
two, [First; Gospel] on a feria/feast/memorial and [First; Second;
Gospel] on a Sunday or solemnity (OLM 1981 Praenotanda n. 66.1 vs
n. 69.1, n. 84(b)/(c), page-image verified against olm-1981.pdf).
Validate's "citations" check now matches against the rite's own
declared shapes rather than a single literal pattern, preserving all
three invariants it always enforced: zero or one complete shape, never
partial; no part outside what the rite declares; no part repeated.
bootstrap_lectionary_of.ml's cite now extracts a Second reading from
Sunday-cycle ini sections only, correctly excluding the one stray
`second` field lectio's snapshot carries on a weekday-cycle section (a
content-verified scraping artifact). The hand-authored Christmas Day
entry gains its own Second reading from the same OLM passage already
cited for its First/Gospel. Regenerated data/of/lectionary.sexp: 771
entries unchanged, citation fields 1542 -> 1725 (+183, all Second
readings), SHA-256 re-pinned, header wording fixed and a new coverage
bullet added. Responsorial Psalm is deliberately still not emitted --
OLM 1981 Praenotanda n. 71 itself lists it apart from the readings
proper as a chant with its own refrain, and the finding driving this
change names only the missing Second reading.
EF output verified byte-identical to the branch start (empty
lib/rites/rite_ef + data/ef diff since v1.0.0, plus a direct binary
comparison of `day`/`readings` for 2026, 1583 and 9999 against a
worktree build of the pre-change commit).
Tests: three new fixtures in test_validate.ml prove the generalisation
holds both directions (a multi-shape rite accepts either of its
declared shapes; a rite that never declared a shape still rejects it).
test_citation_coverage_of.ml's pinned residual grows 41 -> 49, all new
entries the same already-understood chapter-crossing shape.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Layers 2 and 5 for the reading citations, which until now had coverage
from layers 3 and 4 only -- both oracle-bounded, at 2050 and 2027.
test_validate.ml said so in its own words ("No fixture here exercises
citations") and test_golden.ml's describe pinned twelve fields, none of
them a citation. 358 tests -> 369, and 370 under the sweep.
Layer 2 as two Validate checks rather than standalone QCheck properties,
so they ride the existing prop_invariants and the exhaustive sweep
instead of duplicating that machinery. "citations" asserts a day's parts,
sorted, are exactly [First; Gospel] -- one condition carrying three
invariants: zero or two but never one, nothing outside First and Gospel
since the chants are deliberately unbuilt, and no part twice, which a
bare cardinality test would miss. "citations-unresolved" is the separate
coverage half: the chain fell through every step. Both are gated on the
rite producing some citation somewhere, so a rite whose lectionary is not
built is held to neither and the synthetic fixtures stay unaffected.
The result over the whole domain: every day of every liturgical year
1583-9999 resolves exactly one Epistle and one Gospel. Mutation-proved
live rather than merely silent -- treating a well-formed pair as
malformed reddens the suite with real days showing [first,gospel].
citations-unresolved has no live witness at all, which is why
test_validate.ml gains five fixtures driving both checks through a new
?readings override, including the gate itself.
Layer 5 as six pins, one per chain step, so a regression names the step
that broke. Every literal was read out of the scans before being
compared with colitur, per that file's standing rule; scan lines are in
each pin's comment. Two of the six cover step 4, and the plan's own dates
for steps 1 and 4 were wrong: 2030-01-13 is a temporal day (Holy Family
on the generic Sunday slug) and would not have exercised step 1, while
2038-03-08 is John of God, who has a full proper Mass and never routes
through a Common -- so he becomes the step-1 pin instead.
A separate formatter rather than widening describe: widening would
invalidate all thirty existing literals at once and the only practical
way back would be pasting in whatever colitur printed, which is what the
file's header forbids. Restoring them honestly means hand-verifying
thirty more Masses against the scans, a task of its own. Stated rather
than hidden, and defensible because layer 2 now checks the shape of
every day in every year, which is the breadth that widening would have
bought.
Two pins earned their keep immediately. Lent I Monday failed on "Ezek"
against colitur's "Ezech" -- notation only, and colitur matches the
Missal's own abbreviation; layer 3 normalises this away and cannot see
it. The displaced-Sunday feria pins M26 shape 2(b)'s known-wrong
walkback deliberately, labelled as such so a future fix fails loudly,
and established two things M26 had not recorded: both parts come from
the displacing feast, not only the Gospel it cites, and the reference
carries a stray trailing period inherited through the bootstrap.
Blast radius: zero. The CLI never calls Validate, no data file changed,
and 20 years spanning 1583-9998 produce 7301 byte-identical lines
between the pre-change binary and HEAD.
Step 4's blind spot is now measured rather than argued. Corrupting the
Common of Non-Virgins I's Epistle leaves layer 3 (16801 days) and layer
4 (730 days) both green, reddening only one unit test and one new pin.
Both step-4 pins matched the scans on the first attempt -- the first
independent confirmation that route has ever had. It narrows the gap
without closing it: two of five Common-routed saints are witnessed,
isidore-of-seville is not, and gregory-the-great and patrick are
unreachable in any year 2005-2050.
Register: section 6.7 addendum. validate.mli documents both new labels;
liturgical_day.mli's "always empty until Plan 4" was outlived by the
lectionary and is corrected.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Fix round 1 on the commemoration-identity/tie-break work: the "genuine
same-band tie" M17 adjudicated as open was not a tie at all. RG 91's
table enumerates only "dies liturgici" (real feasts) -- entry 24's own
text is "Festa III classis, in calendario Ecclesiae universae
inscripta" -- so a Celebration.t.status = Commemoration_only candidate
(a saint reduced to a bare commemoration) has no row in the table to
begin with. Precedence_ef.band used to read rank alone, so it silently
lent such a candidate the same table entry as a genuine Feast of its
own rank; the calendarium's own 22 September row confirms the
distinction in its own notation ("S. Thomae de Villanova ... III
classis. / Commemoratio Ss. Mauritii et Soc. Mm." -- Thomas carries a
class number, Maurice carries none).
Fixed at the source, not by adding a status tier to compare_precedence:
band now checks status first, ahead of every rank-keyed branch, and
returns unclassified for any Commemoration_only candidate. M17 deleted
(not re-adjudicated) -- 22 September now resolves identically on both
sides, with no divergence left to name.
Blast radius measured independently (a temporary git worktree at the
pre-fix commit): 4451 days change across the whole 1583-9999 domain,
exactly 4 verified shapes -- 3576 x maurice-and-companions-martyrs ->
thomas-of-villanova and 282 x eleutherius -> philip-neri (admitted set
changes), 502 x appollonia/cyril-of-alexandria and 91 x dorothy/titus
(order only, independently confirmed against the calendarium's own
listing convention). Zero days change who is observed. Further swept
the whole domain for a genuine "two different candidates on the
identical real table entry" residual -- the shape RG 113 truly gives
no instruction for -- and found it empty: of 109201 same-rank ties
domain-wide, 83950 now resolve by band alone and the remaining 25251
are exclusively two Commemoration_only candidates tied at unclassified,
never two real feasts. The residual admit still breaks alphabetically
is real, but narrower than previously documented.
The "66 days" figure is reconciled, not merely disputed: 599 is the
tie population, 65 (whole-comparator: 67) is the real admitted-set
decision count within it (independently reproduced against the
pre-Task-B binary), 149 is order-only. Every one of the 65 real
decisions traces to the same Commemoration_only/Feast root cause as
Maurice/Thomas.
Also: validate.ml's admission fixed-point check recovers a
commemoration's real origin (by matching its slug against the day's
own temporal office) instead of reconstructing every candidate as
Sanctoral, since band -- unlike EF's own admit -- does read origin;
precedence_ef.ml/.mli's motivating example and blast-radius claims
corrected to no longer rest on the fixed Maurice/Thomas case;
test_identity_rank_corroboration's own population count corrected now
that 22 September (and 21 other Feast-status matches) became reachable;
its rank-agreement pin documents exactly what it does and does not
prove. Register (§4, §6.1, §6 checklist) and CLAUDE.md corrected in
place, including the RG 113 first-sentence gap this exercise surfaced
but did not close, recorded as a new open item.
275 -> 276 tests (with the exhaustive sweep), all green.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Three carried items from Plan 2's parked rulings, closed:
1. Slug uniqueness moves from a 200-sample QCheck property scoped to
one rite (test_temporal_ef.ml) into Validate's own "slugs" check, so
every consumer gets it. The resumed-Sunday exemption that property
carried is dropped, not weakened elsewhere: Plan 2 verified zero
duplicate slugs domain-wide (all 8 416 years), and by construction a
resumed Sunday only ever backfills a week number Septuagesima cut
short that same liturgical year, so it can never repeat a number
that year's own January Sundays already used. The now-redundant
property and its is_resumable_sunday_slug helper are removed from
test_temporal_ef.ml; test_validate.ml's own domain-wide property
covers the same ground for every consumer.
2. The anchors-erosion guard (Plan 2: deleting entries from a rite's
anchors list left the whole suite green) is implemented, but not in
Validate. Which of a rite's named days are Easter-derived is
knowledge only the rite's own `named` function has; Rite.t
deliberately exposes only `temporal` and `anchors`, never `named`,
so a rite-agnostic Validate has no ground truth to check anchors'
completeness against. Hardcoding an Easter offset, or even Easter
itself, would smuggle Western/Gregorian-specific knowledge into code
meant to also serve a future Julian-reckoning rite; rediscovering
"named-ness" structurally from `temporal` alone is unsound for EF,
since most ordinary Sunday/feria slugs from Septuagesima onward are
also constant-offset-from-Easter by construction. The guard is
therefore EF-specific and lives in test_temporal_ef.ml, discovering
the Easter-derived slug set mechanically (scanning a window around
Easter and keeping whatever `named` answers Some for) rather than
hand-copying either named's or anchors' own offset list, then
asserting completeness against the real anchors for the domain's
Easter extremes (1598, 1666) plus an ordinary year. A negative
fixture proves the guard has teeth, matching Plan 2's exact
regression (anchors missing "ef-ascension" reports it, and only it,
as missing).
3. test_validate.ml's extreme_years comment claimed 1818/2038; verified
against Computus.gregorian_easter directly, the domain's actual
Easter extremes (1583..2500) are 1598/1666. Corrected.
Verification: the full 1583..9999 domain sweep (233 tests via dune
test's 200-sample default, plus a manual full sweep) reports exactly
one failure -- the known, already-pinned year-9999 season-truncation
case -- and zero occurrences of the new "slugs" check anywhere in the
domain. Deleting "ef-ascension" from the real anchors list (reproducing
Plan 2's regression directly) is caught immediately by the new EF test
and, confirmed empirically, invisible to Validate's own full property
sweep -- direct evidence for why item 2 cannot live in Validate.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Widen Validate.run to take the rite's sanctoral layer alongside the rite
itself (Calendar.year needs both), and add five checks over the fully
resolved liturgical year, on top of the existing temporal-only pass:
- observed: a day's observed celebration never also appears among that
same day's own commemorations/omissions.
- lost: no sanctoral entry is silently dropped. Per slug, the number of
times it is actually sighted (observed + commemorations + omitted,
summed over the year) must never fall below the number of times its
own Date_spec resolves within the year's span -- also fires if
resolving the year raises at all, the most total form of loss.
- duplicated: the same per-slug count must never exceed the number of
Date_spec resolutions either. Deliberately NOT "no slug appears
twice": a fixed date can legitimately resolve twice in the ~20% of
liturgical years whose 371-day span reaches it on both ends (30
November/St Andrew is the worked example in validate.mli).
- unconverged: no day's omitted reason indicates Calendar's placement
pass hit its round guard before reaching a fixed point.
- admission: the rite's own rules.admit is a fixed point on what it
already admitted -- the rite-agnostic form of "the admission limit
was not exceeded" available without embedding a rite's own numeric
caps (RG 111's, for EF) into kernel code.
Each check has a dedicated negative fixture in the synthetic rite
(test_validate.ml), hand-traced against Calendar's actual resolution
mechanics before writing the assertion, and verified to fail for the
right reason against the code before this change. One pair
(unconverged/duplicated) is not fully independent: hitting the round
guard genuinely also trips duplicated, a real consequence of Calendar's
own accounting once a candidate is simultaneously sighted at its
permanent natural date and wherever the last placement round left it --
documented in guard_rules's own comment, not papered over.
test_validate.ml's ef_rite/run now use the real Rite_ef.context and the
real bootstrapped data/ef layer (Precedence_ef and the sanctoral
bootstrap did not exist when this scaffolding was first written) rather
than the earlier placeholder rules. Validate is clean across the whole
1583..9999 domain against real EF data except the one already-documented
year-9999 truncation case (test_year_9999_does_not_raise).
|
| |
|
|
|
|
|
|
|
|
|
| |
Validate took four loose arguments that had to come from the same rite with
nothing enforcing it, and Calendar is about to add more. Bundling makes a
mismatched assembly unrepresentable through the normal path.
season_runs replaces the hardcoded assumption that every season occupies exactly
one unbroken run. That holds for the 1962 rite but is false for the modern
form's Ordinary Time, which is one season in two runs -- as written the check
would have reported a false failure every year for the second rite.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Validate.run ~year:9999 raised (year_start (year + 1) asked year_start
for civil year 10000, out of the kernel's 1583..9999 domain), even
though 9999 is itself in range and kernel computation must never raise
on in-range input; ~year:9998 already returned zero failures. run now
clamps its scan to 31 December 9999 instead of computing year_start
(year + 1) when year is the domain maximum, and validates the
resulting truncated final liturgical year rather than not being able
to run it at all.
The design spec's validation §5 lists eight checks; only five were
implemented (coverage, seasons, weeks, weekday, closure). The two
missing were a real gap, not just a documentation slip:
- §5.7 anchor agreement. All of an EF year's Easter-derived and fixed
named days were pinned only by point assertions for 2026. run now
takes an ~anchors:(int -> (string * Date.t) list) parameter -- the
rite's own independent restatement of those dates, paired with the
slug each should carry, not derived from temporal itself -- and
checks that temporal agrees on every one of them. Temporal_ef.anchors
supplies EF's list. Kept rite-agnostic: the anchor list comes from
the rite argument, not the kernel.
- §5.8 determinism. run now calls temporal a second time for every
date and checks the result is structurally equal to the first.
Also, finding 8: the rank/season closure checks compare vocab entries
via their _to_string images, which is only sound if those images are
injective. run now checks List.map rank_to_string ranks and
List.map season_to_string seasons for duplicates up front and reports
a "vocab" failure if either collapses two distinct values to the same
string, rather than relying on that injectivity unasserted.
Test-quality fixes to the existing synthetic fixture, found while
adding coverage for the above: the fixture's own comment claimed its
mutation target (2026-03-15) was "not a Sunday" and "sits safely
mid-run" -- it is a Sunday, which made the coverage/week mutations
cascade further than documented even though the assertions still
target specific check labels. Moved to a genuine mid-week day
(2026-03-17) and the comment corrected. extreme_years's own test
required only "found at least one" of the two Easter-extreme years;
tightened to require both, since both genuinely exist in 1583..2500.
Covering tests: test_year_9999_does_not_raise (would error under the
old code; the fix is pinned by calling run 9999 directly with no try,
plus asserting the truncated year is reported via an ordinary
"seasons" failure, not silently or via coverage); anchor-clean and
anchor-fires cases on the synthetic rite; a determinism-fires case
using a target date whose temporal alternates what it returns across
successive calls; two vocab-injectivity-fires cases (collapsed rank
strings, collapsed season strings).
|
|
|
Coverage, season contiguity and completeness, Sunday-aligned week numbering,
slug well-formedness, weekday agreement and vocabulary closure.
Checks run over a liturgical year rather than a civil one, since Christmastide
straddles January and would otherwise appear to recur.
Run against EF temporal for landmark years, both Easter extremes, and 200
random years across 1583..9998 -- the property layer is how confidence reaches
past the oracle horizon.
|
