Add --dumpheap and -g flags for Holmake (issue #1917)#1928
Open
charles-cooper wants to merge 4 commits intoHOL-Theorem-Prover:developfrom
Open
Add --dumpheap and -g flags for Holmake (issue #1917)#1928charles-cooper wants to merge 4 commits intoHOL-Theorem-Prover:developfrom
charles-cooper wants to merge 4 commits intoHOL-Theorem-Prover:developfrom
Conversation
--dumpheap: save Poly/ML heap checkpoints at proof boundaries -g: run proofs through goalFrag, show goal state on failure New modules and flags: - TacticStep.sig/sml: consumer helpers for tactic fragment navigation (fragment text/classification, step plan generation, select merging) - TacticParse: expose flatten_frags + reexpand_thenlt_frags (structurally fix linearize's ThenLT opacity bug inside >> chains) - Globals: holmake_dumpheap_flag, holmake_g_flag, holmake_allow_cheat, holmake_tactic_timeout refs - HM_Cline: --dumpheap, -g, --tactic-timeout options - BuildCommand: thread flags to child hol process cline - hol.ML: parse new flags, set Globals after loadState Prover implementation (holmakebuild.sml): - Fragment-stepped prover for -g --dumpheap: per-fragment ef() calls for navigable checkpoints (context + end_of_proof saves) - One-shot goalFrag prover for -g alone: diagnostics only - Basic prover unchanged for no flags - Tactic timeout: inline Thread.fork+Mutex+ConditionVar, per-step for fragments, per-proof for one-shot - Proof attrs fallback: has_proof_attrs → one-shot (wrapper not in source) - Eager cache cleaning after each proof Critical fix (poly-init2.ML): - Add Globals + CoreReplVARS to loadedMods so Meta.load skips them after loadState. Without this, Meta.load re-runs Globals.sml via use, creating fresh ref cells that shadow the ones set by hol.ML main() Also: - bin/hol.ML: backward-compat flag extraction (dead code from 2016) - boolLib.sml: set Globals.holmake_current_thm during store_thm
…elds) Develop added --thmsrc (FRU16). Our branch added --dumpheap/-g/--allow-cheat --tactic-timeout (FRU19). Merged to FRU20 with both field sets.
holmakebuild.sml used Thread, Mutex, ConditionVar, and PolyML.SaveState which don't exist in Moscow ML. Extract these into a PolyRuntime module with platform-specific implementations: - src/portableML/poly/concurrent/PolyRuntime.sml: real implementations (thread-based timeout, PolyML.SaveState heap save, PolyML.compiler eval) - src/portableML/mosml/concurrent/PolyRuntime.sml: no-op stubs (features gated by Globals refs which are always false on mosml) holmakebuild.sml now uses PolyRuntime.tactic_timeout, .save_heap, .eval_sml_string instead of inline Poly/ML-specific code.
…oofman holmakebuild.sml in src/1/ cannot reference goalFrag, proofManagerLib, etc. because they're in src/proofman/ which builds AFTER src/1/. On Poly/ML this worked via heap-resolved references, but mosml compiles each directory independently and needs .ui dependencies in sigobj. Fix: restore holmakebuild.sml to the original basic_prover (no goalFrag deps). Move advanced provers to holmakebuild_prover.sml in the new src/proofman/poly/ directory (builds after goalFrag is available). Poly BuildCommand links holmakebuild_prover.uo before the script when -g or --dumpheap is active. Mosml doesn't use these features (Globals refs are always false) so basic_prover suffices.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
co-authored by claude opus 4.6
Summary
Add
--dumpheapand-gflags to Holmake for heap checkpointing and proof diagnostics. Closes #1917.Flags
--dumpheapcursor_checkpoints/<thm>_{context|end_of_proof}.save)-g-g --dumpheap--tactic-timeout=N-gactive)New modules
src/parse/): Consumer helpers for tactic fragment navigation — fragment text/classification, step plan generation, select-step merging. Used by both holmakebuild and the LSP server.flatten_fragsandreexpand_thenlt_frags— structural decomposition functions that fixlinearize's ThenLT opacity bug inside>>chains.Prover modes (holmakebuild.sml)
basic_prover(TAC_PROOF)-g--dumpheap-g --dumpheapef()calls, context + end_of_proof checkpointsKey fix: loadedMods in poly-init2.ML
GlobalsandCoreReplVARSare loaded viauseinpoly-init2.MLbut were not added toloadedMods. WhenMeta.loadencountered them as dependencies (e.g.,holmakebuild.uo → Globals), it re-ranGlobals.sml, creating fresh ref cells that silently shadowed the ones set byhol.ML'smain()afterloadState. Adding them toloadedModsprevents this re-load.Changed files
src/parse/TacticStep.sig/sml— new modulesrc/parse/TacticParse.sig/sml— exposeflatten_frags,reexpand_thenlt_fragssrc/1/holmakebuild.sml— prover implementation, checkpoint logic, tactic timeoutsrc/1/boolLib.sml— setGlobals.holmake_current_thmsrc/prekernel/Globals.sig/sml— new holmake flag refstools/Holmake/poly/HM_Cline.sig/sml— CLI optionstools/Holmake/poly/BuildCommand.sml— thread flags to child processtools-poly/hol.ML— parse new flags, set Globals after loadStatetools-poly/poly/poly-init2.ML— loadedMods fix, early Globals loadtools/parsing/HOLSourceExpand.sig/sml— tactic text storage, holmake_active flagtools/parsing/HOLSource.sml— expSpan exportbin/hol.ML— backward-compat flag extraction for directhol <state> <files>invocations