Conversation
ThmSetData's stored-attribute path records an ADD delta before applying
it to the global value, so a set type whose apply_to_global rejects the
theorem leaves a delta that raises again in every descendant theory.
That is an upstream bug, present independently of this work, and fixing
it belongs in its own change: restore src/1/ThmSetData.sml,
src/parse/AncestryData.{sml,sig} and the Portable.uninterruptible
primitive added for it to their upstream state.
KeyedThmSet's own export_thm keeps updating before recording -- that is
local to code introduced here and needs no shared-code change -- and the
IndDef selftest now checks only the diagnostic on the stored-attribute
path, since persistence there is governed by the upstream ordering.
path_11 exists only to supply the one_one field of the path TypeBase entry; stopped_at_11 and pcons_11 are already exported and simp-tagged, so the conjunction added nothing to pathTheory's public namespace. Also drop the redundant trailing semicolons on the two Theorem value-bindings added alongside it.
The level-2 quality gate had been un-runnable since eb9def1. Holmake never typechecks selftest.sml -- on Poly/ML a .uo is a load script, so the file is compiled by quse declaration by declaration as it executes -- and execution aborted early enough that roughly 20000 lines had never been compiled at all, let alone run. Kernel and harness: - theory_is_available asked for the current theory through Theory.current_theory, which raises when there is no theory segment. [bin/hol run] loads no prelude, so a script reaching [load "Refute"] hits exactly that state. Ask the way Theory.get_parents does. - selftest.sml opens a scratch segment for the same reason, and shadows check_result so an exception from a predicate is one failed test rather than an aborted file: testutils.timed guards the function it runs but not the predicate it then applies, and the idiom used throughout this file does its work in the predicate. - the tests that enter the pipeline below refute_problem now mint the dynamically scoped call token themselves and release run resources on the way out, as refute_problem does. Without it the smart gate raised "no active Refute call"; with a token but no release, a cache entry is stranded under a token nobody can look up again and its compiled_test is never closed. Non-termination and soundness in the narrowing backend, which had never executed because the committed module did not typecheck: - Refute_QC_Narrow wired retry_potential to an unbounded self-call, so a failed certification replay re-entered the same schedule entry for ever with a growing ignore list -- the list was the heap growth, and upd_size could not bound it because the recursion happened inside one entry. Charge retries at an entry to a budget, as the random driver already charges its own. - visit_examples derived an example's genuineness from leaf values alone, dropping the demotion the rest of the module applies to an approximated domain. Under upd_certify false this reported a Genuine counterexample to the true goal !x:num. ?y. y = SUC x. Also: name the registry that actually refused when Cv rejects a type. The custom and abstract generator registries are disjoint, so "custom or abstract generator registered" sent the reader looking for a register_generator call that need not exist. Regression tests accompany each fix. Level 1 now runs to completion in under two minutes at ~2.4GB peak, down from a 148GB runaway; failures are 41, all pre-existing defects this makes visible for the first time.
Eleven interactive transcripts plus a README covering the user-facing
surface: the entry points and verdicts, datatypes and functions, the
three substrates and determinism, smart generators, narrowing, custom
generators, the unused-assumption sweep, the model finder, and the
extension points.
These are session transcripts, not theory scripts -- Holmake ignores
them. Each was run through
bin/hol --holstate=refuteheap < examples/<file>
and the prose reconciled against what actually came back. Files 09 and
10 need a Kodkodi component and a Java runtime; without one those calls
report Unknown rather than failing.
Several transcripts currently describe defective behaviour as though it
were designed -- the certification gap in 03, the potential-only
sections and the full-copy typedef workaround in 10, the ersatz
weakening in 11. They need re-running and rewriting as those defects
are fixed.
register_quotient documented two accepted registration theorems and had a destructor for each, but quotient_theorem_info only ever called dest_bare_quotient and hardcoded the partial flag, so dest_total_equivalence was dead code and every total extensionality theorem was rejected as an unsupported shape. ratTheory.RAT_EQUIV is one, so four selftests -- the public registration validation, the frac registration merge, the quotient axiom goldens and the refute$qn display pins -- all died in their first registration call. The dispatch is on the conclusion's head constant rather than on a failed parse. A QUOTIENT conclusion cannot also be a universally quantified equation, so the head decides the shape outright, and each destructor keeps its own diagnostics; parsing as QUOTIENT and falling back to the total branch on failure would report a malformed QUOTIENT theorem as a malformed equivalence. The abs/rep cross-check stays on the QUOTIENT branch alone, because a total equivalence names only the representation relation and cannot identify supplied constants. Both destructors now raise one message naming both accepted shapes: neither alone can tell which one the caller was aiming at, so the old bare "unsupported shape" was not actionable. The second bijection law of a typedef reached the encoding as the exported biconditional P r <=> rep (abs r) = r. That cannot work: for an r outside P the value abs r is unrepresented, so the equation is unknown rather than false, the biconditional is unknown rather than true, and no scope of a proper-subset typedef was satisfiable. The model finder therefore found nothing at all for such a type, while a whole-type typedef was unaffected -- zoo_three's own ABS/REP law had no model at any cardinality row, zoo_univ's did. The encoding now sees P r ==> rep (abs r) = r together with the surjectivity P r ==> ?a. rep a = r. The guard drops exactly the half that mentions unrepresented values, and the surjectivity restates that half without naming abs, so the abstract carrier stays pinned to P's extension instead of to some subset of it; without it a typedef pinned below its true cardinality yields spurious models. With the membership axiom the pair is equivalent to the biconditional, so no model is gained or lost. A whole-type typedef degenerates to T ==> ..., and the registration accessor still reports the theorem's own conjuncts -- only preprocessing sees the restatement. The level-1 failure count goes from 41 to 37, removing exactly those four failures and adding none.
Three defects in Refute_Extract, all in code the selftest had never reached, accounted for nine level-1 failures. Generated names. 556d5c6 made binder names injective, escaping every non-alphanumeric character behind a v_ prefix, and routed upper_name and lower_name through the same function. Those two mint names for generated datatype constructors and generated functions, which are already separated by a fresh serial -- C_CONS_refute_ty_3 became C_v_CONS_urefute_uty_u3 and f_rx_odd_1 became f_v_rx_uodd_u1 for no gain beyond unreadable output. Worse, the same function names SML type variables, and the escaping ate the leading quote: :'a compiled to the value identifier v_pa, which is not a type at all. Injectivity now belongs to clean_name and binders alone; sanitize_name restores mere character legality for the names Refute mints itself. Constructor patterns in strict mode. fa026fc pointed strict definition clauses at the observation matcher, so that a char-list CONS would never be rendered as an SML pattern. The matcher only knew how to observe generated datatypes, but strict extraction keeps lists, options and pairs in their native SML representations and mints no datatype for them, so every definition matching on [] , ::, NONE, SOME or a pair rejected the whole goal with "unknown lazy pattern constructor list$NIL". It now emits the native patterns the strict expression compiler already emits for those constructors; the lazy representation, where every type is a datatype, is unchanged. Unrequested structural equality. f2b0f24 stopped compile_types from requesting equalities, but equality_declarations declared one per registered type in strict mode regardless of what was requested, so the removal changed nothing. A representation-only compilation still emitted structural equality for every type it touched, and any type mentioning an arrow failed outright, because equality on a function has to enumerate its domain. Both modes now declare exactly the requested set. Discovery cannot widen the declared type set behind the datatype declarations that precede it: ensure_type already registers every constructor argument, element, domain and range type. The byte golden moves from 3359/3964 to 3461/4157 bytes. It was last recorded at 6156067, before four later commits that legitimately changed emission -- variables carry a type key since 2aebf52, definition clauses go through the observation matcher since fa026fc, its nonlinear patterns since 42beb32, and smart generator outputs bind before residual checks since f66f652 -- so no fix could have restored the old digest. The emitted source was read in full: the strict program is the prelude, no equality declarations, and one native list match; the lazy program adds the hole helper, the two-constructor refute_ty_3 declaration and its suspended spine. The level-1 failure count goes from 37 to 28, removing exactly those nine failures and adding none.
Eleven level-1 failures across the model-finder translation pipeline came from one library defect and five stale goldens. The defect is a8e7d31. It wanted a partially applied BIT1 to translate, and got there by dropping NUMERAL, BIT1 and BIT2 from built_in_consts. But that table is what every earlier stage consults: def_props_for_const, unfold_defs_in_term, specialize_consts_in_term, add_to_uncurry_table and box_type all ask is_built_in_const, so a literal 5 stopped being a numeral to all of them. It was unfolded and specialized into refute$sp3$arithmetic$NUMERAL with the definitional axioms BIT2 = ZERO + (ZERO + SUC (SUC 0)) in tow -- unary arithmetic, which is exactly what the comment a8e7d31 deleted had warned about. Binarization then never triggered, skolemization and case unfolding goldens drifted, and the live bridge stopped firing smart binary integers. The skeleton goes back on the table and the nut layer, which already recognizes a fully formed numeral before it looks at heads, expands what is left: NUMERAL n as n and BIT1/BIT2 n as 2n + 1 and 2n + 2. A bare constructor eta-expands into the same case rather than reaching the arity-0 built-in branch, whose only outcome for it was to raise. That fixes the built-in count and never-unfold pins, all five preprocessing goldens, and one live-Kodkodi failure. Five goldens recorded behaviour their own commits had already changed. min_univ_card_of_rep of Opt (Struct [Atom (2, 0), Atom (3, 2)]) was pinned at 6. An Atom (k, j0) occupies indices j0 .. j0 + k - 1, so Atom (3, 2) reaches index 4 and demands 5; the implementation has said k + j0 since 670b9b1, which introduced both halves, so the golden was arithmetic that never held. The scope facto pins predate 79c8070, which made concreteness quantify over the constructor argument types rather than over the binder types of each argument type -- the latter is empty for every first-order field, so the old test only ever exercised the trivial case. A num list whose num is capped at an inexact 2 is now inconcrete under both facto values, and therefore exact under neither; completeness still carries the facto-sensitivity the test was written for. certify's Discarded arm returned a Potential carrying "certification refuted the model" until 8d7f8c1 made it Drop, on the ground that kernel evaluation has refuted the assignment at every certainty level. Its Certified arm stopped merging decoded solver values into the evaluations at 569bbc4 and stopped attaching the reconstruction report at 96676da. The certified eval is now the kernel's own, which for the underspecified HD [] is the term itself, and the test pins model = NONE as well. certification_copy has taken the reconstruction's per-type atom rows since c16c124, so that custom atom names certify; the merged-type-var fixture still passed types = [] and could no longer produce an atom substitution. It now carries the row MFM.reconstruct produces. tests/mf-binary-integers.kki still encoded Num as Isabelle's clamping nat, if i <= 0 then 0 else i. HOL4's Num is @n. if 0 <= i then i = &n else i = -&n, that is ABS (integerScript.sml:1888, with Num (-a) = Num a at 1946), and fd828ee corrected the translation without regenerating the golden. tests/forl-expressions.kki was hand-edited by c2c8766 rather than regenerated: that commit made the bitwise operators parenthesize their right operand, which changes 1 & (2 & 3) and 1 | (2 & 3) but not the left-nested BitXor (BitXor (1, 2), 3), whose correct rendering stays 1 ^ 2 ^ 3. The level-1 failure count goes from 28 to 16, removing exactly these eleven plus "smart binary integers did not fire on the arithmetic goal" and adding none.
mn200
requested changes
Sep 23, 2026
mn200
left a comment
mn200
left a comment
Member
There was a problem hiding this comment.
Documentation has multiple instances of similar problems:
- scripting should be used for the DESCRIPTION manual
- doc-files must conform to template
- some doc-files seem as if they can be omitted
Source-code:
- structures should almost always have signatures
I'd like to see the IndDefLib changes pulled out into a separate PR.
| [`Refute.try_refute`](#Refute.try_refute), | ||
| [`DB.thms`](#DB.thms) | ||
|
|
||
| The complete library guide is \ref{Description:the-holrefute-library}. |
Member
There was a problem hiding this comment.
Please don't have text after the See-also list of idents
Member
There was a problem hiding this comment.
Doesn't conform to template (in help/template), which calls for an hrule after the type block and a one-line summary.
| them. | ||
|
|
||
| ``` hol4 | ||
| val cfg = Refute.default_config |
Member
There was a problem hiding this comment.
This should use scripting (with leading >>) so that the code actually runs and produces appropriate output in the generated file.
| [`Refute.try_refute`](#Refute.try_refute), | ||
| [`Refute.find_unused_assms`](#Refute.find_unused_assms) | ||
|
|
||
| The complete library guide is \ref{Description:the-holrefute-library}. |
Member
There was a problem hiding this comment.
Don't put material after the see-also section
| are exactly those where that numeral is missing. | ||
|
|
||
| #### Types the executable backends can test | ||
|
|
Member
There was a problem hiding this comment.
Does this mean that loading Refute adds a dependency on the theories of rationals and reals?
| that constant; when the model finder builds its tables, a clause with | ||
| no constant head is dropped with a warning. | ||
|
|
||
| Structural registrations require distinct type variables as parameters |
Member
There was a problem hiding this comment.
Would it be better to have this meta-data generated and stored by default.
Member
There was a problem hiding this comment.
This file should have a signature
Member
There was a problem hiding this comment.
This file should have a signature; and using ref for global values is extremely suspect.
Member
There was a problem hiding this comment.
This file should have a signature
A server gets the heap its directory's Holmakefile asks for, and up to src/boss that heap is bin/hol.state0, which has boolLib, proofManagerLib and DB but nothing from src/coretypes onwards. defnbase_init named DefnBase, so a server in src/num/theories died compiling its own startup files. The store of user definitions is DefnBaseCore's, which that heap has; DefnBase only re-exports the lookup. A startup step that will not compile now costs its own feature rather than the session, and says which one in a window/showMessage sent once the handshake is done. Dying there is the one failure a client cannot be told about: it happens before initialize is answered, so all it can report is that the server exited. What such a step writes now reaches the user too. Claiming stdout for the JSON-RPC frames, and pointing TextIO.stdOut at stderr, is what stdioConnection has always done on the server's behalf, but it ran after the startup files had been compiled, so their diagnostics went onto the wire and were eaten. LSPServer.claimStdout is that same hijack, callable before anything else runs. The init-file load test ran on the full heap alone. It runs on hol.state0 as well now, and fails if the heap and the --bare flag disagree, so dropping the flag cannot leave it quietly testing the same heap twice. Its files are dependencies of every log in that directory: editing one changes what all three exercise while leaving each object file alone. A protocol test covers the same ground from outside, by serving a directory that names hol.state0 as its heap. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A proof the LSP defers is replayed under Context.with_context, which answers that thread's ambient reads from the proof's own context. Writes still go to the live cell, and srw_ss() initialised itself by writing the folded state back and reading it again, so under a pin it answered with the state unfolded: no TypeBase simpls, and none of the updates the ancestors had parked. A script that builds its own tactics out of srw_ss() -- what the theories below src/boss do, the context-reading shim covering a declaration's own reads and not a top-level function's -- then ran its proofs against a fraction of the simpset. Three proofs of arithmeticScript that a build proves were reported as failures, and stepping through them showed them going through, a walk restoring the context rather than pinning it. Under a pin the fold happens in place and the live cell is left alone. Context.is_pinned answers from the counter ambient reads already consult, so a session with no proof replaying pays nothing for it. The fold itself is now shared by a one-entry memo, keyed on the identity of the state and the TypeBase it folds in. A read that must not write has nowhere else to keep its answer, and the fold is 3ms: it ran 651 times while listTheory built, and says so in the log each time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A script that defines its own simp from srw_ss() reads the ambient simpset: the context-reading shim covers a declaration's own reads, not the ones a top-level function makes. The expander defers the tactic expression to when the proof runs, so such an alias reads whatever the process is doing then, and for a proof the LSP has deferred that is under a pin. A Proof[exclude_simps = ...] window does not reach it either. Eta-expanding to the goal and the context, and taking the simpset from that context, is what srw_tac has always done and what these aliases mean. The val-bound aliases inside the local blocks of listScript and rich_listScript keep their ambient read. One of those is bound once and frozen where it sits, which is not the same thing as a proof's context, and widening it left rich_listTheory not terminating. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
one_line_ify collapses an argument column whose type has one constructor and whose pattern variables the right-hand side ignores, replacing the pattern with a variable in every clause. The test for that admitted a column as soon as one clause qualified, so a definition whose other clauses do read those variables had equations built for it that are not theorems, and the finisher reached GENASSUME with a residual rather than T. A function taking a string and an index as a pair is enough to meet this: whichever clause raises an error ignores both components. Clauses already holding a variable there are untouched by the collapse, so they still pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A hover on a documented identifier carries the text of its Reference entry below the type, and a link to the file that text was read from. The entry's own cross-references -- its "See also" list, and the "Also exported as" banner on an alias -- are written against the single-page anchor scheme the manual used to have, which resolves to nothing in a hover, so each points at the entry it names. Both come from Manual/build/Docfiles-processed, the polyscripter- evaluated mirror of help/Docfiles that bin/build writes: markdown a client can render, where the .txt beside each source is a pandoc plain-text rendering and the source still holds its frontmatter and directives. A tree built with --no-helpdocs has neither that mirror nor the index, and a hover there shows what it always did. LSPExtension.helpLookup has been called by the hover since it was written and has never had an implementation: the only thing that installed it was Help.sml, which a language server does not load. It is lsp/help_init.ML's now, beside the other server-start files, and Help.sml goes back to being a terminal pager for help. The index is read once, on the first documented hover, and a tree that has none is remembered as having none.
The processed Reference entries are not finished markdown: mdbook runs
smdpp over them. A hover renders them as they stand, so it shows the
pandoc-only constructs that neither the book nor the PDF ever
displays -- \index{}, \label{}, and ```{=latex} / ```{=html} raw
blocks, body and all. A ```{=mdbook} block keeps its body.
Whose correct rendering is nothing at all, which is why they are worth
removing before an entry uses one: an author has no reason to expect
such a construct to surface, so nothing would stop them writing it,
and the hover would be the only place it appeared.
What smdpp resolves -- \ref{}, \refentry{}, \cite{} -- is left as
written. It renders as literal text, and a cross-reference the reader
has to look up beats a deleted one. Should entries start using them,
the pass belongs in process_docfiles, where doing it once would make
the processed tree markdown in name as well.
No entry carries any of this today, so the check is a load-time
selftest rather than a case in the protocol suite: a test driven from
the built tree would pass over nothing and read as a clean result.
Generate the DESCRIPTION chapter's transcripts with polyscripter (only the Kodkod session stays static), bring the reference entries to the help/template shape, and drop the entries for thin wrappers, which their parent entries now mention.
Drop the entries for extension hooks a proof author does not call (register_backend, register_frac_type, register_ersatz, register_generator_family, harvest_registrations) and for thin wrappers (export_refute_*, whose theorem attributes the DESCRIPTION now documents; try_refute, folded into refute_goal). The hooks keep their contracts as comments in Refute.sig. Bring every remaining entry to help/template: a Failure section in each, and a See-also list ending in a period. Correct the refute_psimp condition, abstract_generator's constructor requirement, and when the model finder registers typedefs and quotients by itself.
Every HolRefute structure now has a signature, ascribed opaquely, and no module keeps a global ref. Registries, caches and the configuration are Context.Data slots owned by the new Refute_Session: a Refute call reads the context captured at its entry, shares that view with its worker threads, and at exit commits its cache changes to the live context unless something else changed them meanwhile. Registrations publish straight to the live context and to the calling view. Every change serialises on its state's lock and runs its callback outside the view's lock, so a callback may read any state. The configuration ref becomes set_config / current_config / with_config, and REFUTE_TAC reads the configuration of the context it runs in. Cross-call caches go stale by a generation token held in their own state instead of global counters. EvalSML's term-table registry is gone: the host scopes the tables around dispatch and each reconstruction. EvalEnum chooses a fresh definition prefix against the theory's current names, and its unreachable failure hook is deleted. The selftest moves to the new configuration API and pins a registration made from inside a Refute call.
The docfiles still described the removed the_config ref; they now describe the stored configuration and set_config / with_config / current_config. REFUTE_TAC_WITH's failure clause covers updaters validated only when applied. Each fact now lives in one entry: the term-level wrappers and the Model/NoModel outcomes in refute, the generator replacement rule once per generator entry. Rewrap two over-long lines in the DESCRIPTION chapter.
A review of the branch against develop found helpers written more than once, hand-rolled library functions, dead code and some wasted work. Mechanical, behaviour-preserving fixes only. Shared instead of copied: factor_types, premise_head, theorem_term and close_free, rf_type, remaining, int_of_numeral, data_type_spec, chop, an argmin (least_by), the Potential downgrade (Refute_Cert.downgrade), the QC/QC_Narrow run-body skeleton, and the instance rebuild shared by make_instance and transport_instance. Library calls replace hand-rolled code: AList, KNametab list operations, Conv.QCONV, pred_setSyntax set literals, Portable.make_counter, Lib.enumerate where the start is 0. Removed: Model's reconstruct/term_for_rep, define_clique, compile_plan, serial_commas, PropSat.simplify, ParList.get_some, the always-true should_tabulate_suc_for_type and its branches, parameters with a single value (scope cursor iterative flag, extraction mode, termlists_of selector), ~60 unreachable catch-all arms in Refute_Extract, and unused signature entries. Backends now register only through Refute.sml. Less work: record_primitive uses a per-extraction field map instead of scanning TypeBase per application; the builtin codatatype list is checked before the ancestry test; types are deduplicated before classification; all_vars and free_vars_lr are hoisted; quadratic appends are linear; narrowing normalises and converts to PNF once per instance, not per depth. Investigation-log comments are cut to current facts.
Backends declare a family (Quickcheck, ModelFinder or Other), and QuickcheckBackends takes the registered Quickcheck family instead of Refute_QC's hard-coded name list, which also named the narrowing backend Refute_QC does not own.
Refute_Core.sig and the Refute facade each listed the config types and all ~70 updaters; both now include Refute_Config, the facade realising its datatypes as Refute_Core's so the two stay one type.
Extract spelled the literal test out three times. The enumerator's clause-pattern copy lacked word literals, so a word-literal clause input compiled to an unguarded wildcard. No outcome is known to change: a downstream check already filtered the extra candidates.
The three candidate counters travelled as string-keyed stats and were re-parsed, summed and re-rendered in QC, EvalCompute and EvalSML. Refute_Core now owns the qc_counters record, its one rendering into stats and its one summary text, shared by QC's vacuity reason and the witness line.
The four num/int orders were listed in MF_HOL, twice in Nut and in Mono; MF_HOL's order_consts now feeds all of them. Nut's arithmetic if-chain is a key table, and Nut checks at load that its word and char operator tables name exactly MF_HOL's built-in constants.
A backend record now carries an optional render hook returning the scope, bindings and model text of a counterexample; kodkod supplies it, and the scope/model/boxed-type display code moves from Refute_Core into Refute_ModelFinder. Backends without a hook show their bindings with format_term. format_term prints Quot terms through a user printer on a copy of the grammar instead of a placeholder substitution, so long terms containing Quot now wrap at their real width.
The model finder's codatatype, quotient, typedef and frac registries become one operator-keyed table of classifications, so a type operator can have only one. A registration replaces only its own kind; the one exception is Frac, which replaces a quotient or typedef. Built-in codatatypes and fmap's synthetic encoding count as classifications too, so a typedef registration over fmap is now refused. harvest_typedef now answers only for genuine typedefs, which removes the need for Refute_QC.transportable_typedef's raw_typedef_data guard against the synthetic frac/fmap entries.
Refute_Core.call_memo memoises a builder for the running call, backends included: concurrent callers wait for the first build. The model finder's definition/nondefinition tables and the certainty ceiling's nondefinition scan use it, so QC's smart context, every model-finder instance and harvest restarts share one build. Measured on find_unused_assms over sumTheory (2s probes): 16 table builds at ~15ms in 22-23s, about 1%, so no cross-call cache.
Fourteen structures kept their signature inline, three of them as an anonymous `:> sig ... end`. Each now has X.sig declaring signature X, ascribed `structure X :> X`, and the two uppercase signature names (REFUTE_PROP_SAT, REFUTE_MODEL_FINDER_MONO) follow the structure name. Interfaces are unchanged. Refute_Config, which holds only a signature, stays a .sml: holdep makes every reference depend on Refute_Config.uo, which a lone .sig cannot provide.
Contributor
Author
Documentation:
Source-code:
|
upd_search QuickcheckBackends resolved the family's backend names when the update was built, and config_in applied updates outside any session, so the registry read went to the live context. Inside a proof that is the "ambient context read while a proof was running" warning, and a tactic given an older context ran the live registry's backends. The QuickcheckBackends arm now resolves on application, and config_in applies updates in a session over the tactic's context. Either change alone leaves the ambient read; the new selftest fails under each.
TypeBase's accessors read the live context, so a Refute call given an older context saw datatypes defined after it, and a tactic's reads were reported as ambient reads inside a proof. Refute_TypeBase mirrors the twelve TypeBase functions Refute uses over Refute_Session.context, the running call's view, and every call site goes through it. Outside a call the view is the live context, so top-level entry points are unchanged. Refute writes no TypeBase entry during a call, so a frozen view misses nothing the call made itself.
load compiles a module's sources in the caller's top level, so after `open realTheory` the pervasive abs is the theorem of that name and load "Refute" failed with type errors. process_docfiles runs every docfile in one session, and Conv.MP_CONV opens realTheory before the Refute docfiles load the library.
Feedback.emit_MESG, emit_WARNING and emit_ERR switched their flag off and left it off, so every later docfile in the shared process_docfiles session rendered without HOL messages, warnings or error details, among them the Refute tactics' counterexample reports.
With warnings no longer suppressed across docfiles, the Parse.set_known_constants example prints the PROD_IMAGE overload name in its output, and reference.pdf failed with "Unicode character Π (U+03A0) not set up for use with LaTeX".
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
2 participants
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.
Summary
This PR adds
src/HolRefute, a counterexample generator for HOL4 goals, built on Poly/ML only. It provides four diagnostic tactics (REFUTE_TAC,QUICKCHECK_TAC,NARROWING_TAC,MODEL_REFUTE_TAC), the SML entry points behind them, a user manual chapter (Manual/Description/Refute.smd), 16 help docfiles, a selftest with level-2 acceptance tables, theory-hygiene tests, and an executable example corpus adapted from Isabelle's Nitpick manual and example suites.The library has four backends: exhaustive and random Quickcheck, native narrowing, and a Kodkod-based finite model finder. Substrates are untrusted accelerators; every counterexample is replayed and, where replay succeeds, turned into a HOL theorem. HolRefute leaves no type, constant, theorem or binding in the user's theory on any path (success, failure, timeout, interrupt); its only ambient effect is teaching the global
EVALcompset closed:ratarithmetic and:realinv.What is ported from Isabelle/HOL, and how closely
Model finder: a port of Nitpick
The model finder is a module-for-module port of Nitpick (Isabelle2025-2,
src/HOL/Tools/Nitpick). The pipeline, the intermediate languages and the trust model are Nitpick's; the adaptation is concentrated in the HOL-facing layer.nitpick_preproc.MLRefute_ModelFinder_Preprocconjuncts_oforder, axiom-side skolemisation depth).nitpick_mono.MLRefute_ModelFinder_MonoIdand set products stay unfolded (no nut builtin), the Pure meta-connective cases,bounteous_constsand tracing are not ported, andis_harmless_axiomis narrowed.nitpick_scope.MLRefute_ModelFinder_Scopenitpick_rep.MLRefute_ModelFinder_ReprelationTheory) rather than sets of pairs, and the application boundaries are kept.nitpick_nut.MLRefute_ModelFinder_NutBoundNameconvention. Thenutdatatype and its operator enumerations are unchanged;cstgains the word and char operations. OneNatToInttotality bound is deliberately corrected against upstream and marked in the code.nitpick_kodkod.MLRefute_ModelFinder_KodkodNumof a negative integer, curried relations).nitpick_peephole.MLRefute_ModelFinder_Peepholes_all/s_existon an empty declaration,rel_expr_intersectsonAtomSeq,s_join'sUnivclauses) plus the HOL4-side bit-width choice.nitpick_model.MLRefute_ModelFinder_Modelnitpick_hol.MLRefute_ModelFinder_HOLsimps; typedef, quotient and codatatype registries and the ersatz table are re-derived from HOL4 theory data.nitpick.ML(pick_them_nits_in_term)Refute_ModelFindermerged_type_var_table_for_terms, since HOL4 has no sorts.kodkod.MLRefute_Forlkodkodi-1.5.7component, without Isabelle's launcher.kodkod_sat.MLRefute_ForlSat*_HOMEvariables.prop_logic.ML, cdclite part ofsat_solver.MLRefute_PropSatNitpick.thyrefuteScript.smlunknown,wf',wfrec',card',sum',safe_The), with fmap rows added.nitpick_commands.MLconfigrecord withupd_*updaters andREFUTE_TAC_WITH, not Isar syntax.The verdict model is Nitpick's:
Genuine/QuasiGenuine/Potentialis decided by the encoding,max_potentialis charged as in Nitpick (only a genuine model spends amax_genuineslot, where Nitpick's sound branch also charges quasi-genuine ones), and Refute trusts Kodkodi exactly as Nitpick trusts Kodkod (aGenuineverdict with no certificate is valid). Deliberate deviations, all documented in the README and manual:if ?x. P x then @P else unknownwhere Isabelle leaves the occurrence unguarded and constrains it only through the witness-conditionalEps_psimp; a guard vetoesNoCounterexample.NoCounterexampleis a total claim. Anything bounds-relative reportsUnknownwith a reason, and a value-positionunknownin any harvested axiom vetoes it.:charare exact native carriers (2^wand 256 atoms), which turn smart binarization off. Nitpick has no counterpart.realis rational-valued, as in Nitpick. Polymorphic goals are tested at configured monomorphic instances and never earnNoCounterexample, where Nitpick varies the type variables' cardinalities like any other type.sat_solver = "smart"prefers a configured JNI or external solver; Nitpick's smart order never picks a JNI solver by itself.ARBin the raw definition; only the user's equations are harvested, so the same spurious-counterexample risk as Nitpick applies.Quickcheck: design ported, execution re-engineered
exhaustive_generators.ML(theRefute_QCcomment cites the upstream lines). Smart generators follow Isabelle's predicate-compiler design:Refute_SmartGenmode-checks Horn SCCs for positive and negated first-order modes and flattens function equations into graph clauses;upd_allow_function_inversiondefaults off like Isabelle's flag, andupd_use_subtypematchesuse_subtype.random_fun_liftdoes, but eagerly rather than lazily.Refute_Eval.plan) that two substrates run: in-process SML extraction (Refute_Extract) andcomputeLib. Both consume one PRNG in the same order, so a seed reproduces the candidate stream on either.abstract_generators.MLbecomesabstract_generator;find_unused_assms.MLbecomesRefute_Unused(check_/find_/print_unused_assms), with the same maximal-droppable-set semantics.quickcheck_common.MLis not ported: budgets, iterative size deepening, the backend pool and certainty ceilings areRefute_Core's own.Narrowing: generators ported, engine native
The type representation (
Narrowing_sum_of_products),finitize_functionsand the quantifier-pulling pass are ported fromnarrowing_generators.ML. The Haskell engines (Narrowing_Engine.hs,PNF_Narrowing_Engine.hs) are replaced by a native SML narrowing engine (Refute_Narrow,Refute_QC_Narrow), so no Haskell toolchain is needed. Finite function inputs areffunupdate chains defined inrefuteScript.smlinstead of Isabelle's type-scopedConstantnames.HOL4-only additions with no Isabelle counterpart
Refute_Cert,Refute_Cert_Narrow,Refute_Cert_Model): QC hits are replayed withcomputeLib, narrowing replays its case tree, and model-finder values are replayed through Skolem provenance, bounded synthesis, one-layer cases, single-property induction, Presburger andREAL_ARITH. Replay is fail-closed and never weakens the encoding's certainty.ParList, below).theory_tests/checks that a descendant theory inherits nothing.register_generator_family, fmap),Refute_EvalFmapfor ground finite-map equality, and the rat/real compsets.Changes outside
src/HolRefutesrc/portableML/poly/concurrent/ParList.{sig,sml},selftest.sml,Holmakefile(new)A small racing/mapping combinator library over Poly/ML threads:
map_with_workers,get_some_with_workers,get_some,get_first, anduninterruptible_wait.Refute_Coreruns backend admission and the backend race through it (map_with_workersfor admission,get_some_with_workersfor the concurrent pool,get_firstforupd_sequential).Refute_QCusesuninterruptible_waitso the theory-revert cleanup after an interrupted run still completes.Multithreading,Future,Timeoutand nowParListare built by the kernel band with--poly_not_holand linked into sigobj. Naming this directory in HolRefute'sINCLUDESwould rebuild it with the overlay in scope and create anSref -> Overlaydependency that breaks the next kernel bootstrap insrc/bool(documented in HolRefute's Holmakefile).Thread_Attributes.uninterruptibleclears the broadcast flag, and HOL's REPL delivers Ctrl-C asThread.broadcastInterrupt, which Poly/ML drops rather than defers for a thread not accepting broadcasts. A masked join therefore swallowed Ctrl-C.ParListmasks withInterruptDeferinstead and keeps joins observant. Workers are interrupted, neverThread.killed, since a killed worker can leak the process-global theory mutex. Directed-interrupt tests cannot see any of this, soselftest.smldrives the masked windows throughParList_Testhooks. The Holmakefile change only wires that selftest in underHOLSELFTESTLEVEL.src/coalgebras/pathScript.sml,selftest.sml,HolmakefilepathTheoryhad constructors,path_cases, injectivity and distinctness theorems but no case constant and noTypeBaseentry. This addspath_casewith itscompute/simpequations,case_cong,case_eq,case_elim, acaseoverload socase p of stopped_at x => ... | pcons x r q => ...parses, and aTypeBaseregistration usingpath_bisimulationas the induction principle.llist,ltree,itree,itreeTau,lbtree,path) validates each entry through its case constant andTypeBase.constructors_of;pathcould not be registered without both. The selftest's model-finder table exercisespathinjectivity, distinctness and bisimulation.pathnow behaves like the other coalgebraic types undercasesyntax,EVALand the simplifier. The coalgebras selftest gains simp andcase-syntax checks and aTypeBaseregistration check.path_11stays local since its two conjuncts are already exported.src/parallel_builds/core/HolmakefileAdds
../../HolRefutetoINCLUDESunderPOLY, for every kernel. This is what pulls HolRefute intobin/build; no sequence file changes. HolRefute builds under--otknlas well as the standard kernel.AGENTS.md(new symlink toCLAUDE.md)Lets agent tooling that reads
AGENTS.mdpick up the existing project notes. No content.Manual/Description,help/DocfilesA new
Refutechapter and 16Refute.*docfiles.Testing
HOLSELFTESTLEVEL=2 Holmakeinsrc/HolRefuteis the quality gate: the selftest (level 2 adds cross-substrate conformance, the narrowing table, the corpus and the model-finder acceptance tables), thentheory_tests/. Model-finder rows needHOL4_KODKODIpointing at an unpackedkodkodi-1.5.7and a Java runtime; without it they report inconclusive and the theory scripts still build.Holmake examplesinsrc/HolRefutebuilds the example corpus.src/coalgebrasandsrc/portableML/poly/concurrentselftests cover the changes described above.