isabelle-watchdog

A build watchdog for Isabelle, and the build-trajectory corpus it records.

Two things that ship together because one calls the other:

• The watchdog supervises an isabelle build and kills it on a stalled stdout, a wall-clock budget, or a tactic looping on a single line — and in that last case it names the line, which is the difference between "the build hung" and "by (auto simp: …) at AlphabetReduction.thy:1488".
• The recorder appends one JSON line per attempt to a corpus: the outcome, the budgets that were in force, the error loci, the reasoning you wrote beforehand, and the incremental diff of the sources. Over time that is a record of how a proof was actually found, as opposed to how it reads once finished.

pip install isabelle-watchdog

Use

# supervise a build and record the attempt
BUILD_SESSION=MySession isabelle-build -m 'diagnosis: the induction is too weak;
                                           change: generalise over the tape index;
                                           expect: ok'

# or call the watchdog directly around any command
isabelle-watchdog isabelle build -d t MySession

# read the corpus
trajectory --help          # every view, grouped by the question it answers
trajectory lengths --fit   # how many attempts did each proof take?
trajectory notes           # what did you predict, and were you right?
trajectory check           # is every recorded diff still intact?
trajectory audit           # do these readers' own statistics hold up?

# every command takes -V/--version and -h/--help
trajectory --version

Why record a build at all

A finished proof tells you where you ended up. It does not tell you how many attempts it took, which of them made progress, or what you believed at the time — and those are the questions worth asking if you want to know whether a development was hard, or whether a tool helped.

Three design choices follow from wanting that record to be trustworthy:

The diff is the payload, stored as text. Each record carries its own incremental diff inline, anchored to a public commit. A corpus is therefore portable: you can read it, and reconstruct any attempt's sources from it, without the original git object store. An earlier prototype chained snapshots on refs/attempts/* and was unshareable for exactly that reason.

A prediction, recorded before the outcome. Notes take four keys — diagnosis:, change:, expect:, ref:. expect: is the one worth the trouble: it is the only field in a build corpus that scores itself. Because that only holds if the note predates the build, the record stores whether it did (note_pre_build) rather than assuming.

The corpus can prove its own integrity. Every payload is exactly git diff --no-color -M <base> <tree> for trees the record names, so trajectory check regenerates and compares each one. Where objects survive, that is both the strongest available check and the exact repair — no inference about what was lost. Defects that cannot be repaired without fabricating content are reported and left alone.

Configuration

Everything is environment variables, so the tooling composes with whatever build system a project already has.

variable	default	what
WATCHDOG_TIMEOUT	20	kill after N seconds of stalled stdout
WALL_TIMEOUT	40	absolute wall-clock cap
BATTERY_FACTOR	2.0	scale the budgets on battery power; 1.0 disables
LOAD_FACTOR_MAX	4.0	cap on the measured contention factor; 1.0 disables
LOOP_PROGRESS_THRESHOLD	3	consecutive same-line warnings before a loop kill
BUILD_PROGRESS_THRESHOLD	15	passed to Isabelle as -o build_progress_threshold
WATCHDOG_LOG_DIR	resolved (below)	where records go
BUILD_SOURCE_PATHSPECS	*.thy *ROOT *ROOTS	what counts as source
BUILD_SESSION	derived	session to build (isabelle-build)
BUILD_RECORD	on	trajectory capture on/off (--no-record)
TRAJECTORY_CORPUS	—	read a specific corpus
TRAJECTORY_ATTRIBUTION	—	attribution facts a corpus cannot show

The wall timeout is deliberately tight. A build that hits it is either looping or has become measurably more expensive, and both are worth knowing about; raising the budget to make a red build go green trades a fast, specific failure for a slow, vague one.

On battery the budgets are scaled rather than bypassed, so a battery-throttled-but-fine build stops tripping while a genuine cost regression still does. The loop-detection threshold is scaled too — without that, a slow but healthy command crosses the unscaled threshold and gets killed as a loop while the scaled budgets still have room.

A busy machine, versus a slow one

These look alike and are not, so they are handled differently.

Battery throttling changes how much work a CPU-second buys. Nothing can measure that after the fact, so it takes an assumed factor — BATTERY_FACTOR.

Sharing the machine changes how many CPU-seconds you get per wall-second, and that is measurable: a descheduled process accrues no CPU time at all. So the watchdog samples its process tree's CPU time and works out the duty cycle — CPU-seconds per wall-second. A build getting a quarter of a core has had a quarter of the budget it was charged for, and gets four times as long. Nothing is estimated, and nothing is calibrated: 0.25 of a core means the same thing on every machine.

Three cases, and the third is the point:

