Check every worksheet and solution on each push - #3
Merged
Conversation
etc/check.sh runs the twelve .pr through LPTP and holds each to the number of gaps it should have -- 35, 13, 12, 17, 10 and 13 for the worksheets, none for the solutions bar the one in worksheet 3 that cannot be closed. No error and no syntax error anywhere. It also compares each .tex against what its .pr writes, ignoring the first line, which LPTP rewrites to its own installation. That is the check that was missing: ws4_soln.tex had fallen 46 lines behind its proofs and still showed seventeen lemmas, so the PDF a reader opened was missing a property the worksheet asks for. Both failure modes were tried on purpose before this was committed, and both are caught. The workflow builds LPTP from source with GNU Prolog, runs the script, fails if the run leaves the tree dirty, and typesets all twelve documents in a second job. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
1 participant
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.
The repository had no CI, and the kind of thing that goes wrong here is
silent: a lemma that stops being checked, a property nobody proves, a PDF
that drifts away from the proof it was made from. All three happened, and
none of them announced itself.
What is checked
etc/check.shruns the twelve.prfiles through LPTP and holds each to thenumber of gaps it is supposed to have — 35, 13, 12, 17, 10 and 13 for the
worksheets, none for the solutions apart from the single deliberate one in
worksheet 3. Any
LPTP-ErrororLPTP-Syntaxfails the run. The lattermatters: a syntax error makes LPTP skip a lemma with a one-line warning
that is easy to lose among the gap warnings, which is exactly how worksheet
1's opening lemma went unchecked.
It then compares each
.texagainst what its.practually writes, ignoringthe first line, which LPTP rewrites to the absolute path of its own
installation. This is the check that was missing:
ws4_soln.texhad fallen46 lines behind its proofs and still showed seventeen lemmas.
Both failure modes were induced on purpose before this was committed — a
.texwith twenty lines cut out, and a deliberately wrong gap count — andboth are caught with a message naming the file.
The script is meant to be run by hand too:
The workflow
Two jobs.
proofsinstalls GNU Prolog, clones and builds LPTP from source,runs the script, and then fails if the run left the working tree dirty —
check.shputs back every.texit regenerates, so anything remaining is afile that should not have moved.
typesettingruns plain TeX twice over alltwelve documents and insists on a DVI from each.
Verified locally against an LPTP built exactly as the workflow builds it:
twelve files, all counts as expected, no error, tree clean afterwards.
🤖 Generated with Claude Code