build: warn when bin/unquote is older than tools/parsing/HolLex - #2037
Open
lukaszcz wants to merge 5 commits into
Open
build: warn when bin/unquote is older than tools/parsing/HolLex#2037lukaszcz wants to merge 5 commits into
lukaszcz wants to merge 5 commits into
Conversation
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.
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.
Member
|
Poly/ML HOL does not run |
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
The quote filter's lexer is generated from
tools/parsing/HolLexbyconfigure, and by no Holmakefile rule. So when a grammar change toHolLexarrives — typically by pulling in someone else's commit —nothing in the build rebuilds
bin/unquote. The stale binary keepsrunning the old lexer and silently mis-lexes the new syntax, and the
resulting failures point anywhere but at the quote filter.
build.smlalready guards against exactly this class of staleness: itruns
check_againstover the configure/build scripts, and sweepsapp_sml_files (check_against hmake)acrosstools/Holmakeandtools-poly/Holmaketo catch a stalebin/Holmake. That sweep cannotcatch
HolLexon either count — it has no.smlextension, and it doesnot live under a
Holmakedirectory.Change
Add a
check_againstcall forbin/unquoteagainsttools/parsing/HolLex, in both build drivers:tools-poly/build.sml(Poly/ML, usingHOLFileSys)tools/build/build.sml(mosml, usingOS.FileSys)Placed alongside the existing
bin/Holmakecheck, and following thesame shape: only fire if the executable is present and readable/
executable, so a not-yet-configured tree is unaffected. On a hit the
user gets the standard
check_againstwarning — "you should reconfigurethe system", Ctrl-C to abort or RETURN to continue — rather than a hard
failure.
Notes
diagnostic for a failure mode that currently manifests as confusing
downstream parse errors.
bin/unquoteabsent case is silently skipped rather than fatal,unlike the
bin/Holmakecheck which dies — a missing quote filteris not this check's business to diagnose.