| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
RG 33 omits a II/III-class vigil in three cases: it falls on a Sunday, it
falls on a I-class feast, "vel si festum cui praemittitur in alium diem
transferri aut ad commemorationem reduci contingat". Only the first two
were built; the third was recorded in precedence_ef.ml as unimplemented on
the grounds that no witness existed in the shipped data. That reasoning was
wrong, and the rule fires on 1 744 days across 1583-9999.
Both halves of the clause reduce to one observable question -- is the feast
the OBSERVED office on the following day (RG 34 puts it there) -- so the
kernel asks it once per candidate, after place_transfers has settled the
year. No fixed point is needed: a vigil is a candidate only on its own day,
never on its feast's, so suppressing it cannot change what the next day
observes. Precedence.rules gains vigil_feast, which returns the slug of the
feast a vigil precedes; the kernel cannot infer that itself, because only
two of the five vigil/feast pairs share a slug stem.
Blast radius, measured pre-change binary vs HEAD over the whole domain and
classified: 1 744 days, three shapes, zero unexplained. 1 199 are the feast
reduced to a commemoration (10 August on a Sunday, St Lawrence); 478 and 67
are the feast transferred under RG 96 after the Sacred Heart or Corpus
Christi takes its day. The Assumption's and the Ascension's vigils never
qualify -- their I-class feasts always keep their own day.
Independently witnessed, which is unusual here. The published Ordo -- the
only witness outside the Divinum Officium -> missalemeum -> lectio lineage
-- omits St Lawrence's vigil on 2025-08-09, agreeing with colitur against
both engines. That date had been read earlier as an Ordo gap; the Ordo was
right, and correcting the misreading is what surfaced this clause. On
2027-08-09 the feast does keep its day and the Ordo omits a vigil colitur
correctly keeps, which is a genuine Ordo gap.
Allow-lists: C39 (lectio, 10 rows) and a 2038 oracle class citing the
register, the 2026-2027 window having no instance. The golden pin asserting
St Lawrence's vigil is violet moved 2025 -> 2027; its own comment had
reasoned about the vigil's weekday and missed that RG 33 also looks at the
feast's. Two new pins cover both shapes of the clause.
The vigil/feast table is built with Slug.of_string_exn: mutation testing
showed that of_string plus Result.to_option turns a typo into None, which
this hook's contract reads as "not a vigil", switching the rule off in
silence. Two tests assert the table against the shipped data in both
directions.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Date_spec carried one variant, Fixed(month, day), and its own header said
Sunday- and Easter-relative forms would arrive with the OF sanctoral. They
arrive early because two things needed them at once: a user-supplied
overlay carrying a local movable feast had no way to express "the first
Sunday of October", and Rogation Wednesday's commemoration has been
recorded as architecturally blocked since 2026-08-13.
That blockage turns out to have been a premise, not a fact. The register
concluded the Rogation "is not Commemoration_only sanctoral data by
nature... it needs a genuinely THIRD kind of thing this architecture has
no name for" -- but the reasoning rested on there being "no civil (month,
day) pair to anchor a Fixed entry to". That is a statement about
Date_spec's expressiveness. With Easter_offset the entity is ordinary
sanctoral data, the identical shape Add major-litanies already ships,
differing only in how the date is written. No third channel was needed.
The register is corrected rather than left contradicting the code.
Two variants: Easter_offset of int, and Nth_weekday of {month; nth;
weekday} with negative nth counting from the end. Fixed's sexp
representation is untouched, so all 327 sanctoral entries and the whole
overlay parse unchanged. Both are re-validated in t_of_sexp through their
smart constructors, extending the idiom Fixed already used -- the failure
that guards against is invisible, a spec deserialising into something
that silently never resolves and a celebration vanishing with no
diagnostic.
Easter is supplied by the rite, not computed in the kernel. Computus
ships Gregorian and Julian both, and picking one here would hard-code a
Roman assumption into rite-agnostic code and be silently wrong for a
Julian-reckoning rite. Rite.t gains an easter field; Rite_ef supplies the
Gregorian one.
Layer keeps a split index. Fixed entries stay in the year-independent
(month, day) table, which preserves the fast path and the "30 November
counted twice in a 371-day span" behaviour validate.mli documents for St
Andrew. Movable entries have no year-independent key by construction --
the same spec lands on a different (month, day) each year -- so they
resolve per civil year into a rata-die table. index_by_date is removed
rather than kept as an alias: two ways to index a layer, one of which
silently ignores movable entries, is the trap this change exists to
avoid.
Two domain-edge defects, both found by the suite rather than reasoning. A
liturgical year is Advent-anchored, so resolving civil year y names y +/-
1, and at the edges those are 1582 and 10000, which Computus correctly
refuses by raising. The ceiling surfaced through the domain-ceiling test,
the floor through `colitur day 1583` failing outright. Fixed once, in
Layer.index, the single point that calls the rite's easter -- a clamp
repeated per caller would have been two places to get wrong a third time.
Rogation Wednesday: RG 87 assigns the Litaniae minores to the Monday,
Tuesday AND Wednesday before Ascension (scan1:691); colitur built the
first two from the start and never the third. RG 88 keeps it out of the
Office, so the Ascension Vigil remains observed. RG 89 routes it through
the Major Litanies' rules, but RG 109's closed list names only maiores,
so by RG 107 it is an ORDINARY commemoration -- confirmed in the output,
not assumed. Name from the Missal's own "feria IV" (scan1:20495-20497),
violet to match the Monday and Tuesday offices.
Blast radius, full 1583-9999 sweep against the pre-change binary: 2257
days, every one the same shape, zero unclassified, line counts equal both
sides. The complement is the informative half -- in the other 6160 years
the Rogation does not appear at all, because RG 111 admits one
commemoration on a II-class day and an impeded feast takes it under RG
113, a Commemoration_only candidate having no row in RG 91's table. Both
shapes are pinned.
Allow-lists unmoved: layer 3 compares no commemorations and is blind by
construction, and layer 4's 2026-2027 window has a competing feast on
both Wednesdays, so the Rogation is capped out in exactly the years the
oracle can see. C8 is unchanged, asserted by its own count pin.
Not built: Sunday-relative specs, which nothing needs yet, and the
--overlay plumbing that would let a user actually supply a local movable
feast. Nth_weekday therefore ships with synthetic and property coverage
only; inventing a shipped entry to exercise it would be fabricating
calendar data.
Register: section 6.10.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Liturgical_day.citations has read "always empty until Plan 4" since Plan 3;
it is now filled. Rite.t gains a readings function, rite-supplied for the
same reason transfer_target is: what a day with no proper falls back to is a
rubric, not a universal. Calendar calls it and passes its own temporal
function as the callback the rite needs to reach another date.
Steps 1 and 2 only: the observed celebration's own proper, else the day's own
temporal slug. Nothing encodes "Lent has daily propers" -- the presence of an
entry is the discriminator.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Five follow-ups from the fix-round re-review, none touching a computed
result.
M20's note had said "moderate-high, not certain" with a specific revisit
trigger attached. The fix round raised the label to "near-certain" and
deleted the trigger in the same edit. Upgrading a confidence while
removing the condition that would lower it again is the one move this
record must not make, so the trigger is restored alongside the higher
label: no primary text anywhere names the Major Litanies in a
Mass-orations-count worked example, only the general II-class-Sunday
rule twice over. RG 434(b) closes the Office-shaped doubt and nothing
further.
"WORD-IDENTICAL" overstated the relation between RG 111(b) and n.
434(b). Only the trailing "quae tamen omittitur si commemoratio
privilegiata facienda sit" is verbatim in both; the openings differ,
n. 434(b) recasting the rule into the orations register. The claim was
self-refuting -- both texts are quoted adjacent to it -- and the
argument never depended on it. Now "identical in its operative clause".
And n. 434 is not "a different part of the same document": the running
heads put RG 111 under Rubricae generales and n. 434 under Rubricae
generales Missalis Romani, two distinct corpora bound in one volume,
which is the entire force of the corroboration. The code comment had
understated its own point.
Also corrects the register's LT line range for n. 434(b) (3574-3576, not
3564-3570; the (b) clause is not in the cited range), and records in
calendar.ml the diagnostic that channel (3) trades away: a rite whose
transfer_target names a date its own disposition omits used to raise a
loud, mislabelled Validate failure and is now silent at the origin. The
kernel cannot distinguish that from a deliberate omission without rite
knowledge it must not have, so accepting it is right -- but the signal
is gone, and that should be written down rather than discovered later.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(fix round 1, F1)
The prior fix (settled_at) recognised two settlement channels for a
transferred candidate at its target -- winning outright (observed) or
surviving as a commemoration -- but missed a third: reaching the target
and then being CAPPED OUT there, by admit's own RG-111-style admission
count limit or by disposition's own Omit. That candidate lands in the
target's own omitted list, genuinely settled and accurately labelled, but
settled_at did not check that list, so the origin reported it as
unresolved under the same wrong, hardcoded unconverged_reason -- the exact
original bug, one level further out.
Unreachable on shipped EF data (the Major Litanies are the only privileged
Commemoration_only candidate real data carries, and no second one can ever
share Easter+2), but reachable by construction: a second privileged
Commemoration_only entry on the Litanies' own transfer target that
outranks it in admit's Class1 selection, or -- without any synthetic data
-- forcing the Litanies' own RG 109(f) privilege to Ordinary, which makes
the transferred candidate lose that same cap against its own real target.
Fixed by adding target-omitted membership as a third disjunct in
settled_at. New regression test in test_calendar.ml, built the same way:
the real EF layer plus one synthetic privileged Commemoration_only entry
on the real 2011 transfer target, sorting ahead of the Litanies so it wins
the Class1 slot. Mutation-verified to fail specifically when the third
disjunct is removed. COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force stays
clean after the fix, confirming it changes no shipped day's output.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
as observed
Calendar.build_day's `unresolved` check decided whether a Transfer-disposed
candidate had genuinely settled at its target by checking only whether it
became that day's own `observed` celebration. That was correct for every
prior use of Precedence.Transfer: a losing FEAST, which RG-96-style rules
guarantee an unblocked target to win outright once it arrives.
It is not correct in general. A rite's rules are free to dispose a
Celebration.status = Commemoration_only candidate as Transfer too (the EF
Major Litanies, RG 80, do exactly this) -- and such a candidate can never
become `observed` anywhere, by the same status that makes it eligible to
transfer in the first place. The old check mislabelled a cleanly-settled
transfer of that shape as "did not converge" (a hardcoded string, not a
real read of the placement pass's own convergence) and double-counted it
in Validate's own duplicated-sighting check.
Replaced with `settled_at`, which re-resolves the target date and accepts
either `observed` or membership in that day's own admitted commemorations.
A strict superset of the old check -- every existing use (a transferred
feast winning its target) is unaffected -- and stays rite-agnostic: it
reads only Precedence.resolution's existing fields, no EF-specific
knowledge added to the kernel.
Found by the exhaustive property sweep (COLITUR_EXHAUSTIVE_SWEEP=1) the
moment a rite first produced this shape, not anticipated in advance.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Four findings from Task 6 review, addressed on top of f15e44d.
1. transferred_out was a single Date.t option, so when RG 97-98 collides
three or more feasts on one date (more than one loser), only the last
one Hashtbl.iter happened to visit survived -- a genuinely lost move,
and which one survived depended on OCaml's hash seed
(OCAMLRUNPARAM=R), an environment read a kernel invariant forbids.
RG 97-98 says coinciding feasts transfer "in order" -- plural -- so
the type was wrong, not the fixture: transferred_out is now
(Celebration.t * Date.t) list. transferred_in stays a single option,
deliberately: a day receives at most one arrival (RG 96 sends each
departure to the next non-I/II-class day, and the first to arrive
occupies it). The per-day list is canonicalised (sorted by target
date, then slug) after accumulation, the same fix layer.ml already
applies to its own date-bucket index and for the same reason.
Verified clean across 15 runs under OCAMLRUNPARAM=R; disabling the
canonicalisation step showed the raw order genuinely flip between
seeds, confirming the fix is load-bearing.
2. Every deferred candidate in the fixture was the same rank, so
compare_deferred's band branch was unreachable and reversing it broke
nothing -- the RG 97-98 test was pinning slug order, not band order.
The fixture now has three ranks (Hi1 outranks Hi2, both transfer,
both outrank Lo), with slugs chosen so band order and slug order
disagree. Reversing the band comparison now fails the test on
"higher-band loser claims 2 Feb first", received the wrong slug
instead.
3. A transfer_target free to name any date could place a candidate
outside the liturgical year's own start/stop bounds: invisible to
year/build_day, so it would be observed nowhere and, since its
origin's re-resolution would report it as settled, omitted nowhere
either -- genuinely gone, contradicting calendar.mli's "never
silently dropped". place_transfers now checks the range on every
placement and routes an out-of-range one to a permanent-exclusion
table instead of assignment, with its own cited omitted reason.
4. Precedence.resolve folds Transfer and Repose into one deferred case,
and place_transfers routed all of it through transfer_target (RG
96's search), which is only correct for Transfer. Repose is RG
100-102's repositio, a distinct rubric this module does not
implement. Documented rather than split into a second mechanism:
nothing in the EF ruleset returns Repose (design spec section 1.3,
"declared, not exercised"), so the gap is latent, not a live bug.
Two new tests (origin records every departure; transfer target outside
year is recorded not lost); the RG 97-98 test's fixture and assertions
rewritten for finding 2.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Calendar.year now runs a placement pass after resolving every day: each
deferred candidate (RG 95's I-class-only right of translation, via
Precedence's Transfer disposition) is placed on the next day the rite's
new Rite.t.transfer_target names as admissible, transferred_in/out are
set on the two ends of the move, and the whole year is re-resolved to a
fixed point, bounded by a hard max_transfer_rounds = 64 guard.
transfer_target is rite-supplied rather than a generic search Calendar
drives itself: RG 96's 'not I or II class' is not derivable from band or
disposition alone (RG 91's own table lets a universal I-class feast
outrank an ordinary Sunday in a raw contest, yet RG 96 forbids landing a
translation there regardless), and the search's starting point is
rite-specific too (the Annunciation exception). It takes an occupant
callback exposing what Calendar currently resolves as observed on any
date, so the rite never has to re-implement occurrence resolution.
Two correctness properties drove most of the design:
- A candidate's permanent natural loss at its own origin (the layer entry
never moves) is rediscovered every round; left unfiltered this
oscillates a placed candidate between two dates forever, since its own
rank makes it look 'occupied' to a fresh search from its origin. Both
the round loop's gather and the final per-day omitted accounting filter
this out, keeping only sightings that are either brand new or losing at
a candidate's *current* target (a fresh RG 97-98 bump).
- RG 97-98's sort has to actually decide something, not just happen to
agree with Precedence.resolve's own tie-break next round: a
claimed-this-round overlay lets earlier-processed candidates in one
round block later ones in the same pass, so two coinciding I-class
feasts land on consecutive admissible days in the one round they
collide, in band order.
Also folds in Task 5's review finding: year_bounds clamps y to [1582,
9999] once, up front, rather than guarding start and stop independently
(each guard only ever covered one of the two rite.year_start calls,
leaving year 999 and year 100000 each able to call it out of domain
through the other branch).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Precedence.resolution already tracked what happened to every losing
candidate -- commemorated, deferred, or omitted with a reason -- but
Liturgical_day.t had nowhere for the deferred and omitted buckets to land,
so Calendar dropped them at the door. Task 12's no-celebration-lost
invariant needs to read that accounting off the day result itself, not
re-resolve every day to reconstruct it, so a reason recorded nowhere is not
recorded.
Add Liturgical_day.omitted : ('r Celebration.t * string) list, after
transferred_out and before citations. Calendar.resolve_day now folds
resolution.omitted (Precedence's own native omissions, reasons intact) and
resolution.deferred (mapped to "deferred: transfer placement not yet
implemented (Task 6)") into it.
Adds a full-day accounting test against the whole Calendar pipeline: four
colliding sanctoral entries plus the day's feria, checked as a slug set
(matching test_precedence.ml's own nothing-silently-lost test) so a
candidate silently dropped or duplicated into two buckets would fail it,
plus an identity check that the deferred and admission-limit reasons don't
get swapped.
|
|
|
Transfers make per-date resolution impossible to do correctly: resolving 25
March can push a feast onto 26 March, and RG 97-98 has coinciding I-class
feasts transfer in table order, which needs global knowledge. So year computes
a whole liturgical year in one pass and day indexes into it. Pure, no cache, no
mutable state.
This commit resolves each day but does not yet place deferred transfers; they
are recorded with a reason. Task 6 adds the placement pass.
|
