Skip to content

build: warn when bin/unquote is older than tools/parsing/HolLex #2037

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lukaszcz wants to merge 5 commits into
base: develop
Choose a base branch
from
+43 −0
Open

build: warn when bin/unquote is older than tools/parsing/HolLex #2037

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
718d6ab
build: warn when bin/unquote is older than tools/parsing/HolLex
lukaszcz Aug 10, 2026
3bcd15c
build: warn when bin/hol is older than the sources it is compiled from
lukaszcz Aug 10, 2026
ae9cf65
build: check quote-filter staleness via bin/hol under Poly/ML
lukaszcz Aug 14, 2026
d0f7b36
Merge branch 'develop' into build-check-stale-unquote
lukaszcz Aug 14, 2026
4f674bb
build: reword stale bin/hol check comment
lukaszcz Aug 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions tools-poly/build.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,34 @@ in
die ("No Holmake executable in " ^ fP [HOLDIR, "bin"])
end

(* 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.
Checking hol covers Holmake's embedded filter too: configure builds
Holmake first. *)
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"]};
check_against hol "tools/parsing/HolLex";
app_sml_files (check_against hol)
{dirname = fP [HOLDIR, "tools", "parsing"]})
else ()
end




Expand Down
15 changes: 15 additions & 0 deletions tools/build/build.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down