Skip to content

on-call-rota: does a valid rota exist, and what did the policy not say? - #11

Closed
sajonaro wants to merge 3 commits into
mainfrom
on-call-rota
Closed

sajonaro wants to merge 3 commits into
mainfrom
on-call-rota

Conversation

@sajonaro

@sajonaro sajonaro commented Oct 3, 2026

Copy link
Copy Markdown
Contributor

Adds on-call-rota/ on top of the pruned main (#10).

Six weeks of on-call from a team of four: nobody two weeks running, at most two weeks each, leave respected, and a new joiner only in their second month. The cap is a scale l0 → l1 → l2 whose top has no up, so a third week is absent rather than refused.

  • A rota exists, and the witness is the rota: Ann, Cat, Ann, Bob, Cat, Bob. There are ten in all; derive rota reads them out as rows.
  • Two gaps: the policy never says whether a primary may hand over straight into their own leave (Bob's week 2, Cat's week 3).
  • The planner's trap: give Cat week 1 and no rota can be finished. The only ways out are those gaps.
  • The strict variant adds "not the week you come back from leave", and no rota exists. Reasoning back from week 4: it must be Ann, so week 3 must be Cat, which is a gap. A rota exists only if the policy's open question is answered yes. compare gives rota-exists LOST, with no witness to print.

Differences from the plan: no shared libraries/rota.lib.writ (one user). The plan's predicted trap shows up only through the gaps, and the README says so.

Cross-check: 55 → 57 properties (55 compared). ./run-tests.sh all: 280 checks, 0 failed.

🤖 Generated with Claude Code

sajonaro and others added 2 commits October 3, 2026 20:52
Six weeks, four people, leave, a new joiner, at most two weeks each — the cap
carried by a scale whose top has no `up`, so a third week is absent. A rota
exists and the witness is the rota; ten in all, read out by derive as rows.
Handing over straight into one's own leave is a gap: the policy is silent.
Giving Cat week 1 strands the planner at that gap. One more rule (not the week
you come back) and no rota exists unless the gap is answered yes.

Cross-check 55 -> 57 properties (55 compared); 280 checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…d a foreign key

change-an-enum: widening the CHECK is instant; the first WRITE of the new
value is the migration, and the shortcut writes it while r1 still reads.
split-a-table: dual write and backfill; the shortcut switches reads once the
backfill has started — five steps, the longest route in the collection.
add-a-foreign-key: NOT VALID spares the old rows, not the running code; adding
it mid-rollout makes the old release's deletes fail, in two steps.

writ sql reads CHECK … IN as an enum and REFERENCES as an arrow, as planned;
it reads NOT VALID as a plain foreign key (identical output, --strict accepts
it) while declining VALIDATE CONSTRAINT — asserted as found. The parent
README's "the shortcut is always shorter" is now what was measured: shorter in
two of six, never longer.

Cross-check 57 -> 63 properties (61 compared); 305 checks.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
db-migration-problems: change an enum, split a table, add a foreign key
@sajonaro

sajonaro commented Oct 3, 2026

Copy link
Copy Markdown
Contributor Author

Superseded by #14, which landed this together with #12 and #13 on main.

@sajonaro sajonaro closed this Oct 3, 2026
@github-actions github-actions Bot locked and limited conversation to collaborators Oct 3, 2026
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant