mirror of
https://github.com/saymrwulf/verifying-crypto-with-lean.git
synced 2026-09-03 19:53:45 +00:00
build: the book compiles on this Ubuntu — tectonic + dual-engine preamble
No root available here, so the toolchain is tectonic (single user-space binary, packages fetched on demand). The preamble unicode block is now dual-engine: pdfTeX keeps its DeclareUnicodeCharacter list, XeTeX gets a newunicodechar twin generated from the same 37 mappings — both branches must stay green (Mac pdflatex, Ubuntu tectonic). build.sh is the one command. The committed PDF is current for the first time since July 6: 116 pages, ch13 + the live-log section finally in print. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
62d12dc3fa
commit
f0088a317e
3 changed files with 99 additions and 37 deletions
16
build.sh
Executable file
16
build.sh
Executable file
|
|
@ -0,0 +1,16 @@
|
|||
#!/usr/bin/env bash
|
||||
# Build the book. No root, no TeX Live install: tectonic is a single
|
||||
# user-space binary that fetches packages on demand (first run is slow,
|
||||
# after that it's seconds). pdflatex also works (the preamble carries a
|
||||
# dual-engine unicode block); tectonic is what the repo's button uses.
|
||||
set -euo pipefail
|
||||
cd "$(dirname "$0")"
|
||||
TECTONIC="${TECTONIC:-$HOME/.local/bin/tectonic}"
|
||||
if [ ! -x "$TECTONIC" ] && command -v tectonic >/dev/null; then TECTONIC=tectonic; fi
|
||||
[ -x "$TECTONIC" ] || command -v "$TECTONIC" >/dev/null || {
|
||||
echo "no tectonic. Install (no root):"
|
||||
echo " curl -sL https://github.com/tectonic-typesetting/tectonic/releases/download/tectonic%400.15.0/tectonic-0.15.0-x86_64-unknown-linux-musl.tar.gz | tar xz -C ~/.local/bin"
|
||||
exit 1
|
||||
}
|
||||
"$TECTONIC" -X compile main.tex
|
||||
pdfinfo main.pdf 2>/dev/null | grep Pages || true
|
||||
BIN
main.pdf
BIN
main.pdf
Binary file not shown.
120
preamble.tex
120
preamble.tex
|
|
@ -109,43 +109,89 @@
|
|||
\newcommand{\lean}[1]{\inlinecode{#1}}
|
||||
\newcommand{\rust}[1]{\inlinecode{#1}}
|
||||
\newcommand{\code}[1]{\inlinecode{#1}}
|
||||
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}} % →
|
||||
\DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}} % ←
|
||||
\DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
|
||||
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} % ∀
|
||||
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} % ∃
|
||||
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}} % ∧
|
||||
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}} % ∨
|
||||
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}} % ¬
|
||||
\DeclareUnicodeCharacter{2260}{\ensuremath{\neq}} % ≠
|
||||
\DeclareUnicodeCharacter{2264}{\ensuremath{\leq}} % ≤
|
||||
\DeclareUnicodeCharacter{2265}{\ensuremath{\geq}} % ≥
|
||||
\DeclareUnicodeCharacter{22A2}{\ensuremath{\vdash}} % ⊢
|
||||
\DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}} % ·
|
||||
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} % ℕ
|
||||
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}} % ℤ
|
||||
\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} % ℓ
|
||||
\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}} % ×
|
||||
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}} % ∈
|
||||
\DeclareUnicodeCharacter{2211}{\ensuremath{\Sigma}} % ∑
|
||||
\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} % ≡
|
||||
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}} % ∣
|
||||
\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}} % ⟨
|
||||
\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}} % ⟩
|
||||
\DeclareUnicodeCharacter{1D53D}{\ensuremath{\mathbb{F}}} % 𝔽
|
||||
\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}} % ₀
|
||||
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}} % ₁
|
||||
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}} % ₂
|
||||
\DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}} % ²
|
||||
\DeclareUnicodeCharacter{2075}{\ensuremath{{}^5}} % ⁵
|
||||
\DeclareUnicodeCharacter{2713}{\ensuremath{\checkmark}} % ✓
|
||||
\DeclareUnicodeCharacter{2717}{\ensuremath{\times}} % ✗
|
||||
\DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}} % ⁻
|
||||
\DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}} % ¹
|
||||
\DeclareUnicodeCharacter{00B3}{\ensuremath{{}^{3}}} % ³
|
||||
\DeclareUnicodeCharacter{2070}{\ensuremath{{}^{0}}} % ⁰
|
||||
\DeclareUnicodeCharacter{2074}{\ensuremath{{}^{4}}} % ⁴
|
||||
\DeclareUnicodeCharacter{2076}{\ensuremath{{}^{6}}} % ⁶
|
||||
% Unicode in Lean listings, both engines. pdfTeX maps code points via
|
||||
% inputenc; XeTeX/Tectonic is natively Unicode but the tt font lacks the
|
||||
% glyphs, so newunicodechar substitutes the same math forms. BOTH branches
|
||||
% derive from one list — edit both or the engines diverge (the build button
|
||||
% compiles under tectonic, the Mac under pdflatex; both must stay green).
|
||||
\ifdefined\XeTeXversion
|
||||
\usepackage{newunicodechar}
|
||||
\newunicodechar{→}{\ensuremath{\to}} % →
|
||||
\newunicodechar{←}{\ensuremath{\leftarrow}} % ←
|
||||
\newunicodechar{↔}{\ensuremath{\leftrightarrow}} % ↔
|
||||
\newunicodechar{∀}{\ensuremath{\forall}} % ∀
|
||||
\newunicodechar{∃}{\ensuremath{\exists}} % ∃
|
||||
\newunicodechar{∧}{\ensuremath{\wedge}} % ∧
|
||||
\newunicodechar{∨}{\ensuremath{\vee}} % ∨
|
||||
\newunicodechar{¬}{\ensuremath{\neg}} % ¬
|
||||
\newunicodechar{≠}{\ensuremath{\neq}} % ≠
|
||||
\newunicodechar{≤}{\ensuremath{\leq}} % ≤
|
||||
\newunicodechar{≥}{\ensuremath{\geq}} % ≥
|
||||
\newunicodechar{⊢}{\ensuremath{\vdash}} % ⊢
|
||||
\newunicodechar{·}{\ensuremath{\cdot}} % ·
|
||||
\newunicodechar{ℕ}{\ensuremath{\mathbb{N}}} % ℕ
|
||||
\newunicodechar{ℤ}{\ensuremath{\mathbb{Z}}} % ℤ
|
||||
\newunicodechar{ℓ}{\ensuremath{\ell}} % ℓ
|
||||
\newunicodechar{×}{\ensuremath{\times}} % ×
|
||||
\newunicodechar{∈}{\ensuremath{\in}} % ∈
|
||||
\newunicodechar{∑}{\ensuremath{\Sigma}} % ∑
|
||||
\newunicodechar{≡}{\ensuremath{\equiv}} % ≡
|
||||
\newunicodechar{∣}{\ensuremath{\mid}} % ∣
|
||||
\newunicodechar{⟨}{\ensuremath{\langle}} % ⟨
|
||||
\newunicodechar{⟩}{\ensuremath{\rangle}} % ⟩
|
||||
\newunicodechar{𝔽}{\ensuremath{\mathbb{F}}} % 𝔽
|
||||
\newunicodechar{₀}{\ensuremath{{}_0}} % ₀
|
||||
\newunicodechar{₁}{\ensuremath{{}_1}} % ₁
|
||||
\newunicodechar{₂}{\ensuremath{{}_2}} % ₂
|
||||
\newunicodechar{²}{\ensuremath{{}^2}} % ²
|
||||
\newunicodechar{⁵}{\ensuremath{{}^5}} % ⁵
|
||||
\newunicodechar{✓}{\ensuremath{\checkmark}} % ✓
|
||||
\newunicodechar{✗}{\ensuremath{\times}} % ✗
|
||||
\newunicodechar{⁻}{\ensuremath{{}^{-}}} % ⁻
|
||||
\newunicodechar{¹}{\ensuremath{{}^{1}}} % ¹
|
||||
\newunicodechar{³}{\ensuremath{{}^{3}}} % ³
|
||||
\newunicodechar{⁰}{\ensuremath{{}^{0}}} % ⁰
|
||||
\newunicodechar{⁴}{\ensuremath{{}^{4}}} % ⁴
|
||||
\newunicodechar{⁶}{\ensuremath{{}^{6}}} % ⁶
|
||||
\else
|
||||
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}} % →
|
||||
\DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}} % ←
|
||||
\DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
|
||||
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} % ∀
|
||||
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} % ∃
|
||||
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}} % ∧
|
||||
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}} % ∨
|
||||
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}} % ¬
|
||||
\DeclareUnicodeCharacter{2260}{\ensuremath{\neq}} % ≠
|
||||
\DeclareUnicodeCharacter{2264}{\ensuremath{\leq}} % ≤
|
||||
\DeclareUnicodeCharacter{2265}{\ensuremath{\geq}} % ≥
|
||||
\DeclareUnicodeCharacter{22A2}{\ensuremath{\vdash}} % ⊢
|
||||
\DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}} % ·
|
||||
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} % ℕ
|
||||
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}} % ℤ
|
||||
\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} % ℓ
|
||||
\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}} % ×
|
||||
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}} % ∈
|
||||
\DeclareUnicodeCharacter{2211}{\ensuremath{\Sigma}} % ∑
|
||||
\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} % ≡
|
||||
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}} % ∣
|
||||
\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}} % ⟨
|
||||
\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}} % ⟩
|
||||
\DeclareUnicodeCharacter{1D53D}{\ensuremath{\mathbb{F}}} % 𝔽
|
||||
\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}} % ₀
|
||||
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}} % ₁
|
||||
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}} % ₂
|
||||
\DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}} % ²
|
||||
\DeclareUnicodeCharacter{2075}{\ensuremath{{}^5}} % ⁵
|
||||
\DeclareUnicodeCharacter{2713}{\ensuremath{\checkmark}} % ✓
|
||||
\DeclareUnicodeCharacter{2717}{\ensuremath{\times}} % ✗
|
||||
\DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}} % ⁻
|
||||
\DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}} % ¹
|
||||
\DeclareUnicodeCharacter{00B3}{\ensuremath{{}^{3}}} % ³
|
||||
\DeclareUnicodeCharacter{2070}{\ensuremath{{}^{0}}} % ⁰
|
||||
\DeclareUnicodeCharacter{2074}{\ensuremath{{}^{4}}} % ⁴
|
||||
\DeclareUnicodeCharacter{2076}{\ensuremath{{}^{6}}} % ⁶
|
||||
\fi
|
||||
|
||||
% ---- pedagogical boxes: each means ONE thing ----------------------------
|
||||
% BIG IDEA — the load-bearing concept of a section.
|
||||
|
|
|
|||
Loading…
Reference in a new issue