القائمة
Techniques for developing proof tools in Isabelle, including understanding HHF (Hereditary Harrop Formula) proof state representation
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
Operational pipeline to start, monitor, STOP, and recover the MathBench missing-lemma loop running in multi-node fleet mode on the MBZUAI cluster (watcher + slurmx fleet REPLs + login-node RPC host + serial adjudication + phase-2 import reconciliation). Use when launching/resuming the fleet run, stopping it cleanly, recovering after a crash, or applying the hard-won operational rules (correct kill sequence, git safety on the shared checkout, shell/conda/timeout fixes, re-collection prerequisite). For the single-machine AoA×PutnamBench eval use `aoa-putnam-eval` instead; for the design rationale of the loop see `MISSING_LEMMA_LOOP.md`.
How to refresh the local semantic embedding database (~1.5 GB of LMDB at ~/.cache/Isabelle_Semantic_Embedding). The development channel is the Hugging Face Hub tarball via manage_data.py (get/update). End users instead pull it anonymously from Cloudflare R2 with `semantics_manage.py pull`. Use when setting up or refreshing the semantic DB on a machine, or when deformalizations / vector stores are stale or missing. Do NOT run R2 `push` — it overwrites the shared remote and is a human-only action.
How to repackage/upload and download/unpack the Isabelle + paired AFP distribution, published together as contrib/Isabelle2025-2_and_afp-2026-05-13.tar.zst on the Hugging Face Hub (via manage_data.py update/get). Use when publishing a rebuilt Isabelle+AFP tarball (after isabelle scala_build, patches, etc.) or installing/refreshing the distribution on another machine.
How to read Isabelle introduction and elimination rules
Playbook for adding a new import to MathBench_ProverBase and reconciling any syntax conflicts (constant/type short-name resolution and notation) so that PutnamBench problems still parse to identical goal terms. Use when adding/changing imports of the MathBench_Prover session, or when investigating MathBench-vs-PutnamBench environment divergences.
How to read constants and theorems generated by Isabelle datatype and codatatype definitions
استنادا إلى تصنيف SOC المهني
| name | isabelle-proof-tool-development |
| description | Techniques for developing proof tools in Isabelle, including understanding HHF (Hereditary Harrop Formula) proof state representation |
This skill provides essential techniques for implementing proof tools in Isabelle, with a focus on understanding how Isabelle represents proof states using HHF (Hereditary Harrop Formula) format. This knowledge is fundamental to building tactics, automated provers, and other proof automation tools in Isabelle.
HHF has the general form:
⋀x₁...xₘ. H₁ ⟹ ... ⟹ Hₙ ⟹ A
Where m, n ≥ 0; A is atomic or recursively HHF; H₁, ..., Hₙ are recursively HHF.
CRITICAL: HHF MUST use meta-logic operators ⋀ and ⟹, NOT object-logic operators ∀ and →
IMPORTANT: When an HHF sequent represents a proof state, it encodes subgoals in a specific way.
Example:
(⋀x y. A ⟹ B ⟹ C) ⟹ (⋀z. D ⟹ E) ⟹ F
This represents a proof state where:
How to read: At the top level, each (⋀vars. premises ⟹ goal) structure before the rightmost element represents one subgoal. Within each subgoal, the meta-quantifiers (⋀) bind local variables, and the nested ⟹ separate premises from the subgoal's conclusion. The rightmost element is the ultimate goal, shown once all subgoals are solved.
The ultimate goal is actually wrapped by an invisible operator Pure.prop :: prop ⇒ prop (not printed). This distinguishes the ultimate goal from intermediate subgoals.
Why needed: Consider these two different proof states:
... ⟹ Pure.prop (A ⟹ B) - Ultimate goal is A ⟹ B; no subgoals remain... ⟹ A ⟹ Pure.prop B - Ultimate goal is B; one subgoal remains (premise A → show B)Without Pure.prop, these would be ambiguous.
Isabelle maintains HHF in normal form where:
A ⟹ B ⟹ C means A ⟹ (B ⟹ C)Key modules in contrib/Isabelle2024/src/Pure/:
Pure/logic.ML - Meta-logic operations including HHF manipulationPure/term.ML - Term structure (handles ⋀ and ⟹)Pure/thm.ML - Theorem representationPure/goal.ML - Goal/subgoal operationsPure/Proof/proof.ML - Proof state structure