duty cycle	verdict	what happens
~0	stalled	killed on time — no CPU is a hang, and more time cannot fix it
0.05–0.9	starved	budgets × 1/duty, capped at LOAD_FACTOR_MAX
≥ 0.9	running	killed on time — a build using a full core is expensive, not starved

That last row is why this is a measurement and not a load-average heuristic: a proof that got genuinely slower burns CPU at full rate, so it still trips its budget and the regression is still visible. Scaling by an estimated system load would have hidden it.

Where the corpus lives

$WATCHDOG_LOG_DIR if you set it. Otherwise the tools look, rather than assuming — first for a committed .isabelle-watchdog naming the directory, then for a corpus already present under a known layout, and only then do they create one at t/logs. Readers resolve the same way, so a reader lands where the writer wrote without being told twice.

# .isabelle-watchdog, at the project root, committed
# the bare line is the log directory, relative to here
results/isabelle-logs

# optional — only needed where the session cannot be derived
session: SPSlowdown
dir: isabelle

Capture starts at your first commit. A record is a diff anchored to a public commit — that anchoring is what makes a corpus portable — so a repository with no commits yet, or a directory that is not one, records nothing. It says so on each build and in --where, rather than failing quietly; the build itself is never affected.

One file in that directory is data; the rest is local state.

file	commit it?	what it is
builds.jsonl	yes	the corpus — irreplaceable, and the reason for all of this
instance-id	no	identifies this working copy, so parallel clones' records pool without collision. Sharing one would merge two machines into one identity
last-build.log	no	the last build's output, overwritten every run
.last-attempt	no	the chain pointer, naming throwaway git objects a clone never receives
next-note.md	no	a note waiting for the next build to consume it

.last-attempt is the one worth being explicit about, because committing it looks harmless — it sits beside builds.jsonl and holds three hashes. Those hashes name tree objects nothing references, so they are strictly local. In a fresh clone they are simply absent; the recorder notices and re-baselines on HEAD rather than losing the attempt, but the diff it writes that once is the whole working tree rather than the edit.

The session is derived too. One ROOT under the project declaring one session is unambiguous, so a single-session project needs no configuration at all: isabelle-build -m '...' and nothing else. Several ROOTs or several sessions is an error listing them rather than a guess — building the wrong session records an attempt against the wrong thing — and that is when the session: key earns its place.

Worth committing one. Discovery can only find a corpus that already exists, which means it says nothing about a fresh clone — whose first build would otherwise mint a corpus in the default place rather than the project's.

Ask before you build, rather than finding out after:

$ isabelle-build --where
project: /home/me/proofs
log dir: /home/me/proofs/t/logs
    why: no corpus found and nothing declared -- this is the default, and a
         build here would create it.
         Commit a .isabelle-watchdog to choose somewhere else.
records: /home/me/proofs/t/logs/builds.jsonl

Supervision without the corpus

Capture is on by default — it is the reason the supervision was written. But the supervision is useful alone, so a project that wants only a build killed when it loops can say so, rather than accumulating records it will never read:

isabelle-build --no-record -m '...'      # this call
isabelle-watchdog --no-record isabelle build -d t MySession
export BUILD_RECORD=0                    # this project

--no-record still logs, still kills, still names the looping line; it just writes no builds.jsonl. An unrecognised $BUILD_RECORD is an error rather than a guess, because the guess would be "on" — which quietly collects the data someone declined.

Requirements

Python 3.10+, git, and isabelle-layout — the ROOT and theory-header parser, which declares no dependencies of its own, so that is the whole tree. The list is short on purpose: this runs beside a build, and anything it depends on is something that can break one.

Status

Alpha. The record schema is still moving; trajectory check will tell you if a corpus written by an older version has drifted, and CHANGELOG.md says explicitly which releases changed it.

The design is documented at length in docs/logging-design.md, which the code comments cite by section number.

Development

pip install -e ".[test]"
pytest -m "not slow and not isabelle"   # pure logic — seconds
pytest -m "not isabelle"                # + real subprocesses
pytest                                  # + a real isabelle build

pytest is a test dependency only — nothing under tests/ is installed or imported by the package. The isabelle marker covers the end-to-end test, which needs a real Isabelle and a prebuilt HOL heap and skips cleanly without them.

isabelle-layout is a runtime dependency, so pip install -e ".[test]" brings it in from PyPI. To test against an unreleased change to it, install the sibling checkout over the top afterwards — that order, because installing this package would otherwise pull the published one back:

pip install ../isabelle-layout

Validating a change against a real project writes to that project's real corpus unless you point WATCHDOG_LOG_DIR at a scratch directory first — see docs/working-on-the-tooling.md.

Licence

MIT.