Stratified Universality

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 #!/usr/bin/env python3
2 """Compile the three final documents without rewriting inherited evidence."""
3 from pathlib import Path
4 import argparse
5 import shutil
6 import subprocess
7 import sys
8 
9 ROOT = Path(__file__).resolve().parent
10 DOCUMENTS = (
11     ("traditional", "Stratified_Universality_Traditional.tex"),
12     ("visual", "Stratified_Universality_Visual_Guide.tex"),
13     ("lean", "Stratified_Universality_Lean_Guide.tex"),
14 )
15 
16 def main():
17     parser = argparse.ArgumentParser(description=__doc__)
18     parser.add_argument("--document", choices=["all", "traditional", "visual", "lean"], default="all")
19     args = parser.parse_args()
20     tex = shutil.which("pdflatex")
21     if tex is None:
22         raise SystemExit("pdflatex is required; install the documented TeX dependencies first.")
23     logs = ROOT / "build_logs"
24     logs.mkdir(exist_ok=True)
25     for folder, name in DOCUMENTS:
26         if args.document not in ("all", folder):
27             continue
28         source = ROOT / folder / name
29         if not source.is_file():
30             raise SystemExit(f"Missing final document source: {source}")
31         for run in range(1, 4):
32             with (logs / f"{source.stem}_pass{run}.txt").open("wb") as log:
33                 result = subprocess.run(
34                     [tex, "-interaction=nonstopmode", "-halt-on-error", "-file-line-error", name],
35                     cwd=source.parent, stdout=log, stderr=subprocess.STDOUT,
36                 )
37             if result.returncode:
38                 raise SystemExit(f"Build failed for {name}, pass {run}; inspect build_logs.")
39         print(f"Built {folder}/{source.stem}.pdf")
40     print("Document compilation does not rerun Python regression suites or certify Lean proofs.")
41 
42 if __name__ == "__main__":
43     main()

Back to source controls

Back to Stratified Universality