hol-checkins — Check-in messages from everything done in the HOL project.

[Hol-checkins] [HOL-Theorem-Prover/HOL] 4e7d15: first draft of tutorial

[Konrad S. <no...@gi...>]

  Branch: refs/heads/nfa-develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 4e7d15d35915e9dbacb6ee0b18fc93bdc83cd713
      https://github.com/HOL-Theorem-Prover/HOL/commit/4e7d15d35915e9dbacb6ee0b18fc93bdc83cd713
  Author: Konrad Slind <kon...@gm...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M examples/formal-languages/regular/automata-tutorial/src/README.md
    M examples/formal-languages/regular/automata-tutorial/src/Summary.md
    M examples/formal-languages/regular/automata-tutorial/src/definitions.md
    M examples/formal-languages/regular/automata-tutorial/src/dfa-to-nfa.md
    A examples/formal-languages/regular/automata-tutorial/src/exercises.md
    M examples/formal-languages/regular/automata-tutorial/src/final-result.md
    M examples/formal-languages/regular/automata-tutorial/src/nfa-to-dfa.md
    A examples/formal-languages/regular/automata-tutorial/to-view.txt
    M examples/formal-languages/regular/automata-tutorial/tutorialScript.sml

  Log Message:
  -----------
  first draft of tutorial



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 886bb6: Drop standalone system.pdf and drules.pdf targets

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 886bb66a4fd1fbec7be3d059b63f024f3186bd84
      https://github.com/HOL-Theorem-Prover/HOL/commit/886bb66a4fd1fbec7be3d059b63f024f3186bd84
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/Holmakefile

  Log Message:
  -----------
  Drop standalone system.pdf and drules.pdf targets

These were halfway-house experiments that built single-chapter PDFs
via .smd → .md → pandoc.  description.pdf (the bundled book PDF) is
the real deliverable, and it doesn't depend on these — it goes through
the .stex → polyscripter → .tex → latexmk path.

The associated .md targets (drules.md, system.md) are now unused too,
so drop them.  modern-syntax.md and suspension-resumption.md stay,
since they're consumed by modern-syntax-chapter.tex and
suspension-resumption-subsection.tex (both `\input` from
description.tex).

`Holmake` (default `all`) now builds:
  description.pdf

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 3d686fe650db0e6bef9f149ee8fe787f5d6e6d5e
      https://github.com/HOL-Theorem-Prover/HOL/commit/3d686fe650db0e6bef9f149ee8fe787f5d6e6d5e
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/system.smd

  Log Message:
  -----------
  Translate Theorem-keyword content in system.smd

stex §1773-1845 (the latter half of "Adding to the Current Theory")
covers the Theorem syntactic form, store_thm, and Triviality.  That
content was held inside the ##skip … ##endskip block as
partially-translated (markdown headings + raw-LaTeX bodies).  Replace
the partial version with a clean translation following the same
conventions used elsewhere in the file:

- \begin{alltt}…\end{alltt} → triple-backtick code blocks
- \mname / \mth / \mtac placeholders → italic *name* / *th* / *tac*
- \HOL{}/\ML{} → plain text "HOL"/"ML"
- store_thm's static type signature is replaced with a polyscripter
  printNameAndType call so we always show the live signature
- in-chapter cross-reference (Sections~\ref{sec:parsing}…) → markdown
  link [§Quotations, Parsing and Printing](#…)
- cross-chapter ref (Chapter~\ref{tactics-and-tacticals}) → prose
  only "the Tactics and Tacticals chapter"; will be promoted to a
  hyperlink once that chapter has its own .smd

The IMP_CLAUSE example has a parenthetical note acknowledging that
the example tactic is illustrative — closing the goal needs a little
more than `rpt strip_tac`.

\index{…} entries are kept in the source: smdpp strips them for the
mdbook output (which has full-text search instead of a printed
index), and pandoc passes them through to LaTeX intact.

The ##skip marker moves down to line 1296 (was 1233), now preceding
only the truly-untranslated remainder (Exporting a theory, ML
functions for accessing theories, Functions for creating definitional
extensions, etc.).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 5cfd6f8d9eaeee6a17f41c2d199c8c9679260a25
      https://github.com/HOL-Theorem-Prover/HOL/commit/5cfd6f8d9eaeee6a17f41c2d199c8c9679260a25
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/system.smd

  Log Message:
  -----------
  Translate "Exporting a theory" content in system.smd

stex §1846-1868 (the `Exporting a theory` paragraph that closes off
"ML functions for theory operations") was untranslated and held
inside the ##skip block.  Translate it following the conventions
used elsewhere:

- \HOL{}/\holmake{} → "HOL"/`Holmake`
- export_theory's static type signature → polyscripter
  printNameAndType call so we always show the live signature
- $name${\small{\tt Theory.sml}} → *name*`Theory.sml` (italic
  metavariable + monospace suffix)
- "in the current working directory" wording is dropped: it's true
  under Moscow ML but misleading under Poly/ML, where theory object
  files (...Theory.{sml,sig,dat}) live in `.hol/objs/`.  The location
  detail isn't load-bearing here, so the line just says where the
  files end up by name and not on disk.
- section~\ref{Holmake} → prose-only "see the section on `Holmake`"
  for now (cross-chapter; misc.tex hasn't been converted to .smd yet).
  Tracked in the same followup memory as the Tactics ref.

The ##skip marker advances past the new content.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 388a4dbcbc0ba38a5f29db4a71eaaefda16e6624
      https://github.com/HOL-Theorem-Prover/HOL/commit/388a4dbcbc0ba38a5f29db4a71eaaefda16e6624
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/system.smd

  Log Message:
  -----------
  Translate "ML functions for accessing theories" in system.smd

stex §1869-1949 covers the access-by-name functions (parents, types,
constants, axiom, definition, theorem, and their plurals).  This was
held in the ##skip block as partial-translation (markdown headings +
raw-LaTeX bodies).  Replace with a clean translation:

- \begin{holboxed}\begin{verbatim} blocks → polyscripter
  printNameAndType calls so signatures stay live
- \etc → "etc."
- \ml{"-"} / \ml{parents "-"} → backticked code
- \noindent dropped (markdown handles paragraph breaks)
- LaTeX % comment lines removed
- the stray `}` on the heading dropped

Two factual fixes the dynamic signatures surfaced:

- axiom, definition, theorem (and the *s plural variants) live in DB,
  not Theory.  The doc had them under Theory.  printNameAndType is
  now pointed at "DB"; mdbook renders the right structure.

- Theory.types returns (string * int) list (name-arity pairs), but
  the prose said "a list of arity-name pairs is returned".  Fixed
  the prose to "name-arity pairs" to match the live signature.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: c8328eb82805199893e0aa3df08b9f702935f732
      https://github.com/HOL-Theorem-Prover/HOL/commit/c8328eb82805199893e0aa3df08b9f702935f732
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Tools/smdpp.sml

  Log Message:
  -----------
  smdpp: also escape `_` and `*` inside math

Markdown's emphasis pass turns `_word_` and `*word*` into <em> tags,
which is fine for prose but breaks math: `$\mathsf{Terms}_{\Sigma_{\Omega}}$`
in source rendered with the inner underscore pair turned into <em>
tags, leaving MathJax with malformed math.

The existing math protection only doubled backslashes.  Extend it to
also prefix `_` and `*` with `\` so CommonMark's escape pass leaves a
literal underscore/asterisk for MathJax.

After this, $\mathsf{Terms}_{\Sigma_{\Omega}}$ et al. render correctly
in mdbook.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: a5eb02516caad1755f4448c1284e6f9e9ef0c9be
      https://github.com/HOL-Theorem-Prover/HOL/commit/a5eb02516caad1755f4448c1284e6f9e9ef0c9be
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/system.smd

  Log Message:
  -----------
  Translate "Functions for creating definitional extensions" intro and "Constant definitions" in system.smd

stex §1950-2014 covers the introduction to definitional extensions
and the first kind, "Constant definitions" with `new_definition`.
Replace the partial translation with a clean version:

- \begin{myenumerate}\item ... \end{myenumerate} → markdown numbered
  list (`1.`, `2.`, ...)
- \[ ... \] display math → $$ ... $$
- \LOGIC{} → §LOGIC (matching existing convention for cross-manual
  refs)
- \HOL{}/\ML{}/\ie/\dots → "HOL"/"ML"/"*i.e.*"/"$\dots$"
- \begin{holboxed}\begin{verbatim} → polyscripter
  printNameAndType call.  new_definition's canonical user-facing
  location is boolSyntax (Theory has it under nested
  Theory.Definition, which printNameAndType doesn't navigate).
- \holquote{$term$} → “$term$” (Unicode HOL term-quote pair) to
  match the convention used elsewhere in the file
- \lb\rb{} (LaTeX `\{\}` shortcut) → `\{\}` in math mode, rendering
  as `{}` for the empty hypothesis set
- \noindent dropped, % comment lines removed, \\ line breaks dropped
- the stray `}` on the heading dropped

The ##skip marker advances to just before "Constant specifications".

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: c3bedc91ca89a5d3f2c3fd2801fd284c947ccd9d
      https://github.com/HOL-Theorem-Prover/HOL/commit/c3bedc91ca89a5d3f2c3fd2801fd284c947ccd9d
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/system.smd

  Log Message:
  -----------
  Translate the remaining sections of system.smd

stex §2015-2358 covers:
  - Constant specifications (new_specification)
  - Type definitions (new_type_definition, TYPE_DEFINITION,
    *op*_TY_DEF naming)
  - Defining bijections (define_new_type_bijections)
  - Properties of type bijections (prove_rep_fn_one_one,
    prove_rep_fn_onto, prove_abs_fn_one_one, prove_abs_fn_onto)

This was the last of the partially-translated content held inside the
##skip ... ##endskip block.  All four sections are translated using
the conventions established earlier:

  - \begin{myenumerate}\item ... \end{myenumerate} → markdown lists
  - \[ ... \] display math → $$ ... $$
  - \begin{holboxed}\begin{verbatim}...\end{verbatim}\end{holboxed} →
    polyscripter printNameAndType calls (canonical structures:
    boolSyntax for new_specification / new_type_definition; Drule for
    define_new_type_bijections and the prove_*_fn_* helpers)
  - \begin{hol}\begin{alltt|verbatim}...\end → triple-backtick code
  - \LOGIC{} → §LOGIC
  - \HOL{}/\ML{} → "HOL"/"ML"
  - \m{abs}/\m{rep}/\m{P}/\m{th} (LaTeX local italic macros) → *abs*
    /*rep*/*P*/*th*
  - \ty{op} → italic *op* in prose, $\mathit{op}$ in math
  - \fun → \to (math), \turn → \vdash, \lquant{X}t → \forall X.\ t,
    \equant{X}t → \exists X.\ t
  - ${\sf X}_{\cal T}$ → $\mathsf{X}_{\mathcal{T}}$
  - \bs (LaTeX backslash-char macro) inside HOL term displays → \
  - \noindent / \medskip / % comments / \\ line breaks dropped
  - stray `}` on \subsubsection-derived headings dropped

The ##skip / ##endskip markers are removed entirely; system.smd is
now fully translated for the mdbook output.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: fc87ebbdc0c74c8a061ec1a3a5dc44640f9d3440
      https://github.com/HOL-Theorem-Prover/HOL/commit/fc87ebbdc0c74c8a061ec1a3a5dc44640f9d3440
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/Holmakefile
    M Manual/Description/desc-unicode.sty
    M Manual/Description/description.tex
    M Manual/Description/system.smd
    R Manual/Description/system.stex

  Log Message:
  -----------
  Make system.smd canonical; drop system.stex

system.smd is now fully translated, so retire system.stex and route
the description.pdf chapter through the same .smd → .md → pandoc path
that modern-syntax-chapter.tex uses:

  system.md: system.smd $(PS_STUFF)
        $(PS_NOUMAP)
  system.tex: system.md pdf-macros.lua
        (printf '\\chapter{...}\\label{HOLsyschapter}\n' ; \
         pandoc --top-level-division=chapter ... -t latex $<) > $@

The "# The HOL Logic in ML" H1 is removed from system.smd's body so
that pandoc's --top-level-division=chapter doesn't double-emit a
chapter heading on top of the printf-prepended one; smdpp picks the
chapter name up from SUMMARY.md and injects an H1 for the mdbook
output (matching modern-syntax.smd's pattern).

The pandoc fragment path needs a few macros that pandoc's standalone
template would otherwise provide:

  - \tightlist  (for tight markdown lists)
    Added a \providecommand to description.tex's preamble.

  - The Unicode chars ❲❳ ⟦⟧ ⇨ ⩋ now appear as literal UTF-8 bytes in
    the generated system.tex (previously polyscripter's umap converted
    them to LaTeX commands, but the .smd → pandoc path doesn't go
    through umap).  Added \DeclareUnicodeCharacter entries for U+2772,
    U+2773, U+27E6, U+27E7, U+21E8, U+214B in desc-unicode.sty,
    mapping them to the stix package's \lbrbrak / \rbrbrak /
    \llbracket / \rrbracket / \rightwhitearrow / \upand macros (stix
    is already loaded via layout.sty).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/fc759fbd7ed8...fc87ebbdc0c7

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] e5e605: Doc HTML: Contents TOC with full type info; redire...

[Michael N. <no...@gi...>]

  Branch: refs/heads/new-theorygraph
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: e5e60502a53d8ac10fe8ff3726dcf78faf799f34
      https://github.com/HOL-Theorem-Prover/HOL/commit/e5e60502a53d8ac10fe8ff3726dcf78faf799f34
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M help/src-sml/HOLPage.sml
    M help/src-sml/Htmlsigs.sml
    M src/parse/Parse.sml
    M src/postkernel/Theory.sig
    M src/postkernel/Theory.sml
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  Doc HTML: Contents TOC with full type info; redirect indexes

Per-theory HTML doc opens with a Contents block:
  - Type operators: each as "<opname> : <pretty-printed applied type>"
  - Constants: each as "<name> : <type>"
  - Axioms / Definitions / Theorems: linked names in a wrapping list
Empty categories show "(none)".  Subheadings use an accent bar to
stand out above the monospace listings.

print_doc_html now takes a {pp_thm, pp_type} record; Theory and Parse
expose Theory.pp_type the same way pp_thm is exposed.  Type-operator
arity is rendered by applying the operator to fresh α, β, … type
variables.

Reference-page navigation now points at the new docs:
  - help/index.html theory list links to <src>/.hol/docs/<thy>Theory.html
  - htmlsigs/TheoryIndex.html and idIndex.html theory entries link to
    <src>/.hol/docs/<thy>Theory.html#<entry>
The doc URL is computed by reading the sigobj symlink for the
relevant Theory.sig.  htmlsigs/<thy>Theory.html is no longer produced
(processSigfile skips Theory.sig inputs).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL]

[Michael N. <no...@gi...>]

  Branch: refs/heads/fix-arith-exclude-frags
  Home:   https://github.com/HOL-Theorem-Prover/HOL

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 458b7a: Fix Proof[exclude_frags = ...] for simp[] and stan...

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 458b7ad5fde1edd78afa1050057f1ec401438b4a
      https://github.com/HOL-Theorem-Prover/HOL/commit/458b7ad5fde1edd78afa1050057f1ec401438b4a
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/modern-syntax.smd
    M help/Docfiles/simpLib..KAL.md
    A help/Docfiles/simpLib.exclude_ssfrags.md
    A help/Docfiles/simpLib.force_add.md
    M help/Docfiles/simpLib.remove_ssfrags.md
    M src/basicProof/BasicProvers.sml
    A src/boss/theory_tests/exclArithBugScript.sml
    M src/simp/src/simpLib.sig
    M src/simp/src/simpLib.sml
    M tools/parsing/AttributeSyntax.sml
    M tools/parsing/HOLSourceExpand.sml
    M tools/parsing/HolParserOld.sml

  Log Message:
  -----------
  Fix Proof[exclude_frags = ...] for simp[] and standalone tactics

Two bugs in the same area:

1. Proof[exclude_frags = ARITH] numLib.ARITH_TAC raised
   Conv.UNCHANGED out of the proof body. Cause: with_simpset_updates
   eagerly called simpLib.remove_ssfrags on srw_ss(), which raises
   UNCHANGED when no fragment matches -- and the bare srw_ss() has
   no fragment named "ARITH" (the merged "ARITH" frag lives in
   boss_ss(), added by boss_augment).

2. Proof[exclude_frags = ARITH] simp[] would still apply ARITH:
   even after stripping ARITH_ss from srw_ss(), boss_augment
   unconditionally re-added it to boss_ss() via ++.

Solution: encode the exclusion in the simpset itself.

* simpset gains an "excluded : string Binaryset.set" field.
* ++ is a silent no-op when the incoming fragment's name is in
  the excluded set.
* New simpLib.exclude_ssfrags : string list -> simpset -> simpset
  removes matching frags from the history *and* records the
  names in "excluded". Never raises UNCHANGED. The implementation
  defensively filters against the union of old "excluded" and
  new names, with a comment stating the simpset invariant
  ("no ADDFRAG in history has a name in excluded") and why
  filtering against just the new names would also be sufficient
  if the invariant is preserved everywhere.
* New simpLib.force_add : simpset -> ssfrag -> simpset is the
  override: clears the name from "excluded" then ++s.
* process_tags routes SF-derived frags through force_add, so
  simp[SF FRAG_ss] still works as the user-facing override --
  for example, simp[SF ARITH_ss] inside Proof[exclude_frags = ARITH]
  re-enables ARITH for that simp call.
* The parser-side translators for exclude_frags = ... now
  emit simpLib.exclude_ssfrags. with_simpset_updates also gains
  a defensive "handle Conv.UNCHANGED" (covers other callers that
  may still pass remove_ssfrags-style functions).

Documentation:
* New docfiles for simpLib.exclude_ssfrags and simpLib.force_add.
* simpLib.remove_ssfrags docfile: corrected curried-arg-order in
  signature; example modernised to Poly/ML REPL style; added
  "Comparison with exclude_ssfrags" section.
* simpLib.++ docfile (simpLib..KAL.md): describes the new
  excluded-set behaviour.
* Manual/Description/modern-syntax.smd: the exclude_frags=
  attribute entry now describes the sticky semantics plus the
  SF override with a worked example.

Test (src/boss/theory_tests/exclArithBugScript.sml):
* Three Theorem blocks exercise the actual Theorem ... Proof[...]
  ... QED parser surface (including should_work, the original
  exception-leak regression).
* Three testutils assertions exercise the new semantics directly:
  - simp[] under exclude_frags = ARITH does not solve.
  - simp[SF ARITH_ss] under same does solve (override works).
  - SIMP_TAC (srw_ss() ++ ARITH_ss) [] (lazy in body) is
    blocked by the exclusion.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: fc759fbd7ed88fc3cf5468f0254f4aafed53e254
      https://github.com/HOL-Theorem-Prover/HOL/commit/fc759fbd7ed88fc3cf5468f0254f4aafed53e254
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/simplifier.stex

  Log Message:
  -----------
  Description manual: cover the new exclude-frags semantics

Three small additions in Manual/Description/simplifier.stex:

* The ssfrag construction section now notes that simpsets carry an
  excluded-fragment set and that ++ is a no-op when the incoming
  fragment is excluded; points readers at force_add / SF for overrides.

* The ExclSF paragraph distinguishes its per-call effect from the
  sticky Proof[exclude_frags = ...] attribute, and notes that SF
  is the in-call escape hatch when the latter is in force.

* The SF paragraph mentions its override role with respect to
  Proof[exclude_frags = ...].

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/0d967a8f0207...fc759fbd7ed8

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 0d967a: Document the three phases of the Poly/ML build

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 0d967a8f02075c33953043c3c98afad6e72f50ad
      https://github.com/HOL-Theorem-Prover/HOL/commit/0d967a8f02075c33953043c3c98afad6e72f50ad
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Developers/developers.md

  Log Message:
  -----------
  Document the three phases of the Poly/ML build

The Initial / Bare / Full progression (driven by phase_extras in
tools-poly/build.sml) was previously only described tangentially via
the hol.state and hol.state0 entries in the bin/ section. Add an
explicit subsection under "Build" so developers editing in early
directories know why a plain local Holmake either fails (when
bin/hol.state has not been built yet) or, worse, succeeds against the
wrong context.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 8abf09: Initial work on Böhm's (beta-)separation/separabil...

[Chun T. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 8abf09e0236868fb1315718505cda565b2e924ad
      https://github.com/HOL-Theorem-Prover/HOL/commit/8abf09e0236868fb1315718505cda565b2e924ad
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M examples/lambda/barendregt/boehmScript.sml
    M examples/lambda/barendregt/head_reductionLib.sig
    M examples/lambda/barendregt/head_reductionLib.sml
    M examples/lambda/barendregt/head_reductionScript.sml
    A examples/lambda/barendregt/separabilityScript.sml
    M examples/lambda/basics/basic_swapScript.sml
    M examples/lambda/basics/nomdatatype.sml
    M src/boss/bossLib.sig
    M src/list/src/listScript.sml
    M src/list/src/rich_listScript.sml
    M src/q/QLib.sig
    M src/q/QLib.sml

  Log Message:
  -----------
  Initial work on Böhm's (beta-)separation/separability thm


  Commit: a2ad2ba3f52c8cb2437011560fb6d51e5d0c8f6e
      https://github.com/HOL-Theorem-Prover/HOL/commit/a2ad2ba3f52c8cb2437011560fb6d51e5d0c8f6e
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M examples/lambda/barendregt/separabilityScript.sml
    M src/boss/hol4-base-unint.thy
    M src/list/src/rich_listScript.sml

  Log Message:
  -----------
  Fix otknl build

The proof of rich_listTheory.LAST_TAKE_EL involves iSUB of numeralTheory (for the first time of this theory), which wasn't imported by rich-list in src/boss/hol4-base-unint.thy. The theorem statement change is optional.


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/6fb4a01a5087...a2ad2ba3f52c

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 24d7da: List HolKernel.ui as prereq for Table-functor rule...

[Michael N. <no...@gi...>]

  Branch: refs/heads/table-sml-phase1
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 24d7dab504e41c88dfc854219a3b9745847ffa37
      https://github.com/HOL-Theorem-Prover/HOL/commit/24d7dab504e41c88dfc854219a3b9745847ffa37
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/1/Holmakefile
    M src/compute/src/Holmakefile
    M src/marker/Holmakefile
    M src/parse/Holmakefile

  Log Message:
  -----------
  List HolKernel.ui as prereq for Table-functor rules (issue #1595)

CI's badincludes selftest under HOLSELFTESTLEVEL `quse`s files like
TypeNet.sml from a fresh REPL state where only testutils' load
chain has run -- HolKernel itself isn't in scope.  Compile then
fails on `open HolKernel`, and downstream errors like
"Value or constructor (pair_compare) has not been declared"
follow.

Same fix-pattern as the previous sigobj-Tab and SharingTables-deps
commits: list the missing sigobj structures as explicit prereqs
so they end up in the .uo metadata and get auto-loaded before the
.sml is `quse`'d.

Adding $(dprot $(SIGOBJ)/HolKernel.ui) to:
  * src/parse/Holmakefile: LVTermNet.uo, TypeNet.uo,
    term_grammar.uo, parse_term.uo
  * src/1/Holmakefile: DefnBaseCore.uo, Ho_Net.uo
  * src/marker/Holmakefile: markerLib.uo
  * src/compute/src/Holmakefile: clauses.uo

LVTermNetFunctor.uo already had HolKernel.ui as prereq from the
develop tree; Termtab.uo / Typetab.uo / SharingTables.uo /
TheoryGraph.uo don't `open HolKernel` so don't need it added.

HolKernel.uo's metadata transitively pulls in Overlay, Lib, Term,
Type, Feedback, Globals, Portable, Thm, Uref -- so listing
HolKernel.ui covers all the kernel-structure references in one
go.

Verified locally with `bin/build cleanAll && bin/build -t
--seq=tools/sequences/upto-parallel` (which runs the badincludes
selftest); previous failure no longer reproduces.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] c8a42d: Refactor polyscripter into a callable library

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: c8a42d38731b648b50ee9ebe4fb631d9d564df24
      https://github.com/HOL-Theorem-Prover/HOL/commit/c8a42d38731b648b50ee9ebe4fb631d9d564df24
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/drules.smd
    M Manual/Description/suspension-resumption.smd
    M Manual/Description/system.smd
    M Manual/Tools/polyscripter.sml

  Log Message:
  -----------
  Refactor polyscripter into a callable library

Extract three top-level entry points so the module can be driven from
SML (e.g., from the smdpp mdbook preprocessor) as well as the existing
CLI:

  setupPolyscripter : unit -> obuf
    one-time initialisation; returns the compiler output buffer

  processStream : { input, output, debug, umap, obuf } -> unit
    drive a single .smd document through the line processor, writing
    output via the supplied callback

  processString : { input, debug, umap, obuf } -> string
    convenience wrapper that captures the output into a buffer

Also add a top-level ref `scriptPrint : (string -> unit) ref = ref print`
that user-script preambles can use in place of `TextIO.print` so their
output goes to the same stream as polyscripter's own emission.
processStream rebinds `scriptPrint` to its `output` callback for the
duration of the call, restoring on completion.  CLI behaviour is
unchanged because the callback is `print` in that path.

The three existing scripted-markdown chapters (system, drules,
suspension-resumption) are updated to use `!scriptPrint` in their
`printNameAndType0` definitions.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 6276369700fccc5fd0237962cf153402e03f368d
      https://github.com/HOL-Theorem-Prover/HOL/commit/6276369700fccc5fd0237962cf153402e03f368d
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Tools/.gitignore
    M Manual/Tools/Holmakefile
    A Manual/Tools/smdpp.sml

  Log Message:
  -----------
  Add smdpp mdbook preprocessor

smdpp reads the [Context, Book] JSON pair from stdin (mdbook's
preprocessor protocol), runs polyscripter on each chapter's content,
and writes the rewritten Book JSON to stdout.  One Poly/ML session
processes the whole book so theory loads amortise across chapters.

The transformations applied to each chapter's content are:

  - drop YAML frontmatter (pandoc-only, ignored by mdbook anyway)
  - run polyscripter on `>>` and `##` directives
  - strip `\index{...}` entries (mdbook search replaces a printed index)
  - drop pandoc raw-block fences like ```{=latex} ... ```
  - convert pandoc superscript syntax `^x^` (no whitespace inside) to
    `<sup>x</sup>` since pulldown-cmark doesn't support it
  - inside `$...$` and `$$...$$`, double every `\` so CommonMark's
    backslash-escape leaves the original backslash intact for MathJax
  - inject `# <chapter-title>` if the chapter source has no top-level
    H1 (e.g., modern-syntax.smd defers titling to its LaTeX wrapper)

