Imported from pirapira/flapjack (
AGENTS.md). Install upstream withnpx skills add pirapira/flapjack. Copyright stays with the author.
Agent Notes
Lean/Lake cache artifacts
Prefer a targeted repair over a global cache reset. When a build is blocked by
one bad or hardlinked cache artifact, remove that individual local .olean
(and its matching generated .ilean, .ilean.hash, or .trace metadata when
present) and rebuild the affected target. Do not use lake clean for this
class of problem: it discards unrelated, reusable cache state.
OLean files under .lake/ are local build outputs, not source artifacts. If
Lake reports that an expected .olean is missing or a hardlink is stale,
identify the exact module path and remove only that module's local generated
.olean/.ilean file (and, when the OLean is absent, its matching generated
trace/hash metadata), then rebuild the required target from source. The
recommended repair is to remove the individual problematic OLean, not to run
lake clean; a broad clean throws away unrelated useful cache state and is
unnecessary for this failure mode.
In particular, when a hardlink is the immediate cause, resolve the exact
.olean path first and remove that individual generated file; do not replace it
with a copied OLean from another worktree. This keeps the rebuilt artifact
source-derived and ensures later source changes are observed.
Do not copy .olean files between worktrees or overwrite one with a copied
artifact: a copied OLean can be newer than its source and hide subsequent
source changes. Cache cleanup is local-only; do not stage .lake outputs.
Fleet workflow
This section coordinates internal fleet agents. External contributors may open their own focused PRs and do not need access to the fleet's bead database.
Keep the CakeML/HOL submodule read-only. Put HOL probes and captured oracle
outputs on the Flapjack side under scripts/hol-probes/; follow that directory's
README and docs/PARITY-TESTING.md for the detailed procedure.
Claim a commit-sized bead before starting work. Record the pushed branch and commit, verification results, or exact blocked reason on the bead, and notify the coordinator. Keep dependency beads open until their own acceptance criteria are met.
Maintain one fleet integration PR. Agents push their own branches but do not open separate PRs; the coordinator merges reviewed work into the integration branch. Merge the updated integration branch back into agent branches with ordinary merges. Do not rebase or cherry-pick shared work.
Before reporting a port complete, build affected Lean modules, run lake test,
scripts/check-hol-refs.py, and scripts/check-warnings.sh. For executable
compiler changes, compare the executed output with original Pancake where an
oracle exists; see docs/PARITY-TESTING.md. State which checks actually ran and
which remain pending (including CI).
Porting HOL theorems: placement, cross-reference, and shape
Every Lean declaration that ports a declaration from the CakeML/HOL4 development must be traceable to its original without a lookup table.
Keep declaration notes local. docs/HOL-LAYOUT.md maps HOL scripts to
Lean modules; it is not a declaration-status log. Put assumptions, statement
differences, and other declaration-specific caveats beside the relevant Lean
definition or theorem. Track open work in GitHub issues, not in
docs/SOUNDNESS.md, which records assurance limits and external assumptions.
Place it in the counterpart file. Each HOL script has one primary Lean
counterpart (for example cakeml/pancake/proofs/pan_to_crepProofScript.sml
maps to the Lean module for the pan_to_crep proof). A ported declaration lives
in that counterpart, or in a submodule beneath it named after the HOL theorem
group or case it covers. Do not create catch-all "bridge", "adapter", or
"evidence" modules that collect fragments from several HOL scripts.
Tag it with @[hol ...]. Import Flapjack.HolRef and write
@[hol "cakeml/pancake/proofs/pan_to_crepProofScript.sml" "pc_compile_correct"]
theorem pcCompileCorrect ... := ...
giving the repository-relative HOL file and the exact HOL declaration name
(Theorem, Triviality, Definition, Datatype, ...). The attribute is
mandatory for every declaration whose docstring or purpose is "this is
HOL's X". scripts/check-hol-refs.py runs in CI and fails when the cited
file or declaration does not exist; scripts/check-hol-refs.py --mapping
prints the HOL-to-Lean mapping, and #hol_refs lists tagged declarations
from inside Lean. A declaration without the attribute is Flapjack-specific
infrastructure; if it has correctness content, say in its docstring why it
has no HOL original.
If the HOL script declares the same name more than once, append the exact
source line to the tag, for example @[hol "cakeml/...Script.sml" "name" 123].
The reference checker rejects ambiguous names without a line and lines that
do not declare that name.
Lean names may differ; the tag may not. Naming may follow Lean
conventions (pcCompileCorrect, stateRel), and keeping the HOL name
verbatim is also fine. Whatever the name, the @[hol] tag carries the exact
original, so the docstring need not repeat the path.
Splitting is allowed along HOL's own case structure. When one HOL theorem
is too large to port at once (for example pc_compile_correct, whose proof is
marked case by case: Skip, Dec, Call, DecCall, ...), each piece carries
the same @[hol] tag and a suffix naming the case, and an assembling theorem
with that tag states the HOL result itself. Each piece must be a genuine case
of the target statement: the same hypotheses as the HOL theorem, the same
conclusion shape, plus induction hypotheses for sub-programs and nothing
else. If a piece needs an extra hypothesis to go through, record it as an
open gap in the docstring; do not leave it as a permanent parameter.
The statement must have HOL's shape. A ported pass-correctness theorem
may not take as a hypothesis: the target evaluation or its result (HOL proves
the existential), the pass simulation predicate being established, post-state
code_rel/excp_rel facts that HOL proves, a universally quantified context
fact that no instance satisfies, or bidirectional event-prefix facts that
already imply the trace-equality conclusion. Theorems about simplified
evaluators (no clock, no memory domain, compile-and-execute "semantics") are
not ports of HOL theorems about the faithful semantics and must not carry
the tag of one.
Reviewed statements are pinned. docs/HOL-TYPE-HASHES.json records the
elaborated Lean type of each reviewed_exact entry in
docs/HOL-THEOREM-MAP.json. CI runs scripts/check_hol_type_hashes.py and
rejects statement drift. After comparing a changed Lean statement with its HOL
source, run python3 scripts/check_hol_type_hashes.py --update and review the
lock-file diff. The hash gate detects Lean statement changes only: it does not
hash the bodies of tagged definitions, the bodies of referenced dependencies,
or the HOL declarations, and it does not prove HOL-to-Lean equivalence or
replace source-level review.
A matching name is not enough. Before adding @[hol], compare the HOL and
Lean declarations' definitions, quantified variables, hypotheses, side
conditions, and conclusions. A different evaluator, an extra successful-pass
assumption, a weaker result, or a key comparison that does not implement HOL
equality is a mismatch even if a proof builds and the reference checker accepts
the name. Fix such a mismatch when tractable. Otherwise, remove the @[hol]
tag, explain the precise mismatch and missing HOL result in the declaration's
docstring, and file a bead for the faithful port. Preserve useful Flapjack-only
infrastructure; delete a declaration only when it is unsalvageable or itself
implements behavior that must be replaced. Do not merge a known mismatch as a
claimed HOL port.
Qualify only named list-to-array state fields. An unqualified tag records a
statement reviewed as exact and has manifest status reviewed_exact. The
(list_as_array := [field, ...]) qualifier is only for specific HOL list
fields represented by Lean arrays; it does not allow any other difference in
the theorem statement or semantics. Review the fields against the surrounding
HOL state relation, list lengths, index bounds, and update behavior. The
manifest must list the same fields and use reviewed_list_as_array after that
comparison; never call a qualified theorem reviewed_exact.
Each qualified field must be a field of a structure in the same Lean module
and have a kernel-checked theorem named holListArrayWitness_<field>. Its
result type must establish RepresentsHOLNodeList for that field and a HOL
list, without assuming RepresentsHOLNodeList in its premises. The reference
checker enforces this shape and Lake checks the theorem proof, but those gates
do not independently establish the cross-language correspondence. Review the
witness and HOL/Lean theorem statements manually; the qualifier does not
authorize changed evaluators, errors, quantified types, side conditions, or
conclusions. If bounds or out-of-range behavior differ, leave the theorem
untagged and document the mismatch beside it.
Representation witnesses alone do not establish transition equivalence. Review successful updates, invalid representations, and out-of-range errors separately before tagging any transition theorem.
Port the executable path, too. As HOL definitions are ported, make the
compiler that flapjack-compile actually runs call the reviewed @[hol]
definitions. A tagged proof-only duplicate beside a different production
implementation is an intermediate step, not completion of the compiler port;
track the production replacement in a dependency-linked bead and test the executed path
against the original Pancake output. Keep a different executable implementation
only for a documented, material performance reason (for example, avoiding a
whole-array copy for each element update), and state the exact relationship to
the HOL-shaped definition and the evidence for the exception. Do not use a
performance exception merely because an existing Flapjack helper has a more
convenient interface.