diff --git a/build.sh b/build.sh new file mode 100755 index 0000000..450168d --- /dev/null +++ b/build.sh @@ -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 diff --git a/main.pdf b/main.pdf index cf893c2..599a1ed 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/preamble.tex b/preamble.tex index 99b7383..3a70fd7 100644 --- a/preamble.tex +++ b/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.