Metadata-Version: 2.5
Name: isabelle-watchdog
Version: 0.5.1
Summary: Isabelle build watchdog, and the build-trajectory corpus it records
Project-URL: Homepage, https://github.com/ott2/isabelle-watchdog
Project-URL: Source, https://github.com/ott2/isabelle-watchdog
Author: Andras Salamon
License-Expression: MIT
License-File: LICENSE
Keywords: build,dataset,isabelle,theorem-proving,trajectory,watchdog
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Build Tools
Requires-Python: >=3.10
Requires-Dist: isabelle-layout>=0.2.2
Provides-Extra: test
Requires-Dist: pytest>=7; extra == 'test'
Description-Content-Type: text/markdown

# 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.

```sh
pip install isabelle-watchdog
```

## Use

```sh
# 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:`. A section opens the note or a
line, or follows `; ` or `. `, so the one-liner and the multi-line form parse
alike. `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:

```sh
$ 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:

```sh
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`](https://github.com/ott2/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`](CHANGELOG.md) says explicitly which releases changed it.

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

## Development

```sh
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:

```sh
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`](docs/working-on-the-tooling.md).

## Licence

MIT.
