Feature request: cross-file suspend/resume

[charles-cooper]

co-authored by claude opus 4.6

Motivation

The current suspend/resume mechanism is a great tool for structuring proofs within a single script file. However, it's limited to intra-file use: the suspension DB is an in-memory Sref, the ExportTheory hook enforces that all suspensions are finalised before the script ends, and nothing is persisted to the theory file on disk.

There are cases where it would be useful to suspend a subgoal in one theory and resume it in a downstream theory — for example:

• Layered developments: A foundational theory establishes the main structure of a proof but a subgoal requires machinery (definitions, lemmas) that naturally belongs in a later theory. Currently, you must either anticipate and manually state the subgoal as a standalone lemma, or restructure the theory hierarchy.

• Large proof efforts: Splitting a proof across files can help manage complexity. The suspend/resume pattern already captures the exact goal context (assumptions, free variable bindings), which is more convenient than manually reconstructing the subgoal statement as an independent lemma.

Current behaviour

• suspend stores the incomplete theorem in boolLib.suspensionDBref (in-memory Symtab)
• ExportTheory hook raises an error if any suspensions remain unfinalised
• Finalise must appear in the same script file

Possible approach

One way to support this:

1. Allow suspended theorems to be serialised into the theory file (e.g., as a new kind of stored theorem with suspendlabel hypotheses intact)
2. Provide a way to import/access them in downstream theories (e.g., load_suspension "TheoryName" "thm_name")
3. Finalise in the downstream theory would discharge the suspension hypotheses and save the completed theorem (possibly back-patching the original theory, or storing it in the finalising theory)
4. The ExportTheory check could be relaxed to allow explicitly marked "deferred" suspensions

Open questions

• Should the finalised theorem live in the original theory or the one that finalises it?
• How to handle theory rebuilds — if the upstream theory changes, suspended goals may no longer match
• Should there be a mechanism to declare which suspensions are intentionally deferred vs accidentally left open?

[mn200]

I agree this is an appealing feature. Another issue is merging resumptions that are handled in distinct child (or grandchildren, ...) theories. If the exported suspension is

  [S1, S2] |- Phi

and two distinct sibling descendants prove the two suspensions, they will generate the theorems [S2] |- Phi and [S1] |- Phi. These can't be combined to generate the desired |- Phi so the machinery will need to store and export the S1 and S2 results when goals haven't been finalised.

[xrchz]

Proposed design: functional suspend/resume with cross-file support

This design also addresses #1881 (re-runnable Resume).

Core idea

Instead of the current destructive-update approach (where Resume mutates the suspended theorem in an in-memory DB by discharging hypotheses), we move to a functional/pure model:

1. The original suspended theorem is immutable — saved to the theory as a normal theorem (with suspendlabel hypotheses)
2. Resume produces a standalone proof of one suspension hypothesis, tagged with a new resumelabel marker constant
3. Finalise assembles everything — finds the original theorem and all resumption proofs, applies PROVE_HYP for each, saves the clean result

New marker constant

A new constant in markerTheory:

resumelabel (s:label) (l:label) (arg:bool) = arg

where s encodes the theory-qualified suspension name (e.g., thy$thm) and l is the label name.

Lifecycle

Theorem thm: stmt Proof ... suspend "lab1" ... suspend "lab2" ... QED

Produces [suspendlabel "lab1" G₁, suspendlabel "lab2" G₂] ⊢ Φ and saves it directly to the theory segment as a regular theorem.

Resume thm[lab1]: tac QED

• Finds the suspended theorem via DB.fetch (current theory or ancestors)
• Extracts the goal from the suspendlabel "lab1" G₁ hypothesis
• User proves it with their tactic
• Wraps the result using resumelabel_def to produce ⊢ resumelabel "thy$thm" "lab1" (suspendlabel "lab1" G₁)
• Saves this as a normal theorem (with a systematic name like thm_lab1_resumption, or user-specified via smlname)

Finalise thm[attrs]

• Fetches the original suspended theorem
• For each suspendlabel hypothesis, searches for a theorem whose conclusion matches resumelabel "thy$thm" "labᵢ" Sᵢ — in current theory, then ancestors
• Unwraps each via resumelabel_def, applies PROVE_HYP
• Checks no suspendlabel hypotheses remain
• Saves the clean ⊢ Φ

Resume syntax for cross-file use

Resume can optionally take a theory-qualified name:

Resume ParentTheory.thm[lab1]: tac QED    (* explicit *)
Resume thm[lab1]: tac QED                 (* searches current theory, then ancestors *)

What gets deleted

The entire in-memory suspensionDBref and associated machinery (find_suspension, remove_suspension, update_suspensionDB, check_DBempty, and the ExportTheory hook) can be removed. Theorem lookup moves to DB.fetch. This is a significant simplification.

Why this solves #1883 (cross-file)

Suspended theorems and resumption proofs are ordinary saved theorems. They persist across theory boundaries automatically. A downstream theory just does Resume and Finalise — no special loading step needed.

Why this solves #1881 (re-runnable Resume)

Since Resume never mutates the original theorem, re-running Resume thm[lab1] just re-proves and re-saves the resumption proof. The original [S₁, S₂] ⊢ Φ is untouched. (Trade-off, as noted in #1881: label reuse within resumptions would no longer be supported.)

Why this solves the sibling-theory problem

If TheoryA exports [S₁, S₂] ⊢ Φ, then TheoryB can resume lab1 (saving ⊢ resumelabel ... S₁) and TheoryC can resume lab2 (saving ⊢ resumelabel ... S₂) independently. A grandchild TheoryD can Finalise by finding the original in TheoryA and the two resumption proofs in TheoryB/TheoryC, combining them all.

Open details

• Naming convention for saved resumption proofs: needs to avoid clashes with user names. Exact convention TBD.
• Local/export behaviour: when Finalise happens in the same file as Resume, the resumption proofs are intermediates — default to local (not exported). When the suspension isn't finalised by export time, they're saved normally. Should there be an attribute to override the default (e.g., force-export a resumption proof even when finalised locally)?

[myreen]

Befors this is considered complete, I hope it's tested to work with Holmake --fast #1909.

[xrchz]

I believe this is solved by #1912