A second pass over the book builds a `(slug -> chapter-file)` registry
from heading anchors and rewrites `[text](#anchor)` links so anchors
that live in a different chapter file get an explicit path prefix
(`[text](other.html#anchor)`).

A small JSON printer is included since the bundled JSON library only
parses.

Holmakefile gains a `smdpp` target that builds it via `buildheap` (same
mechanism as polyscripter; smdpp.sml is consumed alongside
polyscripter.sml so it can call into the library defs).  The
INCLUDES line picks up `$(HOLDIR)/src/bag` so the existing
`testoutput1` self-test (which loads `bagTheory`) can resolve its
dependency under build sequences that don't reach src/bag on their own.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: d5a657b1c83e04f0e424a681d9605681ae840d13
      https://github.com/HOL-Theorem-Prover/HOL/commit/d5a657b1c83e04f0e424a681d9605681ae840d13
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/.gitignore
    M Manual/Description/Holmakefile
    A Manual/Description/MDBOOK-README.md
    A Manual/Description/SUMMARY.md
    A Manual/Description/book.toml
    A Manual/Description/theme/index.hbs

  Log Message:
  -----------
  Wire up mdbook for Manual/Description

book.toml registers smdpp as the html-renderer preprocessor and sets
build-dir to ../book/Description (deliberately outside the source
directory so mdbook serve's watcher does not loop on its own output).

SUMMARY.md lists the three chapters that have already been translated
to scripted markdown: system, drules, and modern-syntax.

theme/index.hbs overrides mdbook's default page template to add a
MathJax tex2jax config script.  Two reasons:

  - the default mdbook config (TeX-AMS-MML_HTMLorMML) recognises
    only \(...\) and $$...$$ for math; our sources use $...$ for
    inline math, so we extend `inlineMath` to include $...$.

  - several LaTeX commands referenced from the sources come from the
    stmaryrd package (\llbracket, \rrbracket, \llparenthesis, etc.)
    and from custom \DeclareUnicodeCharacter mappings (\llbrace,
    \rrbrace, \rightwhitearrow, \upand, \lbrbrak, \rbrbrak).  These
    aren't in MathJax's default macro set, so we define them via
    `TeX.Macros` as `\unicode{xNNNN}` substitutions matching the LaTeX
    side.

Holmakefile gains `mdbook` and `mdbook-serve` phony targets, both
depending on `../Tools/smdpp` so the preprocessor binary is rebuilt
when needed.

MDBOOK-README.md (in the same directory) documents the build flow,
the smdpp passes, math/macros configuration, and known limitations.

Manual/.gitignore adds `book/` to keep mdbook output (which goes to
Manual/book/<bookname>/) out of git.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 7635705875be39c70d5e9928b70db537413e7506
      https://github.com/HOL-Theorem-Prover/HOL/commit/7635705875be39c70d5e9928b70db537413e7506
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/modern-syntax.smd
    M Manual/Description/system.smd

  Log Message:
  -----------
  Convert pandoc multi-line tables to GFM pipe tables

mdbook's CommonMark parser (pulldown-cmark) doesn't understand
pandoc's multi-line/simple table syntax — the dashed border lines get
parsed as `<hr>` and the rest as plain paragraphs.  GFM pipe tables
work in both pandoc and mdbook, so the source can stay shared.

Tables converted:

  system.smd
    - Non-aggregating Unicode characters
    - Building Types via Quotations or ML
    - Building Primitive Terms (also fixes a typo: `mk_const"x",t)`
      had a missing opening paren — the .stex source has `mk_const("x",t)`)
    - Syntactic abbreviations

  modern-syntax.smd
    - Script File Syntax (BNF productions)
    - Syntax for theorem proofs/definitions/etc. (BNF productions)
    - Attribute spec (BNF productions)
    - Keyword / (Commonly used) Possible attributes

Multi-line BNF cells (where one production spans several source lines)
are flattened with `<br>` separators since GFM pipe tables don't
permit literal newlines inside cells.  Pipe characters `|` inside
cells are escaped as `\|`.

The bare `\label{tab:script-file-syntax}` line that previously sat
below the Script File Syntax table is wrapped in a ```{=latex} fenced
block so it remains available for the LaTeX path's `\ref` machinery
but is stripped by smdpp for the mdbook output.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 8d7e7faf91dd2dfe66920d8336c00755ff214943
      https://github.com/HOL-Theorem-Prover/HOL/commit/8d7e7faf91dd2dfe66920d8336c00755ff214943
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/description.tex

  Log Message:
  -----------
  Add array and calc packages to description.tex

The pipe-table conversion in Manual/Description's chapters (commit
3c16d6032) led pandoc to emit calc-style column widths for tables
whose flattened cells exceeded its width-estimation threshold:

  \begin{longtable}[]{@{}
    >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}}
    ...

That syntax requires:
  - array, for the >{...}p{...} column prefix
  - calc, for \real{...} and the multiplicative dimension arithmetic

description.tex previously had longtable and booktabs but neither of
these.  Pandoc's standalone LaTeX template loads all four; because we
\input pandoc fragments rather than using the full template, we need
to supply array and calc in our own preamble.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 54a1fd08370b6d1e97700b768786252006eae0ed
      https://github.com/HOL-Theorem-Prover/HOL/commit/54a1fd08370b6d1e97700b768786252006eae0ed
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/MDBOOK-README.md

  Log Message:
  -----------
  Update MDBOOK-README to reflect tables and serve-port handling

Now that GFM pipe tables are the agreed source format and the LaTeX
preamble has the array+calc packages, tables are no longer a "known
limitation" — promote them to their own section explaining the
convention (line-break flattening with `<br>`, `\|` escaping for
embedded pipes, and the array+calc dependency for pandoc-emitted
proportional column widths).

Also document the recovery path for `Holmake mdbook-serve` failing
when port 3000 is already in use (`pkill -f 'mdbook serve'`, or
`lsof -i :3000` to identify the process).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 5de21d4a3d22653f7da53f43e4d88b86a805089a
      https://github.com/HOL-Theorem-Prover/HOL/commit/5de21d4a3d22653f7da53f43e4d88b86a805089a
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/Holmakefile
    M Manual/Description/MDBOOK-README.md

  Log Message:
  -----------
  Detach Holmake mdbook-serve and emit URL on stdout

The mdbook-serve recipe used to hold the foreground until the server
exited; closing the make process killed the server.  Now:

  - lsof pre-flight check fails fast if port 3000 is already in use,
    with a hint about how to stop the existing server
  - mdbook serve is started in a `(... &)` subshell so it detaches
    cleanly, and the recipe returns immediately
  - the URL (and stop hint, and log path if any) is printed to
    /dev/tty so it survives Holmake's stdout-capture, falling back
    to stderr when no tty is attached (CI, scripts piping)

Logging is opt-in via a make-style variable:

  Holmake mdbook-serve            # default; server output -> /dev/null
  Holmake mdbook-serve LOG=1      # output -> mdbook-serve.log here
  Holmake mdbook-serve LOG=path   # output -> path

mdbook-serve.log is added to EXTRA_CLEANS; *.log is already covered
by the top-level .gitignore.

MDBOOK-README updated to reflect the LOG flag and the new detached
behaviour.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: be7467896971b45fb9a8033305040412f02c3f57
      https://github.com/HOL-Theorem-Prover/HOL/commit/be7467896971b45fb9a8033305040412f02c3f57
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/Holmakefile

  Log Message:
  -----------
  Drop standalone pandoc HTML targets in Manual/Description

The `drules.html` and `system.html` targets generated single-file
pandoc HTML for each chapter into the source directory.  That worked
before mdbook entered the picture, but mdbook copies all files in its
source dir to the build dir as static assets — clobbering the chapter
HTML it just rendered with the pandoc standalone version, leaving
those chapters without sidebar/search/theme.

mdbook's per-chapter rendered HTML is strictly better than the pandoc
standalone (proper navigation, chrome, math config, cross-chapter
links), so retire the pandoc HTML pipeline entirely.  PDFs (system.pdf,
drules.pdf, description.pdf) are unaffected.

`Holmake` (default `all`) now builds:
  system.pdf drules.pdf description.pdf

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 6fb4a01a5087a2bba0542781523b3782a429487c
      https://github.com/HOL-Theorem-Prover/HOL/commit/6fb4a01a5087a2bba0542781523b3782a429487c
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M Manual/Description/modern-syntax.smd
    M Manual/Description/system.smd

  Log Message:
  -----------
  Use proportional alignment-row dashes for pipe tables

Pandoc reads the dash widths in a pipe table's alignment row as
relative column-width hints when emitting LaTeX longtable column
specs.  My initial conversions used `|---|---|---|` for every table,
which gave each column an equal 1/3 share — and for the BNF tables in
modern-syntax.smd (whose middle column is just `::=`) that meant the
Production column got squeezed into one third of the page.

Adjust the alignment rows to roughly match content widths:

  modern-syntax.smd, BNF tables (3): 21% / 11% / 68% (::= centred)
  system.smd, Building Types/Primitive Terms: 22% / 30% / 48%
  system.smd, Syntactic abbreviations: 17% / 46% / 37%

The Non-aggregating Unicode characters table in system.smd already
had proportional dashes from the original conversion and is left
alone.

mdbook/HTML rendering ignores these widths (the browser does its own
auto-sizing of pipe-tables), so this change is LaTeX-only in effect.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/e009b7b09ed8...6fb4a01a5087

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] b87023: Ignore generated help/theorygraph/thypaths.txt

[Michael N. <no...@gi...>]

  Branch: refs/heads/new-theorygraph
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: b87023e570e24434b41add3ed1dc38357895ed1a
      https://github.com/HOL-Theorem-Prover/HOL/commit/b87023e570e24434b41add3ed1dc38357895ed1a
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M .gitignore

  Log Message:
  -----------
  Ignore generated help/theorygraph/thypaths.txt



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] e4b59d: Generate per-theory HTML docs and rebuild theorygr...

[Michael N. <no...@gi...>]

  Branch: refs/heads/new-theorygraph
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: e4b59dba4c152add223365f28cd2d135b720b01c
      https://github.com/HOL-Theorem-Prover/HOL/commit/e4b59dba4c152add223365f28cd2d135b720b01c
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-04 (Mon, 04 May 2026)

  Changed paths:
    M .gitignore
    R help/src-sml/DOT
    M src/portableML/rawtheory/theorytool.ML
    M src/postkernel/Theory.sml
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml
    M tools/build/buildutils.sml

  Log Message:
  -----------
  Generate per-theory HTML docs and rebuild theorygraph via theorytool

- Replace the comment-style docs in *Theory.sig with a styled HTML page
  emitted to <src>/.hol/docs/<thy>Theory.html on every theory export
  (TheoryPP.print_doc_html writes directly to a TextIO.outstream).
- Compute parent links using each parent's recorded metadata path so
  the URL resolves across .hol/docs directories in different sources.
- Rewrite write_theory_graph to use src/portableML/rawtheory/theorytool
  with a new --url-base=DIR option that emits per-node URLs as relative
  paths to the source-dir docs.  Filter to production theories by
  passing the sigobj theory list as positional args, dropping test-only
  theories from the graph.  Delete the old DOT script.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: b9978c634d68e4852be7937706ba746499c17a54
      https://github.com/HOL-Theorem-Prover/HOL/commit/b9978c634d68e4852be7937706ba746499c17a54
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  Link printed theorem names to their source location

print_doc_html now uses each theorem's recorded thm_src_location to
emit an <a class="src-link"> wrapping the theorem name; the URL is the
relative path from <src>/.hol/docs/ to the originating <thy>Script.sml
with a #L<linenum> fragment.  Theorems with no location info still
render as plain text.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 832fc9424ac8128ca32b37d9cc000929a5005d13
      https://github.com/HOL-Theorem-Prover/HOL/commit/832fc9424ac8128ca32b37d9cc000929a5005d13
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/postkernel/Theory.sml
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml
    M tools/parsing/HOLSourceExpand.sml
    M tools/parsing/HolParserOld.sml

  Log Message:
  -----------
  Mirror each Script.sml as a line-anchored HTML next to its theory doc

- TheoryPP.write_script_html copies a Script.sml into HTML, wrapping
  each line in a <span id="Lnnn"> with a visible line-number gutter, so
  source-link URLs of the form "<thy>Script.html#Lnnn" land on the
  right line in any browser without depending on browser-specific
  features like scroll-to-text.
- print_doc_html's source URLs now point at the mirrored
  "<thy>Script.html" rather than the raw .sml.
- Theory.export_theory writes the script mirror alongside the existing
  theory HTML doc, gated on the same option that controls doc emission.
- Rename the controlling trace from TheoryPP.include_docs to
  TheoryPP.include_html_docs to better reflect what it now does;
  HOLSourceExpand and HolParserOld emit the new name when expanding
  Theory[no_sig_docs].  The user-facing attribute keeps its existing
  spelling for back-compat.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: efdb22fbf979513e437f2512ff504203610a8932
      https://github.com/HOL-Theorem-Prover/HOL/commit/efdb22fbf979513e437f2512ff504203610a8932
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/portableML/rawtheory/theorystats.sig
    M src/portableML/rawtheory/theorystats.sml
    M src/portableML/rawtheory/theorytool.ML
    M tools/build/buildutils.sml

  Log Message:
  -----------
  theorytool: --paths-from option to load an explicit *Theory.dat list

Adds a --paths-from=<file> option to theorytool that skips the file
tree scan entirely and instead reads a list of <thy>Theory.dat paths
(one per line) from the given file, loads each via readThy, and
proceeds.  Avoids the "duplicate theory" failure when the same theory
name occurs in more than one location (e.g., a development version in
src/ and an unrelated copy under examples/).

In write_theory_graph, materialise the list by walking sigobj/ for
*Theory.sig symlinks and writing the corresponding canonical .dat
paths (with the .hol/objs/ component stripped, since HFS_NameMunge
re-adds it on access) into help/theorygraph/thypaths.txt before
invoking theorytool with --paths-from.  Drops the older
list_sigobj_theories helper that passed names positionally.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 19f11bf3d83c4072aca05451507cfcc7f4366dc3
      https://github.com/HOL-Theorem-Prover/HOL/commit/19f11bf3d83c4072aca05451507cfcc7f4366dc3
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  HTML doc: visible source-link affordance via name + code icon

Drop the GitHub-style "#" permalink (uninteresting for local files)
and make the theorem name itself a visible source link: accent
colour, no underline, hover underlined, with a small inline </> SVG
icon trailing the name (both wrapped in one <a> so the whole click
target is the link).  The wrapping div retains its id, so deep links
still resolve when needed via address-bar copy.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 95700f587380d6d6f0f91e5f2951b508a6422d1e
      https://github.com/HOL-Theorem-Prover/HOL/commit/95700f587380d6d6f0f91e5f2951b508a6422d1e
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  HTML doc: use Octicons file-code-16 for the source-link affordance

The previous icon was Octicons' code-16 (just "<>"), which doesn't
make the "this links to a source file" semantic obvious.  Switch to
file-code-16 (a document outline with </> inside) — it keeps the code
cue but adds the document/file framing, so the link target reads more
naturally as "open the source script".

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/e4b59dba4c15%5E...95700f587380

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 118674: Improve Holmake parallel-build failure reporting (...

[Michael N. <no...@gi...>]

  Branch: refs/heads/fix-issue1903
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 118674ae1746892ff0e041ae0f259d1c7dd83005
      https://github.com/HOL-Theorem-Prover/HOL/commit/118674ae1746892ff0e041ae0f259d1c7dd83005
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M tools/Holmake/poly/MB_Monitor.sig
    M tools/Holmake/poly/MB_Monitor.sml
    M tools/Holmake/poly/multibuild.sml
    A tools/Holmake/tests/issue1903/Holmakefile
    A tools/Holmake/tests/issue1903/selftest.sml
    A tools/Holmake/tests/issue1903/testdir/Holmakefile
    A tools/Holmake/tests/issue1903/testdir/badboyScript.sml
    A tools/Holmake/tests/issue1903/testdir/slowAScript.sml
    A tools/Holmake/tests/issue1903/testdir/slowBScript.sml
    A tools/Holmake/tests/issue1903/testdir/slowCScript.sml
    M tools/Holmake/tests/parallel_tests/Holmakefile

  Log Message:
  -----------
  Improve Holmake parallel-build failure reporting (#1903)

When `-j N` Holmake aborts because of a failed job, every job that
was killed mid-flight printed a loud red `MKILLED` line *after* the
real failure — burying the actual error under collateral notices.

Tone the kills down (dim "killed" verdict instead) and defer each
failure's tail-of-output + "Full log:" path to a single closing
`*** Holmake aborted - N target(s) failed:` block, so the last lines
on screen now point at the real cause. Under `--keep-going` the
verbose per-failure block still appears inline at the moment of
failure (so live builds still surface the error promptly) and is
*also* repeated in the final summary.

Adds a regression test at `tools/Holmake/tests/issue1903/` that
spins up a parallel sub-Holmake with three slow `Theory[bare]`
scripts plus a deliberately-failing one, and verifies in both
default and `-k` modes that the captured output has the expected
shape.

Closes #1903

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 1354b4: List sigobj Tab deps for remaining Table-functor r...

[Michael N. <no...@gi...>]

  Branch: refs/heads/table-sml-phase1
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 1354b4e049b0e695f156ee445eabb909aec532c4
      https://github.com/HOL-Theorem-Prover/HOL/commit/1354b4e049b0e695f156ee445eabb909aec532c4
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/1/Holmakefile
    M src/marker/Holmakefile
    M src/parse/Holmakefile

  Log Message:
  -----------
  List sigobj Tab deps for remaining Table-functor rules (issue #1595)

CI's `tools/Holmake/tests/badincludes` selftest runs `quse` on
TypeNet.sml, which requires Typetab to be loaded; it isn't unless
TypeNet.uo's metadata includes a Typetab dep.  Same root cause as
the SharingTables/TheoryGraph fix in 7acb21a85: poly_compile
parses the explicit recipe's args for `-I` paths and hands those
to Holdep -- since my recipes don't have `-I`, Holdep with empty
includes returns nothing, so any sigobj-resident structures the
file references are missing from the .uo metadata.

Same per-file fix as before: list the sigobj Tab .ui as an
explicit prereq in the rule.

* src/parse/Holmakefile
  * TypeNet.uo:    + Typetab.ui
  * term_grammar.uo: + Symtab.ui
  * parse_term.uo:   + Symtab.ui
* src/1/Holmakefile
  * DefnBaseCore.uo: + KNametab.ui
* src/marker/Holmakefile
  * markerLib.uo:    + KNametab.ui

LVTermNet.uo, LVTermNetFunctor.uo, Ho_Net.uo, clauses.uo don't
reference sigobj Tabs and stay as-is.

Verified by inspecting TypeNet.uo metadata after a local
`bin/build cleanAll && bin/build -F`: the dep list now contains
`$(HOLDIR)/sigobj/Typetab`.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 7acb21: List sigobj deps for SharingTables.uo and TheoryGr...

[Michael N. <no...@gi...>]

  Branch: refs/heads/table-sml-phase1
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 7acb21a8581ccad2a10237ce40ef01601340dc68
      https://github.com/HOL-Theorem-Prover/HOL/commit/7acb21a8581ccad2a10237ce40ef01601340dc68
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/postkernel/Holmakefile

  Log Message:
  -----------
  List sigobj deps for SharingTables.uo and TheoryGraph.uo (issue #1595)

CI's poly Docker fresh-build failed compiling SharingTables.sml with
"Structure (RawTheoryReader) has not been declared".  Cause:
poly_compile parses the explicit recipe's args for `-I` paths and
hands those to Holdep as the only include-path search list.  My
recipe was `$(HOLMOSMLC) Overlay.ui Table.ui -c $<` -- no `-I`,
so Holdep with empty includes returned nothing, the .uo metadata
omitted the auto-detected deps, and poly's runtime loader reached
SharingTables before RawTheoryReader was in scope.

Pre-existing Termtab/Typetab rules avoid the bug because their
.sml files only open Term/HOLPP, which the parent load chain
already brings in by the time those structures are needed.
SharingTables/TheoryGraph have wider footprints, including
RawTheoryReader (in src/portableML/rawtheory) that the parent
chain doesn't pre-load.

Fix is to list the deps explicitly in the rule's prereqs so they
land in the .uo metadata regardless of Holdep's search.  This
mirrors the pattern already in src/parse/Holmakefile for
parse_term/term_grammar.

* SharingTables.uo: + sibling DB_dtype.uo, sigobj Term.ui /
  Type.ui / RawTheoryReader.ui.
* TheoryGraph.uo: + sibling Theory.uo, sigobj Portable.ui.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] e009b7: Give clearer error from UNABBREV_TAC for missing a...

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: e009b7b09ed8eb5646878b929f051b965abf7c78
      https://github.com/HOL-Theorem-Prover/HOL/commit/e009b7b09ed8eb5646878b929f051b965abf7c78
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/marker/markerLib.sml
    M src/marker/selftest.sml

  Log Message:
  -----------
  Give clearer error from UNABBREV_TAC for missing abbrev

Previously, UNABBREV_TAC "x" (and so fs[Abbr `x`] and friends) delegated
to FIRST_X_ASSUM to find the matching Abbrev (x = ...) assumption, and
when no such assumption existed the failure surfaced as a bare
HOL_ERR{origin_function = "FIRST_ASSUM", message = ""}. That gave the
user no clue that the actual problem was a typo in (or otherwise stale
reference to) an abbreviation name.

Catch the FIRST_X_ASSUM failure and re-raise a UNABBREV_TAC-tagged
error naming the missing abbreviation; the matching-abbrev path is
unchanged.

Closes #1483

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL]

[Michael N. <no...@gi...>]

  Branch: refs/heads/fix-empty-Abbr-error
  Home:   https://github.com/HOL-Theorem-Prover/HOL

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL]

[Michael N. <no...@gi...>]

  Branch: refs/heads/fix-issue-1086
  Home:   https://github.com/HOL-Theorem-Prover/HOL

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 21ecab: Stop case-printer's strip_case orphaning bound var...

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 21ecab858b3590457299884309eb83e1b7490f92
      https://github.com/HOL-Theorem-Prover/HOL/commit/21ecab858b3590457299884309eb83e1b7490f92
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/1/Pmatch.sml
    M src/datatype/selftest.sml

  Log Message:
  -----------
  Stop case-printer's strip_case orphaning bound variables

Pmatch.strip_case (used by the case-expression pretty-printer via
TypeBase) flattens a nested case where the outer pattern binds a
variable v and the inner case scrutinises `v = e` for some closed e.
The merge substitutes [v |-> e] into the *first* (true-branch) pattern
so that the two clauses can be inlined into the outer case. The check
guarding the merge required v to be a variable, fvs to be patvars, and
e to be closed, but it didn't require v to be absent from the
true-branch rhs.

For

    case x of MCons y ys => if y = T then y else F | MNil => F

dest produced clauses (MCons T ys, y) and (MCons y ys, F) — the y in
the first rhs was the outer-pattern's y, but after the substitution
that rhs's binder is gone, so y is left orphaned. The closed term
printed as

    \x. case x of MNil => F | MCons T ys => y | MCons y ys => F

which doesn't round-trip through the parser (the printed `y` reads as
a free variable). Issue #1086.

Re-enable the safety check that was already commented out at the merge
site (with the right helper name): require v not to occur free in the
rhs being paired with the substituted pattern. When the check fails,
strip_case keeps the inner case visible rather than producing a
broken merge. The non-eq branch right below already does the analogous
check via tm_null_intersection over free_varsl rhsides; this commit
just reinstates it for the eq branch.

Regression test in src/datatype/selftest.sml asserts that the example
above prints to a string that re-parses to an alpha-equivalent term.

Closes #1086

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] ba02bd: Initial draft of allowing loading theorems via replay

[Michael N. <no...@gi...>]

  Branch: refs/heads/master
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: ba02bdd1e85f06f74cab27660e306d3e2d55b287
      https://github.com/HOL-Theorem-Prover/HOL/commit/ba02bdd1e85f06f74cab27660e306d3e2d55b287
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M src/postkernel/TheoryReader.sig
    M src/postkernel/TheoryReader.sml
    M src/postkernel/ThyDataSexp.sig
    M src/postkernel/ThyDataSexp.sml
    M src/postkernel/prooftrace/Holmakefile
    A src/postkernel/prooftrace/ThmSrc_tr.sig
    A src/postkernel/prooftrace/ThmSrc_tr.sml
    M tools-poly/hol.ML
    M tools/Holmake/core/HM_Core_Cline.sig
    M tools/Holmake/core/HM_Core_Cline.sml
    M tools/Holmake/poly/BuildCommand.sml
    M tools/build/build.sml
    M tools/build/buildcline.sml
    M tools/build/buildcline_dtype.sml
    M tools/build/buildutils.sml
    M tools/sequences/kernel
    M tools/util/FunctionalRecordUpdate.sml

  Log Message:
  -----------
  Initial draft of allowing loading theorems via replay

This adds a `--thmsrc` flag to `bin/build`, `Holmake`, and `bin/hol` that
controls where theorem data comes from when loading theories:

- `dat` (default): theorems are read from `.dat` files via `Thm.disk_thm`
  (current behavior, no change)
- `tr`: theorems are replayed from `.tr.gz` proof trace files via
  `ProofTraceReplay`, with metadata (parents, thydata, thminfo) still
  read from `.dat` files

Flag propagation chain:

```
bin/build --thmsrc=tr
  → Holmake --thmsrc=tr              (forwarded via extra_args in build.sml)
    → hol run --thmsrc=tr ...        (forwarded in BuildCommand.sml run_script)
      → Meta.load "ThmSrc_tr"        (loaded in hol.ML before theory loading)
        → TheoryReader.load_thydata_fn := ThmSrc_tr.load_thydata
        → ThyDataSexp.anon_thm_lookup := <replayed anon thm lookup>
          → *Theory.uo calls TheoryReader.load_thydata → dispatches to replay
          → thydata processing uses replayed anon thms instead of disk_thms
```

Two hook points:

1. `TheoryReader.load_thydata_fn` (named theorems)
A ref defaulting to `load_thydata_from_dat`. When `--thmsrc=tr`, `ThmSrc_tr`
replaces it with a function that calls `ProofTraceReplay.replay` for theorems
and reads `.dat` only for metadata (parents, types/consts, thydata, thminfo).

2. `ThyDataSexp.anon_thm_lookup` (thydata-embedded theorems)
Thydata s-expressions can contain `tag-th` entries — anonymous theorems
used by simp sets, grammar updates, etc. Normally these are reconstructed
via `Thm.disk_thm`. The `anon_thm_lookup` ref allows the replay loader
to intercept these with `(thy, anon_id) → replayed_thm` lookups, so that
even thydata-embedded theorems are replayed rather than asserted from disk.

Design notes:

Why types/consts don't need `incorporate`:
When replaying, definition primitives (`prim_type_definition`,
`gen_prim_specification`, etc.) register types and constants in the
kernel as a side effect. Calling `incorporate_types`/`incorporate_consts`
afterward would retire the kernel IDs created by replay, breaking
uptodate checks on replayed theorems.

Named theorems:
`ThmSrc_tr.load_thydata` calls `ProofTraceReplay.replay thyname` which
builds all theorems via kernel inferences. The named theorems are matched
with `thminfo` (class, private) from the `.dat` file's raw_thm records,
then registered via `DB.bindl`. The returned `Symtab.table` is used by
the generated `*Theory.sml` code (`TDB.find`) to bind SML identifiers.

Anonymous / thydata-embedded theorems:
Thydata s-expressions may embed theorems via `tag-th`. During export,
`ThyDataSexp.thmwrite` assigns each such theorem an anonymous id via
`Theory.add_anonymous_thm`. During loading, `ThyDataSexp.thmreader`
would normally call `Thm.disk_thm (thy, SavedAnon id)` to reconstruct
these. With the `anon_thm_lookup` hook, the replay loader intercepts
this: it looks up `(thy, id)` via `ProofTraceReplay.replayed_thms` and
returns the replayed theorem instead. This is set once at init time
and works across all theories.

Thydata processing:
The `.dat` file is still parsed for thydata (simp sets, grammar updates,
etc.). The string, type, and term vectors are built from the sharing
tables (needed because thydata s-expressions contain `tag-tm`, `tag-ty`,
`tag-str`, and `tag-knm` entries that reference them). No `dec_sdata`
call and no `disk_thm` theorem construction.

Extensibility:
Adding a new theorem source (e.g., `pft`) requires:
1. A new loader module (like `ThmSrc_tr`) that sets both refs
2. Adding the value to `--thmsrc` validation in the three cline parsers
3. Adding a case in `hol.ML` to load the init module


  Commit: 79e7423de3dd2bba35a91d25a1f69bd1b9ca69e1
      https://github.com/HOL-Theorem-Prover/HOL/commit/79e7423de3dd2bba35a91d25a1f69bd1b9ca69e1
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M src/postkernel/prooftrace/ThmSrc_tr.sml

  Log Message:
  -----------
  Use HOLFS for finding .tr.gz sources


  Commit: a70af957e5e2527a13511c679ca506ef261f0840
      https://github.com/HOL-Theorem-Prover/HOL/commit/a70af957e5e2527a13511c679ca506ef261f0840
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M tools-poly/hol.ML

  Log Message:
  -----------
  Support explicit --thmsrc=dat


  Commit: b81caf38ab7f8420a7dacece321fb76b14dd3284
      https://github.com/HOL-Theorem-Prover/HOL/commit/b81caf38ab7f8420a7dacece321fb76b14dd3284
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M tools-poly/hol.ML
    M tools/Holmake/poly/BuildCommand.sml
    M tools/Holmake/poly/multibuild.sml

  Log Message:
  -----------
  Use environment variable for internal thmsrc propagation


  Commit: 01c933ccc81ac040516e270aaff058dfefbb931f
      https://github.com/HOL-Theorem-Prover/HOL/commit/01c933ccc81ac040516e270aaff058dfefbb931f
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M tools-poly/build.sml

  Log Message:
  -----------
  Fix thmsrc in tools-poly/build.sml too


  Commit: e7cfc6349ace67e908d885939014b663c77a0a03
      https://github.com/HOL-Theorem-Prover/HOL/commit/e7cfc6349ace67e908d885939014b663c77a0a03
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M src/postkernel/Theory.sig
    M src/postkernel/Theory.sml
    M src/postkernel/prooftrace/ThmSrc_tr.sml

  Log Message:
  -----------
  Register replayed axioms for uptodate checks


  Commit: 1ff358b2e7cf446bd1d1ce419c7ebba85fe8007f
      https://github.com/HOL-Theorem-Prover/HOL/commit/1ff358b2e7cf446bd1d1ce419c7ebba85fe8007f
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M src/postkernel/prooftrace/ProofTraceReplay.sig
    M src/postkernel/prooftrace/ProofTraceReplay.sml
    M src/postkernel/prooftrace/ThmSrc_tr.sml

  Log Message:
  -----------
  Make ProofTraceReplay take full paths

And use this in ThmSrc_tr to avoid chDir


  Commit: c7c049c388cd2d5d4d736fb3632feb1a2310dc87
      https://github.com/HOL-Theorem-Prover/HOL/commit/c7c049c388cd2d5d4d736fb3632feb1a2310dc87
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    R src/postkernel/prooftrace/HOLsexp-dummy.sml
    A src/postkernel/prooftrace/mlton/HOLsexp-dummy.sml
    M src/postkernel/prooftrace/replay.mlb

  Log Message:
  -----------
  Move HOLsexp-dummy.sml to mlton-specific dir


  Commit: c5de082e7500b3ed4d448d30e2bd400bc5e0e7d6
      https://github.com/HOL-Theorem-Prover/HOL/commit/c5de082e7500b3ed4d448d30e2bd400bc5e0e7d6
  Author: Daniel Nezamabadi <555...@us...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M src/postkernel/prooftrace/Holmakefile

  Log Message:
  -----------
  Don't build prooftrace on systems without Word64

Assisted-by: Claude:claude-opus-4-6


  Commit: 9356dcf6a2eeaeadef7cea08417fe93aaf01ecf9
      https://github.com/HOL-Theorem-Prover/HOL/commit/9356dcf6a2eeaeadef7cea08417fe93aaf01ecf9
  Author: Daniel Nezamabadi <555...@us...>
  Date:   2026-04-14 (Tue, 14 Apr 2026)

  Changed paths:
    M tools-poly/hol.ML
    M tools/Holmake/core/HM_Core_Cline.sml

  Log Message:
  -----------
  Handle --thmsrc tr more gracefully on systems without Word64

Assisted-by: Claude:claude-opus-4-6


  Commit: 7ea54e7afe7fb3e5f03a2cb13bc80e5c1c32ed67
      https://github.com/HOL-Theorem-Prover/HOL/commit/7ea54e7afe7fb3e5f03a2cb13bc80e5c1c32ed67
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-15 (Wed, 15 Apr 2026)

  Changed paths:
    M examples/latex-generation/paper/paper.htex

  Log Message:
  -----------
  Correct error in latex-generation's write-up (s/horizontal/vertical)


  Commit: fe05d1b1e8c711d06047349ec24dcd14df3ee131
      https://github.com/HOL-Theorem-Prover/HOL/commit/fe05d1b1e8c711d06047349ec24dcd14df3ee131
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-04-18 (Sat, 18 Apr 2026)

  Changed paths:
    M examples/CCS/CCSScript.sml
    M examples/formal-languages/pi-calculus/pi_agentScript.sml
    M examples/lambda/barendregt/labelledTermsScript.sml
    M examples/lambda/basics/ctermScript.sml
    M examples/lambda/basics/nomdatatype.sig
    M examples/lambda/basics/nomdatatype.sml
    M examples/lambda/basics/termScript.sml

  Log Message:
  -----------
  The "nominal_datatype" API (preliminary work)


  Commit: 915a1f4d70524ea00e210d5a17007dc04d54f64d
      https://github.com/HOL-Theorem-Prover/HOL/commit/915a1f4d70524ea00e210d5a17007dc04d54f64d
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-04-18 (Sat, 18 Apr 2026)

  Changed paths:
    M examples/lambda/basics/nomdatatype.sml

  Log Message:
  -----------
  Fix build_tns for possibly multiple elements in uns


  Commit: 73d699ef8aac474281efa79cdc04f8d8b1c0b437
      https://github.com/HOL-Theorem-Prover/HOL/commit/73d699ef8aac474281efa79cdc04f8d8b1c0b437
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    A tools/Holmake/core/HM_DirLock.sig
    A tools/Holmake/core/HM_DirLock.sml
    M tools/Holmake/core/HM_GraphBuildJ1.sml
    M tools/Holmake/mlton/Holmake.mlb
    M tools/Holmake/poly/multibuild.sml
    M tools/Holmake/poly/poly-Holmake.ML
    A tools/Holmake/tests/dirlock/Holmakefile
    A tools/Holmake/tests/dirlock/dirA/Holmakefile
    A tools/Holmake/tests/dirlock/dirA/dirAScript.sml
    A tools/Holmake/tests/dirlock/dirB/Holmakefile
    A tools/Holmake/tests/dirlock/dirB/dirBScript.sml
    A tools/Holmake/tests/dirlock/selftest.sml
    A tools/Holmake/tests/dirlock/shared/sharedScript.sml

  Log Message:
  -----------
  Holmake: add per-directory locking for concurrent safety (#1826)

When two separate Holmake processes build in directories that share a
common dependency, both may try to rebuild the shared directory
simultaneously, leading to race conditions and build failures.

Fix this by acquiring a POSIX fcntl advisory lock on a per-directory
lockfile (.hol/holmake.lock) before building targets in that directory.
If another Holmake process is already building there, the second process
blocks until the first finishes, then re-checks timestamps and skips
targets that are already up-to-date.

The locking is added to both build paths:
- HM_GraphBuildJ1 (jobs=1): tracks the currently locked directory and
  acquires/releases on directory transitions.
- multibuild (jobs>1): uses a refcount-based lock map since multiple
  jobs from different directories may be active concurrently.

On non-Unix systems or if locking fails (e.g., unsupported filesystem),
Holmake warns and proceeds without locking, preserving the previous
behaviour.


  Commit: 6d7c29bddce557dfff26c535b5b940736e0555c1
      https://github.com/HOL-Theorem-Prover/HOL/commit/6d7c29bddce557dfff26c535b5b940736e0555c1
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    A tools/Holmake/core/HM_BuildLock.sig
    A tools/Holmake/core/HM_BuildLock.sml
    R tools/Holmake/core/HM_DirLock.sig
    R tools/Holmake/core/HM_DirLock.sml
    M tools/Holmake/core/HM_GraphBuildJ1.sml
    M tools/Holmake/mlton/Holmake.mlb
    M tools/Holmake/poly/multibuild.sml
    M tools/Holmake/poly/poly-Holmake.ML
    M tools/Holmake/tests/dirlock/selftest.sml

  Log Message:
  -----------
  Rework to per-file rather than per-directory locks


  Commit: 7223a01aaf323a01f037bcd51bc72da82a1f37e3
      https://github.com/HOL-Theorem-Prover/HOL/commit/7223a01aaf323a01f037bcd51bc72da82a1f37e3
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    A tools/Holmake/mosml/HM_BuildLock.sml
    M tools/configure.sml

  Log Message:
  -----------
  Add dummy implementation for mosml


  Commit: 5cb4a8d79a4483180bc574549d38426efaa27784
      https://github.com/HOL-Theorem-Prover/HOL/commit/5cb4a8d79a4483180bc574549d38426efaa27784
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M tools/Holmake/hfs/HOLFS_dtype.sml

  Log Message:
  -----------
  Fix concurrent directory creation race

createDirIfNecessary: handle the race where two concurrent Holmake
processes both try to create the same directory (e.g., .hol/objs).
Previously, the second process would crash with EEXIST. Now catch
OS.SysErr on mkDir and re-check whether the path is already a
directory, only failing if it isn't.


  Commit: 43fe97ddfdcf6127e49a13136ed942c9841b51c9
      https://github.com/HOL-Theorem-Prover/HOL/commit/43fe97ddfdcf6127e49a13136ed942c9841b51c9
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M tools/Holmake/tests/parallel_tests/Holmakefile

  Log Message:
  -----------
  Add dirlock to selftest suite

Add dirlock test to parallel_tests so it runs automatically during
selftest builds (bin/build -t).


  Commit: a4dc9ce48d1173f6929df24fc8868b559b3a1caf
      https://github.com/HOL-Theorem-Prover/HOL/commit/a4dc9ce48d1173f6929df24fc8868b559b3a1caf
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M tools/Holmake/tests/dirlock/dirA/Holmakefile
    M tools/Holmake/tests/dirlock/dirB/Holmakefile
    A tools/Holmake/tests/dirlock/shared/Holmakefile

  Log Message:
  -----------
  Use hol.state0 for our early tests


  Commit: 78c1e9618940ec923a0cd7947a60cba84eab732f
      https://github.com/HOL-Theorem-Prover/HOL/commit/78c1e9618940ec923a0cd7947a60cba84eab732f
  Author: Mario Carneiro <di...@gm...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M examples/l3-machine-code/x64/step/x64_stepLib.sml
    M examples/l3-machine-code/x64/step/x64_stepScript.sml

  Log Message:
  -----------
  move proofs out of x64_stepLib


  Commit: 0ec27190aeb059381c230d70097085fd42b14455
      https://github.com/HOL-Theorem-Prover/HOL/commit/0ec27190aeb059381c230d70097085fd42b14455
  Author: Mario Carneiro <di...@gm...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M examples/l3-machine-code/x64/step/x64_stepLib.sml
    M examples/l3-machine-code/x64/step/x64_stepScript.sml

  Log Message:
  -----------
  fix


  Commit: c5d28dbbbff1bf34509719708e928d25e39306c0
      https://github.com/HOL-Theorem-Prover/HOL/commit/c5d28dbbbff1bf34509719708e928d25e39306c0
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M src/TeX/holtexbasic.sty

  Log Message:
  -----------
  Make HOL TeX use \textit for HOL variables, and switch to stix2

Under stix (either version), \mathit{diff} looks horrific because it
refuses to use double-f ligatures.


  Commit: 01f9e7ce8a2034160537b1f84d5c95f74406042f
      https://github.com/HOL-Theorem-Prover/HOL/commit/01f9e7ce8a2034160537b1f84d5c95f74406042f
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-20 (Mon, 20 Apr 2026)

  Changed paths:
    M src/num/reduce/src/Grobner.sml
    M src/num/reduce/src/Normalizer.sml

  Log Message:
  -----------
  Remove some unnecessary dependencies on simpLib and boolSimps


  Commit: 4186723993a85f16a734f59c08cd8f5e20ad5e7c
      https://github.com/HOL-Theorem-Prover/HOL/commit/4186723993a85f16a734f59c08cd8f5e20ad5e7c
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-21 (Tue, 21 Apr 2026)

  Changed paths:
    M examples/l3-machine-code/arm8/asl-equiv/get-armv8.6-hol-snapshot
    M tools/parsing/HOLSourceAST.sml

  Log Message:
  -----------
  Merge branch 'master' into develop


  Commit: 1ad8b7ed6b42758b4d8d83e1abeb05f539ba504e
      https://github.com/HOL-Theorem-Prover/HOL/commit/1ad8b7ed6b42758b4d8d83e1abeb05f539ba504e
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-21 (Tue, 21 Apr 2026)

  Changed paths:
    A tools/Holmake/core/HM_Cachekey.sig
    A tools/Holmake/core/HM_Cachekey.sml
    A tools/Holmake/core/HM_Cachekey_dtype.sml
    M tools/Holmake/core/HM_Core_Cline.sig
    M tools/Holmake/core/HM_Core_Cline.sml
    M tools/Holmake/core/Holmake.sml
    M tools/Holmake/hmcore.ML
    M tools/Holmake/hmcore.mlb
    M tools/Holmake/mlton/Holmake.mlb
    M tools/Holmake/mosml/BuildCommand.sml
    M tools/Holmake/poly/BuildCommand.sml
    M tools/Holmake/poly/poly-Holmake.ML
    M tools/Holmake/tests/parallel_tests/Holmakefile
    A tools/Holmake/tests/rebuild_cachekey/Holmakefile
    A tools/Holmake/tests/rebuild_cachekey/selftest.sml
    A tools/Holmake/tests/rebuild_cachekey/subdir/baseScript.sml
    A tools/Holmake/tests/rebuild_cachekey/subdir/childScript.sml
    M tools/configure.sml
    M tools/util/FunctionalRecordUpdate.sml

  Log Message:
  -----------
  Avoid rebuilds based on mtime, using cachekey instead (#381, #1913)

* Make export_theory idempotent on no-op rebuilds (#381)

When Holmake reruns a script file that happens to produce a
Theory.dat whose content is identical to the existing one (for
example because the edit to fooScript.sml was comment-only, or was
made and then reverted), we would previously still overwrite
fooTheory.dat, fooTheory.sml and fooTheory.sig, advancing their
mtimes and causing Holmake's timestamp-based dep-check to cascade
rebuilds to every descendant theory.

Change export_theory so that each of the three generated files is
first written to a sibling tempfile (<path>.new), and only renamed
over the destination when content actually differs (SHA1 compared).
If the content matches, the tempfile is removed and the existing
destination file (and its mtime) is left alone, so descendants are
not invalidated.

Key points:

* We work in real filesystem paths here rather than HOL paths,
  because HFS_NameMunge.HOLtoFS routes generated theory files into
  .hol/objs/ based on their extension, and a ".new" suffix is not
  recognised.  The tempfile therefore has to be constructed as
  <real-dst>.new, and we explicitly ensure the munged output
  directory exists before opening the tempfile.

* The SHA1 of the new .dat, which is already computed for embedding
  into fooTheory.sml, is reused when deciding whether to replace
  the old .dat (no extra hash pass).  For .sig/.sml the helper
  hashes on demand.

* The rename-or-discard step uses OS.FileSys.rename / remove on
  real paths directly, bypassing HOLFileSys's munging (which would
  re-munge the .new-suffixed tempfile path incorrectly).

* No Holmake change: Holmake continues to use mtime-based rebuild
  decisions.  The win is purely from export_theory no longer
  bumping mtimes unnecessarily.

Adds a selftest (tools/Holmake/tests/idempotent_export) that
verifies:

  - a comment-only edit to baseScript.sml does not advance
    baseTheory.dat's mtime, and therefore does not rebuild
    childTheory;
  - a real content change (added theorem) to baseScript.sml does
    advance both baseTheory.dat and childTheory.dat mtimes;
  - a mere `touch` of baseScript.sml (reruns the script but
    produces byte-identical output) does not advance
    baseTheory.dat's mtime.

This is a first, Holmake-free step towards #381; later steps can
teach Holmake itself to consult content hashes rather than
timestamps, but this change on its own is enough to eliminate the
most common source of unnecessary cascading rebuilds.

* Use [bare] theory attribute in selftest to avoid build failure

* Revert idempotent export_theory work

Reverts:
  693443701 Use [bare] theory attribute in selftest to avoid build failure
  74aede3ff Make export_theory idempotent on no-op rebuilds (#381)

The install_if_changed approach in export_theory cannot by itself
preserve Theory.dat mtimes, because Holmake's BuildCommand.sml
preemptively deletes the expected output files (.dat, .sml, .sig)
before re-running the script, so export_theory never sees an
existing destination to compare against.

Rather than work around that via an intermediate rename-to-.prev
scheme, the plan is to move rebuild-avoidance up to Holmake itself,
using the cachekey machinery already introduced in #1820 to
short-circuit script execution when the inputs are unchanged.  A
subsequent commit will implement that.

* Extract HM_Cachekey module and add --rebuild=<strategy> Holmake option

Groundwork for issue #381: let Holmake use recursive content hashes
(cachekeys) instead of mtimes to decide when a theory target is
up-to-date.  This commit only lays out the plumbing; the actual
rebuild-decision change will come in a follow-up.

Changes:

* New module HM_Cachekey (tools/Holmake/core/) that exposes
    compute_for_node : 'a HM_DepGraph.t -> node -> compute_result
  where
    datatype compute_result = Key of string
                            | Missing of {name, path} list
  This is the cachekey algorithm previously buried inside Holmake.sml's
  do_cachekey function, now reusable from the rebuild-decision path.
  The module also provides stamp-file helpers
    stamp_path_for_datfile, read_stamp, write_stamp, remove_stamp
  for recording the cachekey of the inputs that produced each
  theory .dat file.

* New tiny structure HM_Cachekey_dtype (in its own source file so
  HM_Core_Cline can depend on it without pulling in HM_DepGraph).
  Defines
    datatype rebuild_strategy = Mtime | Cachekey
  together with fromString/toString converters.

* HM_Core_Cline gains a rebuild : rebuild_strategy field (default
  Cachekey), wired through the 27-field FunctionalRecordUpdate
  plumbing.  A new command-line option --rebuild=<mtime|cachekey>
  sets it; the intent is for the flag to govern how theory targets
  decide whether to rerun their script.

* Holmake.sml's do_cachekey is refactored to delegate to
  HM_Cachekey.compute_for_node; behaviour for --cachekey is
  unchanged (same key on the same inputs, same error message on a
  missing dependency).

* Build glue: HM_Cachekey(_dtype) added to hmcore.mlb, hmcore.ML,
  mlton/Holmake.mlb, and poly-Holmake.ML.  FunctionalRecordUpdate
  gains makeUpdate27 (was capped at 26).

No user-visible behaviour change yet: --rebuild defaults to cachekey
but the rebuild-decision logic still consults mtime.  The
rebuild-decision wiring and the stamp read/write integration in
BuildCommand.sml follow in subsequent commits.

* Short-circuit theory rebuilds when --rebuild=cachekey and inputs unchanged

This makes --rebuild=cachekey (the new default) functional: Holmake
no longer reruns a theory script when the recursive content hash of
its inputs matches the hash recorded at the previous successful
build.  Under --rebuild=mtime, behaviour is unchanged.

How the skip works:

* After a successful script run, BuildCommand writes the cachekey
  of the script's dependencies to a sibling stamp file
      <thy>Theory.cachekey
  next to <thy>Theory.dat (in .hol/objs/ under Poly/ML).  The
  stamp is removed at the start of every script run so a failed
  or interrupted run cannot leave a false-positive claim of being
  up-to-date on disk.

* During dep-graph construction in Holmake.sml, when the target
  is a theory (BIC_BuildScript) and the strategy is Cachekey, we
  check that the target file exists, that all deps are already
  built, and that the stamp records a key equal to the current
  cachekey (computed from the same dep list that will be passed
  to the script runner).  If so, the node is marked Succeeded
  immediately and the script is not executed.  If any of these
  conditions fails, we fall back to the existing mtime-based
  needs_building logic.

Supporting changes:

* HM_Cachekey exposes a new lower-level compute_for_deps that
  works on a plain dep list, so the same logic can be invoked
    - at decision time in Holmake.sml, before the node has been
      added to the graph;
    - at success time in BuildCommand.sml, which has the dep list
      but no graph node.
  compute_for_node is reimplemented in terms of compute_for_deps.

* BuildCommand's run_script (poly) now takes an on_success
  callback that fires iff the script's exit status is success
  and the expected outputs are about to be accepted.  The
  BuildScript dispatch passes a callback that writes the
  cachekey stamp; BuildArticle passes a no-op.  The mosml build
  command is changed analogously in-place.

* Holmake.sml reads the rebuild strategy from the command-line
  options into cline_rebuild_strategy, alongside the existing
  cline_cachekey.

No change to the --cachekey CLI command: it continues to compute
and print the same hash.  Holmakefile syntax, build-product
formats, and dep-graph shape are unchanged.

Selftests for the new behaviour will follow in a subsequent
commit.

* Add selftest for rebuild=cachekey

* Attempt to fix mosml build


  Commit: e26190f3b2295dde080df77081117fbb2966ff70
      https://github.com/HOL-Theorem-Prover/HOL/commit/e26190f3b2295dde080df77081117fbb2966ff70
  Author: Matt <328...@us...>
  Date:   2026-04-22 (Wed, 22 Apr 2026)

  Changed paths:
    M tools/Holmake/core/HM_Core_Cline.sig
    M tools/Holmake/core/HM_Core_Cline.sml
    M tools/Holmake/core/Holmake.sml
    M tools/Holmake/hmcore.ML
    M tools/Holmake/hmcore.mlb
    M tools/Holmake/mlton/Holmake.mlb
    A tools/Holmake/mosml/HM_CacheFetch.sml
    M tools/Holmake/poly/BuildCommand.sml
    A tools/Holmake/poly/HM_CacheFetch.sml
    M tools/Holmake/poly/MB_Monitor.sml
    M tools/Holmake/poly/ProcessMultiplexor.sig
    M tools/Holmake/poly/ProcessMultiplexor.sml
    M tools/Holmake/poly/multibuild.sml
    M tools/Holmake/poly/poly-Holmake.ML
    A tools/Holmake/tests/cachefetch/Holmakefile
    A tools/Holmake/tests/cachefetch/selftest.sml
    A tools/Holmake/tests/cachefetch/subdir/fooScript.sml
    M tools/Holmake/tests/parallel_tests/Holmakefile
    M tools/configure.sml
    M tools/util/FunctionalRecordUpdate.sml

  Log Message:
  -----------
  Add support for Holmake building from a cache (#1911)

* implement holmake cache (upload/download) for local files

* fixes

* fix selecting targets from current folder

* use info/warn from Holmake_tools output_functions

* clean up

* cleaner refactor for passing output functions

* add tests

* refactor to fit with the new rebuild by cachekey machinery

* fix tests


  Commit: 27b28d294f05adcabc730d2634bfba6af9a40746
      https://github.com/HOL-Theorem-Prover/HOL/commit/27b28d294f05adcabc730d2634bfba6af9a40746
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-22 (Wed, 22 Apr 2026)

  Changed paths:
    M release-notes/next-release.md
    M tools/editor-modes/emacs/hol-mode.src
    M tools/editor-modes/emacs/holscript-mode.el

  Log Message:
  -----------
  [emacs-mode] Provide add-unicode to pair w/remove-unicode; change keys

Unicode-related functionality now all sits under M-h u prefix with
subsequent keys:

  +   : adds in Unicode, replacing ASCII, e.g., /\ ↦  ∧
  -   : removes Unicode, as per what used to be M-h a
  p   : toggles Unicode pretty-printing

Closes #1879


  Commit: 3ffbec842aca68092395f11b74e636984d958444
      https://github.com/HOL-Theorem-Prover/HOL/commit/3ffbec842aca68092395f11b74e636984d958444
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-22 (Wed, 22 Apr 2026)

  Changed paths:
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  Removed unused TheoryPP.pp_sig_hook

This hook could only be used to generate a side effect (had type
unit->unit) before the comment part of a Theory.sig file was generated.


  Commit: 1ea272ca02ea53bb4cc30229b5f8951325176b38
      https://github.com/HOL-Theorem-Prover/HOL/commit/1ea272ca02ea53bb4cc30229b5f8951325176b38
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-22 (Wed, 22 Apr 2026)

  Changed paths:
    M .gitignore
    M src/postkernel/Theory.sml
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml

  Log Message:
  -----------
  Start on work to remove large comments from *Theory.sig files

Instead put essentially the same text into *Theory.txt.


  Commit: 602e639fb0fd5f17d20558e902a8d2c776d8da9a
      https://github.com/HOL-Theorem-Prover/HOL/commit/602e639fb0fd5f17d20558e902a8d2c776d8da9a
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-23 (Thu, 23 Apr 2026)

  Changed paths:
    M src/1/boolLib.sml
    A src/basicProof/theory_tests/suspCrossAScript.sml
    A src/basicProof/theory_tests/suspCrossBScript.sml
    A src/basicProof/theory_tests/suspFastScript.sml
    A src/basicProof/theory_tests/suspRerunScript.sml
    A src/basicProof/theory_tests/suspSibAScript.sml
    A src/basicProof/theory_tests/suspSibBScript.sml
    A src/basicProof/theory_tests/suspSibCScript.sml
    A src/basicProof/theory_tests/suspSibDScript.sml
    M src/marker/markerLib.sig
    M src/marker/markerLib.sml
    M src/marker/selftest.sml
    M tools/Holmake/tests/quote-filter/expected-mosml
    M tools/Holmake/tests/quote-filter/expected-poly
    M tools/parsing/HOLSourceExpand.sml
    M tools/parsing/HolParserOld.sml

  Log Message:
  -----------
  Functional suspend/Resume (#1912)

* Draft implementation of functional suspend/Resume

Working to the design described in #1883

* Handle invalid SML identifier suspension names

* Add more selftests of suspend/Resume, across files

* Add explicit support for --fast (plus selftest)

* Switch to using AncestryData: address review comment

* Fix wrong type

* Fix types around uses of bij_ed

* Fix treatment of deltas when in current theory

* Theory-qualify suspension store keys, eliminate ancestry scans

Address PR review feedback to avoid scanning all ancestors when looking
up suspended theorems and resumption proofs.

Key changes:

1. Change suspension.theorems store to key by (thy, name) instead of
   just name. This allows distinct suspended theorems with the same
   name in different theories (e.g., fooTheory.mythm vs barTheory.mythm).

2. Record the originating theory at suspension time rather than
   searching for it later. The suspended_theorem_recorder now captures
   Theory.current_theory() when stashing.

3. Remove find_parent_thy_in_store and find_parent_thy_in_db functions.
   The theory is now obtained directly from the suspension key, so no
   ancestry scanning is needed.

4. Update lookup_suspension to:
   - Return (string * thm) option, where the string is the theory name
   - Support both unqualified "foo" and qualified "thy$foo" syntax
   - For unqualified lookups, scan the in-memory dictionary keys (not
     an ancestry scan - just filtering the merged global state)

5. Update find_parent to return (source, parent_thy, thm) tuple,
   threading the theory through to callers.

6. Update all callers (resume, finalise_suspended_thm,
   prim_set_suspended_goal) to use the new return types.

7. Fix RemoveSuspended delta to use (thy, name) key.

* Address review comments

* Fix types


  Commit: 86a5d9bc27d3d7e07299dd3cf69d4e7bebf4d5f2
      https://github.com/HOL-Theorem-Prover/HOL/commit/86a5d9bc27d3d7e07299dd3cf69d4e7bebf4d5f2
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-24 (Fri, 24 Apr 2026)

  Changed paths:
    M tools/Holmake/core/HM_GraphBuildJ1.sml
    M tools/Holmake/poly/multibuild.sml
    A tools/Holmake/tests/longcmdlock/Holmakefile
    A tools/Holmake/tests/longcmdlock/selftest.sml

  Log Message:
  -----------
  Don't use long command filename for locks (#1921)

Fixes #1920

Includes selftest


  Commit: f439019142c52b17db2b9f2a60bc0d548462e707
      https://github.com/HOL-Theorem-Prover/HOL/commit/f439019142c52b17db2b9f2a60bc0d548462e707
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-24 (Fri, 24 Apr 2026)

  Changed paths:
    M tools/Holmake/tests/parallel_tests/Holmakefile

  Log Message:
  -----------
  Include new longcmdlock selftest for Holmake in std. sequence


  Commit: 1d7b982dc38e4986eb817c46dafd24f8e59a35b0
      https://github.com/HOL-Theorem-Prover/HOL/commit/1d7b982dc38e4986eb817c46dafd24f8e59a35b0
  Author: Michael Norrish <mic...@an...>
  Date:   2026-04-24 (Fri, 24 Apr 2026)

  Changed paths:
    M tools/Holmake/tests/longcmdlock/selftest.sml

  Log Message:
  -----------
  Get longcmdlock selftest to pass under Moscow ML


  Commit: 3de8caf0248f867d2617826b65c9c5970ed2ae3c
      https://github.com/HOL-Theorem-Prover/HOL/commit/3de8caf0248f867d2617826b65c9c5970ed2ae3c
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M tools-poly/lsp-server.ML

  Log Message:
  -----------
  Add HOL parse trees to LSP server

Work on #1846


  Commit: 7bc6aec42d6565d6aad32fc911d50bda9b872d4f
      https://github.com/HOL-Theorem-Prover/HOL/commit/7bc6aec42d6565d6aad32fc911d50bda9b872d4f
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M tools-poly/holide.ML
    M tools-poly/lsp-server.ML

  Log Message:
  -----------
  Switch to built trees instead of hol/ml trees


  Commit: 5f6f73f0c886ce558a2822325c1254de786ddc0f
      https://github.com/HOL-Theorem-Prover/HOL/commit/5f6f73f0c886ce558a2822325c1254de786ddc0f
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M tools-poly/holide.ML
    M tools-poly/lsp-server.ML

  Log Message:
  -----------
  Don't change the navigation logic so much


  Commit: 7f7569b2ff73df7ae51c45658ec889ef8448bd08
      https://github.com/HOL-Theorem-Prover/HOL/commit/7f7569b2ff73df7ae51c45658ec889ef8448bd08
  Author: Matt <328...@us...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    A src/basicProof/theory_tests/suspNestedScript.sml
    M src/marker/markerLib.sig
    M src/marker/markerLib.sml
    M src/marker/selftest.sml

  Log Message:
  -----------
  Fix nested suspense/resume proofs (#1923)

* fix nested suspense/resume proofs

* fix spacing


  Commit: e519ff8310f78fbfcd21ece3a05473dc9ae87974
      https://github.com/HOL-Theorem-Prover/HOL/commit/e519ff8310f78fbfcd21ece3a05473dc9ae87974
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M src/postkernel/prooftrace/.gitignore
    M src/postkernel/prooftrace/Holmakefile
    A src/postkernel/prooftrace/PFTOpcodes.sig
    A src/postkernel/prooftrace/PFTOpcodes.sml
    A src/postkernel/prooftrace/PFTReader.sig
    A src/postkernel/prooftrace/PFTReader.sml
    A src/postkernel/prooftrace/PFTReplay.sig
    A src/postkernel/prooftrace/PFTReplay.sml
    A src/postkernel/prooftrace/pft-format.md
    A src/postkernel/prooftrace/pft-replay-test.mlb
    A src/postkernel/prooftrace/pft-replay-test.sml
    A src/postkernel/prooftrace/pft-replay.mlb
    A src/postkernel/prooftrace/pft-ruleset-hol4.md

  Log Message:
  -----------
  Add PFT replay module

This commit introduces the PFT format for HOL proof traces and a
standalone tool for replaying proofs in that format in HOL4.

In the future we intend to also integrate such replay in the system
using the --thmsrc option of Holmake/build.


  Commit: 2bc77711c2c1d20a66daa7209b81f1d2e4ebe75a
      https://github.com/HOL-Theorem-Prover/HOL/commit/2bc77711c2c1d20a66daa7209b81f1d2e4ebe75a
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M examples/lambda/barendregt/boehmScript.sml
    M examples/lambda/barendregt/chap2Script.sml
    M examples/lambda/barendregt/chap3Script.sml
    M examples/lambda/barendregt/head_reductionScript.sml
    M examples/lambda/barendregt/solvableScript.sml
    M examples/lambda/barendregt/takahashiS3Script.sml

  Log Message:
  -----------
  Some lemmas about eta-reduction and beta-eta equivalence


  Commit: 059423e54b150d42f36309bb70ed789e9619e560
      https://github.com/HOL-Theorem-Prover/HOL/commit/059423e54b150d42f36309bb70ed789e9619e560
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M examples/lambda/barendregt/chap3Script.sml
    M examples/lambda/barendregt/head_reductionScript.sml
    M examples/lambda/barendregt/horeductionScript.sml
    M examples/lambda/barendregt/solvableScript.sml

  Log Message:
  -----------
  Use Overload syntax; add further hnf_bestar_cases


  Commit: 49d055302c1a002be77ab39b156e838c525b2401
      https://github.com/HOL-Theorem-Prover/HOL/commit/49d055302c1a002be77ab39b156e838c525b2401
  Author: Chun Tian (binghe) <bin...@gm...>
  Date:   2026-04-28 (Tue, 28 Apr 2026)

  Changed paths:
    M examples/lambda/barendregt/boehmScript.sml

  Log Message:
  -----------
  Fix statements of lameq_subterm_cong


  Commit: 8bfa052cbaee2a4e8e0128a0025dd1e5abe9fe21
      https://github.com/HOL-Theorem-Prover/HOL/commit/8bfa052cbaee2a4e8e0128a0025dd1e5abe9fe21
  Author: Daniel Nezamabadi <555...@us...>
  Date:   2026-04-29 (Wed, 29 Apr 2026)

  Changed paths:
    M src/IndDef/selftest.sml
    M tools/parsing/HOLSourceAST.sml

  Log Message:
  -----------
  Fix isOnlyComments

Closes #1931

Assisted-by: Claude:claude-opus-4-7


  Commit: 60700bdf7cbbfca4f59cf0a84c07c2ce018801cc
      https://github.com/HOL-Theorem-Prover/HOL/commit/60700bdf7cbbfca4f59cf0a84c07c2ce018801cc
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-01 (Fri, 01 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/Holmakefile

  Log Message:
  -----------
  Check for mlton in the PATH when building postkernel/prooftrace


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/77fad203c275...60700bdf7cbb

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 9b6438: Run AliasGen --check from build_help

[Michael N. <no...@gi...>]

  Branch: refs/heads/reference-alias-machinery
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 9b64383d8261d879f89879c537ee8cd3e1dc34c9
      https://github.com/HOL-Theorem-Prover/HOL/commit/9b64383d8261d879f89879c537ee8cd3e1dc34c9
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M help/src-sml/Holmakefile
    M tools/.gitignore
    M tools/build/buildutils.sml

  Log Message:
  -----------
  Run AliasGen --check from build_help

Wire the alias-consistency check into the regular build pipeline so
hand-edited drift between canonical and stub reference entries fails
the build instead of getting noticed only when the manual is built.

build_help (called near the end of bin/build) now compiles
AliasGen.exe alongside makebase.exe and gen_extra_docfiles, then runs
AliasGen.exe --check on help/Docfiles before producing any derived
output.  On failure, build_help dies with a hint to run
help/src-sml/AliasGen.exe --regen help/Docfiles.

Adds AliasGen.exe to the help/src-sml Holmakefile's `all` target so
the mosml branch (mosml_compilehelp) builds it via Holmake.

Drive-by: tighten tools/.gitignore.  The bare `build` rule was
intended to ignore a compiled executable but also matched the
tools/build/ source directory, complicating any new file added there.
Replace with the anchored `/build` plus `!/build/` so the file is
still ignored but the directory is explicitly visible.

Towards GitHub issue #319.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] e882b1: Migrate src/ map users to Table-derived structures...

[Michael N. <no...@gi...>]

  Branch: refs/heads/table-sml-phase1
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: e882b10dd329e41d2b4f4c97c80eabfaca522295
      https://github.com/HOL-Theorem-Prover/HOL/commit/e882b10dd329e41d2b4f4c97c80eabfaca522295
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/1/DefnBaseCore.sml
    M src/1/Drule.sml
    M src/1/Ho_Net.sml
    M src/1/Pmatch.sml
    M src/1/Prim_rec.sml
    M src/1/TypeBasePure.sml
    M src/1/match_goal.sml
    M src/1/simpfrag.sml
    M src/HolSat/dpll.sml
    M src/IndDef/IndDefLib.sig
    M src/IndDef/IndDefLib.sml
    M src/TeX/EmitTeX.sml
    M src/TeX/holindex.lex
    M src/TeX/holindex.sml
    M src/TeX/holindexData.sig
    M src/TeX/holindexData.sml
    M src/TeX/mungeTools.sig
    M src/TeX/mungeTools.sml
    M src/basicProof/BasicProvers.sml
    M src/bool/TexTokenMap.sig
    M src/bool/TexTokenMap.sml
    M src/compute/src/clauses.sml
    M src/datatype/Datatype.sml
    M src/datatype/record/RecordType.sml
    M src/emit/ConstMapML.sml
    M src/finite_maps/alist_treeLib.sml
    M src/finite_maps/flookupLib.sml
    M src/floating-point/binary_ieeeLib.sml
    M src/integer/CooperShell.sml
    M src/integer/CooperSyntax.sml
    M src/integer/OmegaMath.sml
    M src/integer/OmegaSymbolic.sml
    M src/marker/markerLib.sml
    M src/metis/metisTools.sml
    M src/monad/monadsyntax.sml
    M src/n-bit/bitstringLib.sml
    M src/n-bit/blastLib.sml
    M src/n-bit/wordsLib.sml
    M src/num/arith/src/GenRelNorm.sml
    M src/parse/PPBackEnd.sml
    M src/parse/Pretype.sml
    M src/pattern_matches/constrFamiliesLib.sml
    M src/portableML/LSPExtension.sml
    M src/portableML/Profile.sml
    M src/portableML/UTF8Set.sml
    M src/portableML/UnicodeChars.sml
    M src/postkernel/Theory.sml
    M src/postkernel/TheoryGraph.sml
    M src/postkernel/TheoryPP.sig
    M src/postkernel/TheoryPP.sml
    M src/postkernel/prooftrace/PFTReplay.sml
    M src/postkernel/prooftrace/ProofTraceReplay.sig
    M src/postkernel/prooftrace/ProofTraceReplay.sml
    M src/postkernel/prooftrace/ProofTraceWalk.sig
    M src/postkernel/prooftrace/ProofTraceWalk.sml
    M src/postkernel/prooftrace/ThmSrc_tr.sml
    M src/prekernel/Feedback.sml
    M src/prekernel/stringfindreplace.sml
    M src/proofman/goalStack.sml
    M src/quantHeuristics/ConseqConv.sml
    M src/quantHeuristics/quantHeuristicsLibAbbrev.sml
    M src/quantHeuristics/quantHeuristicsLibBase.sml
    M src/quotient/src/quotient.sml
    M src/refute/Canon.sml
    M src/simp/src/Cache.sml
    M src/simp/src/Cond_rewr.sml
    M src/sort/permLib.sml
    M src/taut/tautLib.sml
    M src/tfl/src/Defn.sml
    M src/transfer/transferLib.sml

  Log Message:
  -----------
  Migrate src/ map users to Table-derived structures (issue #1595)

Phase 1 of replacing Binaryset/Redblackset/Redblackmap/Binarymap
with structures derived from src/portableML/Table.sml (the
Isabelle-style 2-3 tree functor).  This commit covers the
per-directory walk through src/ -- one directory at a time, each
using the most appropriate existing instantiation (Symtab, Inttab,
Termtab, KNametab, Typetab, Symreltab) or a locally-defined Tab
where the key type doesn't already have a top-level instantiation.

Directories converted:

  src/portableML/Profile, src/bool/TexTokenMap (early pilots),
  src/portableML, src/prekernel, src/postkernel,
  src/postkernel/prooftrace, src/parse, src/1, src/compute/src,
  src/HolSat (just dpll), src/taut, src/marker, src/refute,
  src/simp/src, src/metis (just metisTools),
  src/IndDef + src/basicProof (rule-induction map together),
  src/quotient/src, src/tfl/src, src/num/arith/src,
  src/datatype, src/datatype/record, src/monad, src/quantHeuristics,
  src/pattern_matches, src/sort, src/transfer, src/proofman,
  src/emit, src/floating-point, src/finite_maps, src/integer,
  src/n-bit (one site stays pending Conv.memoize), src/TeX +
  src/TeX/EmitTeX.

Set operations (union/intersection/difference/subset) and
polymorphic comparator-passing abstractions (Conv.memoize, aiLib,
mlib*, HolSat RBM/SVM) are explicitly out of scope for this
phase.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 57f9353a54fa223f9a3b1e1d0a82b8510bfe24f0
      https://github.com/HOL-Theorem-Prover/HOL/commit/57f9353a54fa223f9a3b1e1d0a82b8510bfe24f0
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/postkernel/Holmakefile
    M src/postkernel/SharingTables.sig
    M src/postkernel/SharingTables.sml
    A src/postkernel/Typetab.sml

  Log Message:
  -----------
  Switch SharingTables to Symtab/Idtab/Typetab/Termtab (issue #1595)

Adds a new top-level Typetab in src/postkernel (parallels the existing
Termtab; partially addresses #1595's "bonus points" task of providing
pre-instantiated maps for common HOL key types).

Migrates SharingTables itself: the `structure Map = Binarymap` aliasing
goes away, and each of stringtable.map, idtable.idmap, typetable.tymap,
termtable.termmap becomes the corresponding Symtab/Idtab/Typetab/Termtab.
Idtab is declared local to SharingTables.sml (the {Thy, Other} key type
is itself private to SharingTables).  build_type_vector and
build_term_vector's int-keyed result maps move to Inttab, with the
Map.find/handle NotFound idiom rewritten as an explicit case-of that
raises SharingTables on missing keys (preserving the user-facing
exception type for build_type_vector; build_term_vector's previous
behaviour was to leak Binarymap.NotFound, which is an improvement).

The signature change is invisible to all known consumers: a sweep of
src/ shows that no consumer accesses Map, the dict-typed record fields,
or the Binarymap structure itself — they only call public functions
(dec_sdata, build_*_vector, write_string/type/term, enc_*).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 824628ca1e892fb7b46e84540b3c3592f2d67830
      https://github.com/HOL-Theorem-Prover/HOL/commit/824628ca1e892fb7b46e84540b3c3592f2d67830
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/real/SOSLib.sml

  Log Message:
  -----------
  Switch src/real/SOSLib to Termtab/MonoTab/IntPairTab/IntTripleTab (issue #1595)

Migrates the entire 2655-line SOS algebraic library, which had no
public-API surface but used Redblackmap (aliased as IMap in places)
internally for ~100 sites:

* monomial (term -> int) → int Termtab.table
* poly (monomial -> rat) → rat MonoTab.table, with a local MonoTab
  defined directly under mono_compare
* vector (int -> rat) → rat Inttab.table
* matrix ((int*int) -> rat) → rat IntPairTab.table, with a local
  IntPairTab
* equation (eqvar -> rat, eqvar = int*int) → rat IntPairTab.table
* equation3 (eqvar3 -> rat, eqvar3 = int*int*int) → rat
  IntTripleTab.table, with a local IntTripleTab
* bmatrix (eqvar3 -> rat) → rat IntTripleTab.table
* epoly (monomial -> equation3) → equation3 MonoTab.table

Translation is mechanical:
  Redblackmap.foldl (fn (k, v, acc) => …)  →
  <Tab>.fold (fn (k, v) => fn acc => …)
The key gotcha is the swapped argument order — Table.fold takes the
table before the seed, where Redblackmap.foldl took the seed before
the table.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 76a45985a5ab195e760c145bf49f446b33693ddb
      https://github.com/HOL-Theorem-Prover/HOL/commit/76a45985a5ab195e760c145bf49f446b33693ddb
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/1/FullUnify.sig
    M src/1/FullUnify.sml
    M src/1/TypeBase.sml
    M src/1/theory_tests/gh168aScript.sml
    M src/1/theory_tests/gh168bScript.sml
    M src/1/theory_tests/gh168cScript.sml
    M src/1/theory_tests/gh168eScript.sml
    M src/HolQbf/QDimacs.sml
    M src/HolQbf/QbfCertificate.sml
    M src/basicProof/BasicProvers.sml
    M src/parse/FCNet.sml
    M src/parse/LVTermNet.sig
    M src/parse/LVTermNet.sml
    M src/parse/LVTermNetFunctor.sml
    M src/parse/Overload.sml
    M src/parse/TypeNet.sig
    M src/parse/TypeNet.sml
    M src/parse/parse_term.sig
    M src/parse/parse_term.sml
    M src/parse/parse_type.sml
    M src/parse/term_grammar.sml
    M src/parse/term_pp.sml
    M src/parse/type_grammar.sig
    M src/parse/type_grammar.sml
    M src/parse/type_pp.sml
    R src/portableML/HOLdict.sig
    R src/portableML/HOLdict.sml
    M src/postkernel/DB.sml
    M src/prekernel/Lib.sig
    M src/prekernel/Lib.sml
    M src/real/RealArith0.sml

  Log Message:
  -----------
  Remove HOLdict and switch FullUnify Env to Symtab/Termtab (issue #1595)

Two related public-API surface cleanups:

* HOLdict was a wrapper around Redblackmap, structurally identical
  except for the helper `dict_topsort`.  After mass-renaming
  HOLdict->Redblackmap across 28 consumers, the wrapper is
  redundant; both wrapper files are deleted.  Per-consumer
  migration to specific Tabs follows in the next commit.

* FullUnify.Env's tri-state environment is rebuilt on top of
  (hol_type Symtab.table * term Termtab.table) instead of two
  Redblackmaps.  triTM and triTY were public exports which turned
  out to have no callers in the tree, contrary to the deferred-
  list note, and so were removed.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 2669464fbb9ecee990871c5e6473762dc7f87ff5
      https://github.com/HOL-Theorem-Prover/HOL/commit/2669464fbb9ecee990871c5e6473762dc7f87ff5
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/1/TypeBase.sml
    M src/1/theory_tests/gh168aScript.sml
    M src/1/theory_tests/gh168bScript.sml
    M src/1/theory_tests/gh168cScript.sml
    M src/1/theory_tests/gh168eScript.sml
    M src/HolQbf/QDimacs.sml
    M src/HolQbf/QbfCertificate.sml
    M src/basicProof/BasicProvers.sml
    M src/parse/FCNet.sml
    M src/parse/LVTermNet.sig
    M src/parse/LVTermNet.sml
    M src/parse/LVTermNetFunctor.sml
    M src/parse/Overload.sml
    M src/parse/TypeNet.sig
    M src/parse/TypeNet.sml
    M src/parse/parse_term.sig
    M src/parse/parse_term.sml
    M src/parse/parse_type.sml
    M src/parse/term_grammar.sml
    M src/parse/term_pp.sml
    M src/parse/type_grammar.sig
    M src/parse/type_grammar.sml
    M src/parse/type_pp.sml
    M src/pattern_matches/constrFamiliesLib.sml
    M src/postkernel/DB.sml
    M src/real/RealArith0.sml

  Log Message:
  -----------
  Migrate post-HOLdict consumers to specific Tabs (issue #1595)

After mass-renaming HOLdict->Redblackmap (previous commit), each of
the 28 consumers moves to the most appropriate Tab structure for
its key type, in five sub-batches:

  1. BasicProvers, FCNet, Overload, RealArith0
  2. type_grammar group: sig+sml + type_pp/parse_type/TypeBase
     (parse_str -> KNametab.table, bare_names -> Symtab.table)
  3. term_pp, term_grammar, parse_term
  4. TypeNet + LVTermNet (custom-key local Tabs)
  5. DB, HolQbf, gh168 tests

`Lib.dict` and `Lib.dict_topsort` intentionally stay polymorphic.

Follow-up exception cleanup folded in: TypeNet, LVTermNet, and
LVTermNetFunctor each declare a local `exception NotFound`
exported from their signature, replacing explicit `raise
Redblackmap.NotFound` re-raises that previously preserved the
public exception interface.  type_grammar's doprint switches
`handle Redblackmap.NotFound` to `handle TypeNet.NotFound`;
constrFamiliesLib's two `TypeNet.find ... handle NotFound` sites
become `case TypeNet.peek ... of` -- the unbound `NotFound` was
a Poly/ML catch-all variable pattern (a latent catch-all-exceptions
bug), and peek-with-option avoids both round-trip and catch-all.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: e69e30adcbd3b2a77f937923b9bc412071a6e168
      https://github.com/HOL-Theorem-Prover/HOL/commit/e69e30adcbd3b2a77f937923b9bc412071a6e168
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/1/ThmSetData.sig
    M src/1/ThmSetData.sml
    M src/num/termination/TotalDefn.sig

  Log Message:
  -----------
  Switch ThmSetData.simple_dictionary to Symtab (issue #1595)

`ThmSetData.simple_dictionary` was the last cross-directory dict
type exposed across src/.  Despite the public-API leak, it turned
out to be cleanly contained:

* The only consumer of the type is `TotalDefn`.
* `TotalDefn.termination_simpdb : unit -> (string,thm) Binarymap.dict`
  has no further consumers anywhere in the tree -- it is only used
  internally as an opaque getter paired with `temp_setDB`.

So this is a two-file move:

* `simple_dictionary` becomes `thm Symtab.table` in both the sig
  and the body.
* `sdict_apply_delta`'s REMOVE branch swaps `Binarymap.remove ...
  handle NotFound => d` for `Symtab.delete_safe`.
* `export_simple_dictionary`'s init fold targets `Symtab.empty`;
  `get_thms` flips the seed/map order for `Symtab.fold`.
* `sdict_withflag_thms` uses `Symtab.update`/`Symtab.empty` directly.
* `TotalDefn.termination_simpdb` updates its return type.
  TotalDefn.sml needs no other change -- the value was never
  inspected.

Bonus: drops a dead `open Binarymap` from `alist_withflag_thms`
(the body did not use any of its bindings).

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: e2649df735e008b23d83fb3d30429dfbf80302a6
      https://github.com/HOL-Theorem-Prover/HOL/commit/e2649df735e008b23d83fb3d30429dfbf80302a6
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/1/TypeBasePure.sml
    M src/parse/parse_term.sig
    M src/parse/parse_term.sml
    M src/pattern_matches/constrFamiliesLib.sml
    M src/postkernel/SharingTables.sig
    M src/postkernel/SharingTables.sml
    M src/postkernel/prooftrace/ProofTraceReplay.sml
    M src/quotient/src/quotient.sml

  Log Message:
  -----------
  Fix source-side issues exposed by fresh-state mosml validation (issue #1595)

Cleaning up source-level issues found while validating the Table.sml
migration on a fresh-checkout build (mosml core build + poly cleanAll
+ bin/build -F).  Three categories:

* Stale Redblackmap reference: ProofTraceReplay.sml line 70 still
  used bare `inDomain(!trDB, thyname)`, which had been brought into
  scope by the now-removed `open Redblackmap`.  Switched to
  `Symtab.defined (!trDB) thyname`.

* Public-API leak of TABLE signature: SharingTables.sig and
  parse_term.sig had `structure Idtab/STBSTab : TABLE where type
  Key.key = ...` exposing the TABLE signature to consumers.  On
  case-insensitive filesystems mosml conflates TABLE.ui and Table.ui
  and refuses to load the result.  Replaced with abstract `type 'a
  idtab` / `type 'a stbstab`; the .sml side adds a matching
  `type 'a foo = 'a Foo.table` alias so opaque sealing matches.

* Redundant local Typetab instantiations: src/1/TypeBasePure.sml,
  src/pattern_matches/constrFamiliesLib.sml, and
  src/quotient/src/quotient.sml each instantiated `Typetab` locally
  with the standard hol_type/Type.compare key, replicating the
  top-level instantiation in src/postkernel/Typetab.sml.  Dropped
  the locals; the sigobj-resident `Typetab` is in scope at each
  use site.

Holmakefile and mlton-mlb adjustments needed for mosml fresh-build
follow in a separate commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 23acc782f7d0db77637db75bfa431cc25063d18b
      https://github.com/HOL-Theorem-Prover/HOL/commit/23acc782f7d0db77637db75bfa431cc25063d18b
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/portableML/mlton/portableML.mlb

  Log Message:
  -----------
  Update src/portableML/mlton/portableML.mlb for Table.sml (issue #1595)

Two adjustments needed when MLton processes this descriptor (which
happens when src/portableML/rawtheory builds dat-printer/theorytool):

* Drop `../HOLdict.sig`/`../HOLdict.sml` lines: those files were
  removed when HOLdict was retired.  This wasn't caught earlier
  because the .mlb is only consulted when MLton is invoked, and
  in-place poly builds had pre-existing dat-printer/theorytool
  executables that satisfied Holmake's freshness check -- only
  fresh-checkout builds (CI's Docker setup, or local
  `bin/build cleanAll`) actually re-invoke MLton.

* Move the Unsynchronized.sml + Table.sml + Symtab.sml + Inttab.sml
  block above UnicodeChars.{sig,sml}: UnicodeChars now uses Symtab
  and Inttab, so they need to load first.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 9cb462ba2c1aac4446614bae4cf0dfdba2ccb057
      https://github.com/HOL-Theorem-Prover/HOL/commit/9cb462ba2c1aac4446614bae4cf0dfdba2ccb057
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    A src/portableML/Chartab.sml
    M src/portableML/Holmakefile
    M src/portableML/mlton/portableML.mlb
    M src/prekernel/stringfindreplace.sml

  Log Message:
  -----------
  Add Chartab as top-level instantiation in src/portableML (issue #1595)

Promotes the Chartab structure (Table functor instantiated with char
keys) from a local definition inside
`src/prekernel/stringfindreplace.sml` to a top-level instantiation
in `src/portableML/Chartab.sml`, alongside Symtab/Inttab/Symreltab.

This means stringfindreplace can use Chartab from sigobj like any
other consumer, and the special-case Holmakefile rule that was
needed to feed Table.ui to mosml when compiling the local
instantiation can be dropped.

* `src/portableML/Chartab.sml` (new), modeled on Inttab.sml.
* `src/portableML/Holmakefile`: new rule next to Inttab/Symtab.
* `src/portableML/mlton/portableML.mlb`: add Chartab.sml after the
  other Tab instantiations.
* `src/prekernel/stringfindreplace.sml`: drop local instantiation;
  the references to Chartab.* in the body now resolve to the sigobj
  structure.
* `src/prekernel/Holmakefile`: drop the `stringfindreplace.uo` rule
  that was loading Table.ui/HOLPP.ui explicitly.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 037a2e0470237bac8ccae3fe220494558607f409
      https://github.com/HOL-Theorem-Prover/HOL/commit/037a2e0470237bac8ccae3fe220494558607f409
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/datatype/record/RecordType.sml

  Log Message:
  -----------
  Drop redundant local Typetab in src/datatype/record/RecordType.sml (issue #1595)

The local `structure Typetab = Table(struct ... end)` instantiation
in RecordType.sml was a clone of the top-level Typetab in
`src/postkernel/Typetab.sml`.  Removed; the `Typetab.*` references
in the rest of the file now resolve to the sigobj-resident
structure.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: 82e55509a76cd5aa01d13aae6b035b151b2d9bd3
      https://github.com/HOL-Theorem-Prover/HOL/commit/82e55509a76cd5aa01d13aae6b035b151b2d9bd3
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/1/Holmakefile
    M src/compute/src/Holmakefile
    M src/marker/Holmakefile
    M src/parse/Holmakefile
    M src/postkernel/Holmakefile

  Log Message:
  -----------
  Add Holmakefile rules for Table-functor instantiation sites (issue #1595)

Files that locally instantiate the Table functor (`structure X =
Table(struct ... end)`) need an explicit Table.ui argument on the
mosmlc command line: mosml's automatic dependency detection picks
up `open Foo` and `Foo.bar` references but not functor applications.

This commit adds Holmakefile rules for each such site touched by
the Table.sml migration.  All rules apply to both poly and mosml
(no `ifndef POLY` gating): poly's auto-rule handles them fine, and
explicit Holmakefile recipes don't break under poly.  Sibling .ui
files are listed as prereqs so Holmake builds them before this
rule fires.

Files getting rules:

* `src/postkernel/Holmakefile`: SharingTables.uo, TheoryGraph.uo
  (Termtab/Typetab rules were already there from earlier commits).
* `src/parse/Holmakefile`: LVTermNetFunctor (now with Table.ui),
  LVTermNet, TypeNet, term_grammar, parse_term.  The
  LVTermNetFunctor entry has no separate `.sig` file (its sig is
  inline in the `.sml`), so the rule must apply under poly too --
  Holmake's default `Foo.ui <- Foo.sig` would otherwise fail
  because there is no Foo.sig.
* `src/1/Holmakefile`: DefnBaseCore, Ho_Net.
* `src/compute/src/Holmakefile`: clauses.
* `src/marker/Holmakefile`: markerLib.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


  Commit: dc97d1581fa28e504753ce79ed6e7c69f000aacd
      https://github.com/HOL-Theorem-Prover/HOL/commit/dc97d1581fa28e504753ce79ed6e7c69f000aacd
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/marker/markerLib.sml

  Log Message:
  -----------
  Switch markerLib's SuspTab to top-level KNametab (issue #1595)

The local `SuspTab` in markerLib was a Table instantiation keyed on
`string * string` (theory-name pair) -- structurally identical to
`KernelSig.kernelname` (a record with `Thy` and `Name` fields).
Switched to use the existing top-level `KNametab` from
`src/prekernel/KNametab.sml`.

Strictly a slight bending of the semantics: kernelnames usually
denote logical entities (constants, type-operators) whereas this
use is a meta-level theory/theorem-name pair.  Reasonable enough
to avoid defining a parallel Tab.

`susp_key` now aliases `KernelSig.kernelname`; construction sites
build `{Thy = ..., Name = ...}` records; the bij_ed encoder packs
the record back to a `(string, string)` pair on the wire so the
on-disk format is unchanged.

`ResTab` (3-tuple key) is unrelated and stays as a local Table
instantiation, so the markerLib.uo Holmakefile rule remains.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/7602098bc456...dc97d1581fa2

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] d753e3: Fix SAT_ORACLE bogus theorems from dropped F conju...

[Michael N. <no...@gi...>]

  Branch: refs/heads/develop
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: d753e36ac449729176abc09134401b55e546a77b
      https://github.com/HOL-Theorem-Prover/HOL/commit/d753e36ac449729176abc09134401b55e546a77b
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-05 (Tue, 05 May 2026)

  Changed paths:
    M src/HolSat/Holmakefile
    M src/HolSat/def_cnf.sig
    M src/HolSat/def_cnf.sml
    M src/HolSat/minisatProve.sml
    A src/HolSat/selftest.sml

  Log Message:
  -----------
  Fix SAT_ORACLE bogus theorems from dropped F conjuncts in to_cnf

When SAT_PROVE/SAT_ORACLE prove a goal `tm`, they ask to_cnf to CNF-ify
`~tm`. GCONJUNCTS splits `~tm` into top-level conjuncts and runs
presimp_conv on any conjunct containing T or F. The to_cnf dispatch
loop then dropped *both* T- and F-valued conjuncts before clausifying
the rest:

    if is_T t orelse is_F t then (m,tops,defs,lfn)
    else …build clause…

Dropping a T conjunct is sound (`p /\ T = p`); dropping an F conjunct
is not (`p /\ F = F`, not `p`). For `tm = b ==> T` the negation is
`b /\ ~T`, which presimps to `b /\ F`; the F clause was silently
dropped, leaving CNF = `[b]`, which MiniSAT correctly reported
satisfiable. SAT_PROVE escaped because its post-hoc satCheck on the
fabricated model failed and the result was discarded; SAT_ORACLE
trusts the SAT verdict and produced the bogus

    SAT_cex |- b ==> ~(b ==> T)

Fix at the root: when to_cnf detects an F conjunct it now raises a new
to_cnf_unsat exception carrying `|- ~tm`, which initialise re-raises
through the existing initexp channel as `|- tm` (via NOT_NOT_CONV).
Both SAT_PROVE and SAT_ORACLE benefit, and so do any other consumers
of to_cnf with the same shape; MiniSAT is no longer invoked for
trivially-unsat preprocessing cases.

A regression test in src/HolSat/selftest.sml asserts
`SAT_ORACLE \`b ==> T\`` returns `|- b ==> T`. The test does not
require a working MiniSAT installation since the fix short-circuits
before invocation.

This is the immediate fix. Issue #1170's discussion also flags a
deeper concern: SAT_ORACLE's "SAT verdict" branch fabricates an
oracle theorem from the SAT solver's model without verifying it, so a
buggy verdict from MiniSAT on any other input can still leak a
bogus theorem. Hardening that path (e.g. always running satCheck) is
left as a follow-up.

Closes #1170

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] b14368: Redo jobs when an existing output doesn't look valid

[Ramana K. <no...@gi...>]

  Branch: refs/heads/replay
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: b1436806029866d4cd27a94422979a1ccf64eebd
      https://github.com/HOL-Theorem-Prover/HOL/commit/b1436806029866d4cd27a94422979a1ccf64eebd
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-04 (Mon, 04 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/emit-candle-merged.sml

  Log Message:
  -----------
  Redo jobs when an existing output doesn't look valid


  Commit: 38e7b1347dbec0cc1d21226b2df9dda7cd6a7403
      https://github.com/HOL-Theorem-Prover/HOL/commit/38e7b1347dbec0cc1d21226b2df9dda7cd6a7403
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-04 (Mon, 04 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/emit-candle-merged.sml

  Log Message:
  -----------
  Tweak cli output


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/c3337ff3cd68...38e7b1347dbe

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 8a00f2: Remove PFTRename

[Ramana K. <no...@gi...>]

  Branch: refs/heads/replay
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 8a00f2170138d51543e942f6b3cb3447b45af56d
      https://github.com/HOL-Theorem-Prover/HOL/commit/8a00f2170138d51543e942f6b3cb3447b45af56d
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/PFTEmit.sig
    R src/postkernel/prooftrace/PFTRename.sig
    R src/postkernel/prooftrace/PFTRename.sml
    M src/postkernel/prooftrace/emit-candle-merged.sml
    M src/postkernel/prooftrace/pipeline-test.sml
    M src/postkernel/prooftrace/pipeline.mlb

  Log Message:
  -----------
  Remove PFTRename


  Commit: efaee6f595efe4d204399d7dd4d2bfdc4af2f29f
      https://github.com/HOL-Theorem-Prover/HOL/commit/efaee6f595efe4d204399d7dd4d2bfdc4af2f29f
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/emit-candle-merged.sml

  Log Message:
  -----------
  Improve emit-candle-merged: parallelise + better CLI


  Commit: e5d41e54c400e5a315e98ade13f80e1c96764814
      https://github.com/HOL-Theorem-Prover/HOL/commit/e5d41e54c400e5a315e98ade13f80e1c96764814
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-03 (Sun, 03 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/PFTEmit.sml

  Log Message:
  -----------
  Improve pft output performance for abs


  Commit: c3337ff3cd68e68fba95c3677ec423abfdbf64e6
      https://github.com/HOL-Theorem-Prover/HOL/commit/c3337ff3cd68e68fba95c3677ec423abfdbf64e6
  Author: Ramana Kumar <ra...@me...>
  Date:   2026-05-04 (Mon, 04 May 2026)

  Changed paths:
    M src/postkernel/prooftrace/PFTEmit.sml
    M src/postkernel/prooftrace/emit-candle-merged.sml

  Log Message:
  -----------
  Locally memoise pft_subst_tm and pft_rename_free

Prevents pathological blowup first encountered in astTheory


Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/1bb03bc34c76...c3337ff3cd68

To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications

[Hol-checkins] [HOL-Theorem-Prover/HOL] 99e0bd: Deduplicate res_quan reference entries by removing...

[Michael N. <no...@gi...>]

  Branch: refs/heads/reference-alias-machinery
  Home:   https://github.com/HOL-Theorem-Prover/HOL
  Commit: 99e0bdfb442f364fdebbe49801639fb2ec5e6a6b
      https://github.com/HOL-Theorem-Prover/HOL/commit/99e0bdfb442f364fdebbe49801639fb2ec5e6a6b
  Author: Michael Norrish <mic...@an...>
  Date:   2026-05-04 (Mon, 04 May 2026)

  Changed paths:
    A help/Docfiles/res_quanLib.RESQ_EXISTS_TAC.md
    A help/Docfiles/res_quanLib.RESQ_GEN_TAC.md
    M help/Docfiles/res_quanLib.RESQ_HALF_SPEC.md
    A help/Docfiles/res_quanLib.RESQ_IMP_RES_TAC.md
    A help/Docfiles/res_quanLib.RESQ_IMP_RES_THEN.md
    A help/Docfiles/res_quanLib.RESQ_MATCH_MP.md
    A help/Docfiles/res_quanLib.RESQ_RES_TAC.md
    A help/Docfiles/res_quanLib.RESQ_RES_THEN.md
    M help/Docfiles/res_quanLib.RESQ_REWRITE1_CONV.md
    M help/Docfiles/res_quanLib.RESQ_REWRITE1_TAC.md
    M help/Docfiles/res_quanLib.RESQ_REWR_CANON.md
    M help/Docfiles/res_quanLib.RESQ_SPEC.md
    A help/Docfiles/res_quanLib.RESQ_SPECL.md
    R help/Docfiles/res_quanTools.IMP_RES_FORALL_CONV.md
    R help/Docfiles/res_quanTools.RESQ_EXISTS_TAC.md
    R help/Docfiles/res_quanTools.RESQ_GEN_TAC.md
    R help/Docfiles/res_quanTools.RESQ_HALF_SPEC.md
    R help/Docfiles/res_quanTools.RESQ_IMP_RES_TAC.md
    R help/Docfiles/res_quanTools.RESQ_IMP_RES_THEN.md
    R help/Docfiles/res_quanTools.RESQ_MATCH_MP.md
    R help/Docfiles/res_quanTools.RESQ_RES_TAC.md
    R help/Docfiles/res_quanTools.RESQ_RES_THEN.md
    R help/Docfiles/res_quanTools.RESQ_REWRITE1_CONV.md
    R help/Docfiles/res_quanTools.RESQ_REWRITE1_TAC.md
    R help/Docfiles/res_quanTools.RESQ_REWR_CANON.md
    R help/Docfiles/res_quanTools.RESQ_SPEC.md
    R help/Docfiles/res_quanTools.RESQ_SPECL.md
    R help/Docfiles/res_quanTools.RES_EXISTS_CONV.md
    R help/Docfiles/res_quanTools.RES_FORALL_AND_CONV.md
    R help/Docfiles/res_quanTools.RES_FORALL_CONV.md
    R help/Docfiles/res_quanTools.RES_FORALL_SWAP_CONV.md
    R help/Docfiles/res_quanTools.dest_res_abstract.md
    R help/Docfiles/res_quanTools.dest_res_exists.md
    R help/Docfiles/res_quanTools.dest_res_forall.md
    R help/Docfiles/res_quanTools.dest_res_select.md
    R help/Docfiles/res_quanTools.is_res_abstract.md
    R help/Docfiles/res_quanTools.is_res_exists.md
    R help/Docfiles/res_quanTools.is_res_forall.md
    R help/Docfiles/res_quanTools.is_res_select.md
    R help/Docfiles/res_quanTools.list_mk_res_exists.md
    R help/Docfiles/res_quanTools.list_mk_res_forall.md
    R help/Docfiles/res_quanTools.mk_res_abstract.md
    R help/Docfiles/res_quanTools.mk_res_exists.md
    R help/Docfiles/res_quanTools.mk_res_forall.md
    R help/Docfiles/res_quanTools.mk_res_select.md
    R help/Docfiles/res_quanTools.strip_res_exists.md
    R help/Docfiles/res_quanTools.strip_res_forall.md

  Log Message:
  -----------
  Deduplicate res_quan reference entries by removing res_quanTools side

The reference manual carried two parallel sets of entries for
restricted-quantifier helpers: one filed under res_quanLib, the other
under res_quanTools.  Most pairs were textually identical except for
the structure name; nothing was gained from keeping both.

Consolidate everything onto res_quanLib:

- 21 plain duplicates (dest/is/mk/list_mk/strip _res_*, RES_*_CONV,
  IMP_RES_FORALL_CONV) deleted on the res_quanTools side; the
  res_quanLib copy already had identical content.

- 4 entries (RESQ_HALF_SPEC, RESQ_REWR_CANON, RESQ_REWRITE1_CONV,
  RESQ_REWRITE1_TAC) had unique See-also cross-references on the
  res_quanTools side (Cond_rewrite.COND_REWR_*, search_top_down,
  RESQ_SPECL, RESQ_REWR_CANON).  Merge those into the res_quanLib
  See-also; replace pre-existing broken refs to RESQ_REWR_CONV with
  RESQ_REWR_CANON; delete res_quanTools side.

- RESQ_SPEC: keep res_quanLib modernised prose; lift the example
  illustrating bound-variable renaming from the res_quanTools entry,
  switch its HOL88 REPL syntax (#let ... ;;, "string" terms) to
  modern HOL4 (>, val it = ..., backtick-quoted term notation).

- 8 entries existed only on the res_quanTools side but their
  identifiers are also exported from res_quanLib (per
  res_quanLib.sig): RESQ_EXISTS_TAC, RESQ_GEN_TAC, RESQ_IMP_RES_TAC,
  RESQ_IMP_RES_THEN, RESQ_MATCH_MP, RESQ_RES_TAC, RESQ_RES_THEN,
  RESQ_SPECL.  Rename to res_quanLib.<id>.md and rewrite internal
  res_quanTools. references accordingly.

Towards GitHub issue #319.

Co-Authored-By: Claude Opus 4.7 (1M context) <no...@an...>



To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications