|
| 1 | +#!/usr/bin/env bash |
| 2 | +# Build arxiv.tex and zip everything arXiv needs to compile it (pdfLaTeX). |
| 3 | +set -euo pipefail |
| 4 | + |
| 5 | +ROOT="$(cd "$(dirname "$0")/.." && pwd)" |
| 6 | +cd "$ROOT" |
| 7 | + |
| 8 | +TEX="arxiv.tex" |
| 9 | +LISTINGS_DIR="lean-listings" |
| 10 | +FIGURES_DIR="figures" |
| 11 | +OUT_DIR="dist" |
| 12 | +ZIP="${OUT_DIR}/arxiv_submit.zip" |
| 13 | + |
| 14 | +echo "==> Regenerating arxiv_with_code.md, arxiv.tex, listings, and figures" |
| 15 | +bash scripts/build_arxiv_tex.sh |
| 16 | + |
| 17 | +missing=0 |
| 18 | +if [[ ! -f "$TEX" ]]; then |
| 19 | + echo "error: missing $TEX" >&2 |
| 20 | + missing=1 |
| 21 | +fi |
| 22 | +if [[ ! -d "$LISTINGS_DIR" ]]; then |
| 23 | + echo "error: missing $LISTINGS_DIR" >&2 |
| 24 | + missing=1 |
| 25 | +fi |
| 26 | +lean_count="$(find "$LISTINGS_DIR" -maxdepth 1 -type f 2>/dev/null | wc -l)" |
| 27 | +if [[ "$lean_count" -eq 0 ]]; then |
| 28 | + echo "error: no listing files in $LISTINGS_DIR" >&2 |
| 29 | + missing=1 |
| 30 | +fi |
| 31 | +fig_count="$(find "$FIGURES_DIR" -maxdepth 1 -name '*.pdf' 2>/dev/null | wc -l)" |
| 32 | +if [[ "$fig_count" -eq 0 ]]; then |
| 33 | + echo "error: no mermaid figure PDFs in $FIGURES_DIR" >&2 |
| 34 | + missing=1 |
| 35 | +fi |
| 36 | +if [[ "$missing" -ne 0 ]]; then |
| 37 | + exit 1 |
| 38 | +fi |
| 39 | + |
| 40 | +mkdir -p "$OUT_DIR" |
| 41 | +rm -f "$ZIP" |
| 42 | + |
| 43 | +echo "==> Writing 00README.json (mark listing files as include so arXiv does not drop them)" |
| 44 | +python3 - <<'PY' |
| 45 | +import json |
| 46 | +from pathlib import Path |
| 47 | +
|
| 48 | +sources = [{"filename": "arxiv.tex", "usage": "toplevel"}] |
| 49 | +for path in sorted(p for p in Path("lean-listings").iterdir() if p.is_file()): |
| 50 | + sources.append({"filename": path.as_posix(), "usage": "include"}) |
| 51 | +for path in sorted(Path("figures").glob("*.pdf")): |
| 52 | + sources.append({"filename": path.as_posix(), "usage": "include"}) |
| 53 | +readme = {"process": {"compiler": "pdflatex"}, "sources": sources} |
| 54 | +Path("00README.json").write_text(json.dumps(readme, indent=2) + "\n") |
| 55 | +print(f" {len(sources)} sources") |
| 56 | +PY |
| 57 | + |
| 58 | +echo "==> Packaging" |
| 59 | +zip -r "$ZIP" \ |
| 60 | + 00README.json \ |
| 61 | + "$TEX" \ |
| 62 | + "$LISTINGS_DIR" \ |
| 63 | + "$FIGURES_DIR"/*.pdf |
| 64 | + |
| 65 | +echo "wrote $ZIP ($(du -h "$ZIP" | cut -f1))" |
| 66 | +echo "Contents:" |
| 67 | +zipinfo -1 "$ZIP" | sed 's/^/ /' | head -40 |
| 68 | +echo |
| 69 | +echo "Upload $ZIP to arXiv (pdfLaTeX; UTF-8 Lean listings render via the listings literate" |
| 70 | +echo "table; mermaid diagrams ship as pre-rendered figures/*.pdf since AutoTeX cannot run mmdc)." |
| 71 | +echo "On arXiv Add Files: Delete All before uploading (uploads merge, they do not replace)." |
| 72 | +echo "On arXiv Review Files: if any lean-listings/*.lean or figures/*.pdf are marked for" |
| 73 | +echo "deletion, UNCHECK them." |
0 commit comments