From 718d6ab4062b53261798100bec9f8387a020f244 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= Date: Mon, 10 Aug 2026 09:19:36 +0000 Subject: [PATCH 1/4] build: warn when bin/unquote is older than tools/parsing/HolLex The quote filter's lexer is generated from tools/parsing/HolLex by configure, and by no Holmakefile rule, so pulling a grammar change into an existing tree leaves the old bin/unquote in place. It then mis-lexes the new syntax, and the failure surfaces a long way from its cause: a lex error part way through some theory build, with nothing pointing at the filter or at the need to reconfigure. build already defends against this class of staleness -- check_against on the configure scripts and on build itself, plus a sweep of every .sml file under tools/Holmake against the Holmake binary -- but none of those reach HolLex, which has no .sml extension and does not live under tools/Holmake. Check it explicitly, raising the same "this suggests you should reconfigure the system" prompt as the existing guards, and only when bin/unquote is actually present so that a tree which has not been configured yet is unaffected. Both build front ends get the check, tools/build for Moscow ML and tools-poly for Poly/ML, each in the idiom the surrounding file already uses for its filesystem calls. --- tools-poly/build.sml | 15 +++++++++++++++ tools/build/build.sml | 15 +++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/tools-poly/build.sml b/tools-poly/build.sml index 223c9c00ea..d2db96c4a1 100644 --- a/tools-poly/build.sml +++ b/tools-poly/build.sml @@ -192,6 +192,21 @@ in die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) end +(* The quote filter's lexer is generated from tools/parsing/HolLex by + configure, and by no Holmakefile rule, so pulling in a grammar change + leaves a stale bin/unquote that silently mis-lexes the new syntax. + The app_sml_files sweep above cannot catch it: HolLex has no .sml + extension and does not live under tools/Holmake. *) +val _ = let + val fP = fullPath + open HOLFileSys + val unquote = fP [HOLDIR,"bin",xable_string "unquote"] +in + if access(unquote, [A_READ, A_EXEC]) then + check_against unquote "tools/parsing/HolLex" + else () +end + diff --git a/tools/build/build.sml b/tools/build/build.sml index 78633c0edf..b951d547b3 100644 --- a/tools/build/build.sml +++ b/tools/build/build.sml @@ -164,6 +164,21 @@ in die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) end +(* The quote filter's lexer is generated from tools/parsing/HolLex by + configure, and by no Holmakefile rule, so pulling in a grammar change + leaves a stale bin/unquote that silently mis-lexes the new syntax. + The app_sml_files sweep above cannot catch it: HolLex has no .sml + extension and does not live under tools/Holmake. *) +val _ = let + val fP = fullPath + open OS.FileSys + val unquote = fP [HOLDIR,"bin",xable_string "unquote"] +in + if access(unquote, [A_READ, A_EXEC]) then + check_against unquote "tools/parsing/HolLex" + else () +end + val _ = case cmdline of From 3bcd15cc670128cfb6cbf79feb778d58f23829ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= Date: Mon, 10 Aug 2026 11:06:12 +0000 Subject: [PATCH 2/4] build: warn when bin/hol is older than the sources it is compiled from bin/hol is compiled by configure from tools-poly/hol.ML and the Holmake sources it links against, and by no Holmakefile rule, so pulling into an existing tree leaves it stale with nothing to say so. The guards already in build do not reach it. check_against covers the configure scripts, build itself and Systeml.sig; the app_sml_files sweep covers tools/Holmake and tools-poly/Holmake but compares them against bin/Holmake, so a tree whose Holmake was regenerated can still run a hol built from quite different sources. hol.ML is covered by nothing at all. This is not hypothetical. 1821cc3 moved the Meta.loadPath extension in hol.ML from before loadState to after, because the state load restores refs to their save-time values and was wiping it, and removed prelude.ML's compensating re-extension in the same commit. A tree carrying the old bin/hol therefore got neither: loadPath stayed at the bare [sigobj], so interactive load and open could not see INCLUDES directories, and the banner prelude prints when the path grows never fired. All six tools/Holmake/tests/repl tests failed against their expected output. That last part is what makes it expensive. repl is a test-only entry in sequences/kernel, so -t reaches it while still inside the kernel sequence, and the failure aborts the build there. Since build cleans and re-uploads sigobj per entry, aborting that early strands every library from src/marker onward, and per-directory Holmake in an affected directory then fails with a name resolution error in unmodified source. Nothing in that symptom points at bin/hol, or at reconfiguring. Poly only: under Moscow ML bin/hol is a shell script emitted by configure, not a compiled artefact, so tools/build/build.sml has nothing to check. --- tools-poly/build.sml | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/tools-poly/build.sml b/tools-poly/build.sml index d2db96c4a1..77b73debfe 100644 --- a/tools-poly/build.sml +++ b/tools-poly/build.sml @@ -207,6 +207,28 @@ in else () end +(* bin/hol is likewise compiled by configure and by no Holmakefile rule, + from tools-poly/hol.ML and from the Holmake sources it links against. + Neither check above reaches it: the sweep compares those sources with + bin/Holmake, so a tree whose Holmake is current can still be running + a hol built from different sources, and hol.ML is caught by nothing + at all. A stale bin/hol misdirects the interactive load path and + fails tools/Holmake/tests/repl, which -t reaches while still inside + sequences/kernel -- so the whole selftest build stops there. *) +val _ = let + val fP = fullPath + open HOLFileSys + val hol = fP [HOLDIR,"bin",xable_string "hol"] +in + if access(hol, [A_READ, A_EXEC]) then + (check_against hol "tools-poly/hol.ML"; + app_sml_files (check_against hol) + {dirname = fP [HOLDIR, "tools-poly", "Holmake"]}; + app_sml_files (check_against hol) + {dirname = fP [HOLDIR, "tools", "Holmake"]}) + else () +end + From ae9cf657867790dfc54db967794d803ab7297939 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= Date: Fri, 14 Aug 2026 14:58:51 +0000 Subject: [PATCH 3/4] build: check quote-filter staleness via bin/hol under Poly/ML Under Poly/ML nothing runs bin/unquote: emit_hol_unquote_script is a no-op there, and the filter's lexer and parser are instead linked into bin/Holmake and bin/hol via hmcore.ML. A stale bin/unquote therefore breaks no build, while the binaries that do mis-lex a pulled grammar change went unchecked -- and the exposure is wider than HolLex, since the HOLSource* and AttributeSyntax sources in tools/parsing are baked in the same way and swept by nothing. So drop the unquote check from tools-poly/build.sml and instead check tools/parsing against bin/hol in its existing check block: HolLex explicitly (no .sml extension), the rest by app_sml_files sweep. Checking hol alone covers Holmake's embedded copy too, because configure builds Holmake before hol -- a bin/hol current with respect to tools/parsing implies a bin/Holmake from the same run or a later one. tools/build/build.sml is unchanged: under Moscow ML unquote genuinely runs as a pipe filter, so its check stands. --- tools-poly/build.sml | 27 ++++++++++----------------- 1 file changed, 10 insertions(+), 17 deletions(-) diff --git a/tools-poly/build.sml b/tools-poly/build.sml index 77b73debfe..8a89f06ffd 100644 --- a/tools-poly/build.sml +++ b/tools-poly/build.sml @@ -192,21 +192,6 @@ in die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) end -(* The quote filter's lexer is generated from tools/parsing/HolLex by - configure, and by no Holmakefile rule, so pulling in a grammar change - leaves a stale bin/unquote that silently mis-lexes the new syntax. - The app_sml_files sweep above cannot catch it: HolLex has no .sml - extension and does not live under tools/Holmake. *) -val _ = let - val fP = fullPath - open HOLFileSys - val unquote = fP [HOLDIR,"bin",xable_string "unquote"] -in - if access(unquote, [A_READ, A_EXEC]) then - check_against unquote "tools/parsing/HolLex" - else () -end - (* bin/hol is likewise compiled by configure and by no Holmakefile rule, from tools-poly/hol.ML and from the Holmake sources it links against. Neither check above reaches it: the sweep compares those sources with @@ -214,7 +199,12 @@ end a hol built from different sources, and hol.ML is caught by nothing at all. A stale bin/hol misdirects the interactive load path and fails tools/Holmake/tests/repl, which -t reaches while still inside - sequences/kernel -- so the whole selftest build stops there. *) + sequences/kernel -- so the whole selftest build stops there. + + tools/parsing is included because the quote filter is linked in, not + run as bin/unquote (HolLex.sml is generated from HolLex by + configure); Holmake embeds it too, but configure builds Holmake + before hol, so checking hol covers both. *) val _ = let val fP = fullPath open HOLFileSys @@ -225,7 +215,10 @@ in app_sml_files (check_against hol) {dirname = fP [HOLDIR, "tools-poly", "Holmake"]}; app_sml_files (check_against hol) - {dirname = fP [HOLDIR, "tools", "Holmake"]}) + {dirname = fP [HOLDIR, "tools", "Holmake"]}; + check_against hol "tools/parsing/HolLex"; + app_sml_files (check_against hol) + {dirname = fP [HOLDIR, "tools", "parsing"]}) else () end From 4f674bb49838ef77482003b0bb5964bebdbb844a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= Date: Fri, 14 Aug 2026 15:06:04 +0000 Subject: [PATCH 4/4] build: reword stale bin/hol check comment The comment's opening "likewise" pointed at the bin/unquote check block deleted in the previous commit, and the tools/parsing rationale trailed as a separate paragraph. Fold both into one self-contained block. --- tools-poly/build.sml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/tools-poly/build.sml b/tools-poly/build.sml index 8a89f06ffd..a4e38d00ad 100644 --- a/tools-poly/build.sml +++ b/tools-poly/build.sml @@ -192,19 +192,17 @@ in die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) end -(* bin/hol is likewise compiled by configure and by no Holmakefile rule, - from tools-poly/hol.ML and from the Holmake sources it links against. - Neither check above reaches it: the sweep compares those sources with - bin/Holmake, so a tree whose Holmake is current can still be running - a hol built from different sources, and hol.ML is caught by nothing - at all. A stale bin/hol misdirects the interactive load path and - fails tools/Holmake/tests/repl, which -t reaches while still inside +(* bin/hol is compiled by configure and by no Holmakefile rule, from + tools-poly/hol.ML, the Holmake sources, and tools/parsing (the quote + filter is linked in rather than run as bin/unquote; HolLex.sml is + generated from HolLex by configure). The sweep above compares those + sources against bin/Holmake only, so hol can be stale while Holmake + is current, and hol.ML is checked nowhere. A stale bin/hol + misdirects the interactive load path and fails + tools/Holmake/tests/repl, which -t reaches while still inside sequences/kernel -- so the whole selftest build stops there. - - tools/parsing is included because the quote filter is linked in, not - run as bin/unquote (HolLex.sml is generated from HolLex by - configure); Holmake embeds it too, but configure builds Holmake - before hol, so checking hol covers both. *) + Checking hol covers Holmake's embedded filter too: configure builds + Holmake first. *) val _ = let val fP = fullPath open HOLFileSys