Merge branch 'blueprint'

loganrjmurphy · May 28, 2024 · 596e098 · 596e098
2 parents e24f851 + 1c059ad
commit 596e098
Show file tree

Hide file tree

Showing 176 changed files with 348 additions and 94 deletions.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -0,0 +1,89 @@
+on:
+  push:
+    branches:
+      - master
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
+
+      - name: Get cache
+        run: ~/.elan/bin/lake exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake build Book
+
+      - name: Cache mathlib docs
+        uses: actions/cache@v3
+        with:
+          path: |
+            .lake/build/doc/Init
+            .lake/build/doc/Lake
+            .lake/build/doc/Lean
+            .lake/build/doc/Std
+            .lake/build/doc/Mathlib
+            .lake/build/doc/declarations
+            !.lake/build/doc/declarations/declaration-data-Book*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -R -Kenv=dev build Book:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            mkdir docs
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      - name: Check declarations
+        run: |
+            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Move documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs
+
+      - name: Upload docs & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: |
+          mv docs/docs .lake/build/doc
diff --git a/blueprint/requirements.txt → blueprint-old/requirements.txt b/blueprint/requirements.txt → blueprint-old/requirements.txt
diff --git a/blueprint/src/common_notions.tex → blueprint-old/src/common_notions.tex b/blueprint/src/common_notions.tex → blueprint-old/src/common_notions.tex
diff --git a/blueprint/src/definitions.tex → blueprint-old/src/definitions.tex b/blueprint/src/definitions.tex → blueprint-old/src/definitions.tex
diff --git a/blueprint-old/src/extra_styles.css b/blueprint-old/src/extra_styles.css
@@ -0,0 +1,53 @@
+div.theorem_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.proposition_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.lemma_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.corollary_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.proof_content {
+	border-left: .08rem solid grey;
+}
+
+figure.subfloat span.subref {
+	display: none;
+}
+
+nav.local_toc ul {
+	font-size: 1.2rem;
+}
+
+@media (min-width:1024px) {
+    nav.toc {
+        width: 25vw;
+    }
+}
+
+@media (min-width:1024px) {
+    div.with-toc {
+        margin-left:25vw;
+    }
+}
+
+@font-face {
+  font-family: 'Open Sans';
+  font-style: normal;
+  font-weight: 400;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(https://fonts.gstatic.com/s/opensans/v29/memSYaGs126MiZpBA-UvWbX2vVnXBbObj2OVZyOOSr4dVJWUgsjZ0B4gaVI.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+2000-206F, U+2074, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+
+body, h1, h2, h3, h4, h5, h6, p, text {
+  font-family: "Open Sans", "Helvetica Neue", Helvetica, Arial, sans-serif !important;
+}
diff --git a/blueprint/src/figures/fig01e.eps → blueprint-old/src/figures/fig01e.eps b/blueprint/src/figures/fig01e.eps → blueprint-old/src/figures/fig01e.eps
diff --git a/blueprint/src/figures/fig01g.eps → blueprint-old/src/figures/fig01g.eps b/blueprint/src/figures/fig01g.eps → blueprint-old/src/figures/fig01g.eps
diff --git a/blueprint/src/figures/fig02e.eps → blueprint-old/src/figures/fig02e.eps b/blueprint/src/figures/fig02e.eps → blueprint-old/src/figures/fig02e.eps
diff --git a/blueprint/src/figures/fig02g.eps → blueprint-old/src/figures/fig02g.eps b/blueprint/src/figures/fig02g.eps → blueprint-old/src/figures/fig02g.eps
diff --git a/blueprint/src/figures/fig03e.eps → blueprint-old/src/figures/fig03e.eps b/blueprint/src/figures/fig03e.eps → blueprint-old/src/figures/fig03e.eps
diff --git a/blueprint/src/figures/fig03g.eps → blueprint-old/src/figures/fig03g.eps b/blueprint/src/figures/fig03g.eps → blueprint-old/src/figures/fig03g.eps
diff --git a/blueprint/src/figures/fig04e.eps → blueprint-old/src/figures/fig04e.eps b/blueprint/src/figures/fig04e.eps → blueprint-old/src/figures/fig04e.eps
diff --git a/blueprint/src/figures/fig04g.eps → blueprint-old/src/figures/fig04g.eps b/blueprint/src/figures/fig04g.eps → blueprint-old/src/figures/fig04g.eps
diff --git a/blueprint/src/figures/fig05e.eps → blueprint-old/src/figures/fig05e.eps b/blueprint/src/figures/fig05e.eps → blueprint-old/src/figures/fig05e.eps
diff --git a/blueprint/src/figures/fig05g.eps → blueprint-old/src/figures/fig05g.eps b/blueprint/src/figures/fig05g.eps → blueprint-old/src/figures/fig05g.eps
diff --git a/blueprint/src/figures/fig06e.eps → blueprint-old/src/figures/fig06e.eps b/blueprint/src/figures/fig06e.eps → blueprint-old/src/figures/fig06e.eps
diff --git a/blueprint/src/figures/fig06g.eps → blueprint-old/src/figures/fig06g.eps b/blueprint/src/figures/fig06g.eps → blueprint-old/src/figures/fig06g.eps
diff --git a/blueprint/src/figures/fig07e.eps → blueprint-old/src/figures/fig07e.eps b/blueprint/src/figures/fig07e.eps → blueprint-old/src/figures/fig07e.eps
diff --git a/blueprint/src/figures/fig07g.eps → blueprint-old/src/figures/fig07g.eps b/blueprint/src/figures/fig07g.eps → blueprint-old/src/figures/fig07g.eps
diff --git a/blueprint/src/figures/fig08e.eps → blueprint-old/src/figures/fig08e.eps b/blueprint/src/figures/fig08e.eps → blueprint-old/src/figures/fig08e.eps
diff --git a/blueprint/src/figures/fig08g.eps → blueprint-old/src/figures/fig08g.eps b/blueprint/src/figures/fig08g.eps → blueprint-old/src/figures/fig08g.eps
diff --git a/blueprint/src/figures/fig09e.eps → blueprint-old/src/figures/fig09e.eps b/blueprint/src/figures/fig09e.eps → blueprint-old/src/figures/fig09e.eps
diff --git a/blueprint/src/figures/fig09g.eps → blueprint-old/src/figures/fig09g.eps b/blueprint/src/figures/fig09g.eps → blueprint-old/src/figures/fig09g.eps
diff --git a/blueprint/src/figures/fig10e.eps → blueprint-old/src/figures/fig10e.eps b/blueprint/src/figures/fig10e.eps → blueprint-old/src/figures/fig10e.eps
diff --git a/blueprint/src/figures/fig10g.eps → blueprint-old/src/figures/fig10g.eps b/blueprint/src/figures/fig10g.eps → blueprint-old/src/figures/fig10g.eps
diff --git a/blueprint/src/figures/fig11e.eps → blueprint-old/src/figures/fig11e.eps b/blueprint/src/figures/fig11e.eps → blueprint-old/src/figures/fig11e.eps
diff --git a/blueprint/src/figures/fig11g.eps → blueprint-old/src/figures/fig11g.eps b/blueprint/src/figures/fig11g.eps → blueprint-old/src/figures/fig11g.eps
diff --git a/blueprint/src/figures/fig12e.eps → blueprint-old/src/figures/fig12e.eps b/blueprint/src/figures/fig12e.eps → blueprint-old/src/figures/fig12e.eps
diff --git a/blueprint/src/figures/fig12g.eps → blueprint-old/src/figures/fig12g.eps b/blueprint/src/figures/fig12g.eps → blueprint-old/src/figures/fig12g.eps
diff --git a/blueprint/src/figures/fig13e.eps → blueprint-old/src/figures/fig13e.eps b/blueprint/src/figures/fig13e.eps → blueprint-old/src/figures/fig13e.eps
diff --git a/blueprint/src/figures/fig13g.eps → blueprint-old/src/figures/fig13g.eps b/blueprint/src/figures/fig13g.eps → blueprint-old/src/figures/fig13g.eps
diff --git a/blueprint/src/figures/fig14e.eps → blueprint-old/src/figures/fig14e.eps b/blueprint/src/figures/fig14e.eps → blueprint-old/src/figures/fig14e.eps
diff --git a/blueprint/src/figures/fig14g.eps → blueprint-old/src/figures/fig14g.eps b/blueprint/src/figures/fig14g.eps → blueprint-old/src/figures/fig14g.eps
diff --git a/blueprint/src/figures/fig15e.eps → blueprint-old/src/figures/fig15e.eps b/blueprint/src/figures/fig15e.eps → blueprint-old/src/figures/fig15e.eps
diff --git a/blueprint/src/figures/fig15g.eps → blueprint-old/src/figures/fig15g.eps b/blueprint/src/figures/fig15g.eps → blueprint-old/src/figures/fig15g.eps
diff --git a/blueprint/src/figures/fig16e.eps → blueprint-old/src/figures/fig16e.eps b/blueprint/src/figures/fig16e.eps → blueprint-old/src/figures/fig16e.eps
diff --git a/blueprint/src/figures/fig16g.eps → blueprint-old/src/figures/fig16g.eps b/blueprint/src/figures/fig16g.eps → blueprint-old/src/figures/fig16g.eps
diff --git a/blueprint/src/figures/fig17e.eps → blueprint-old/src/figures/fig17e.eps b/blueprint/src/figures/fig17e.eps → blueprint-old/src/figures/fig17e.eps
diff --git a/blueprint/src/figures/fig17g.eps → blueprint-old/src/figures/fig17g.eps b/blueprint/src/figures/fig17g.eps → blueprint-old/src/figures/fig17g.eps
diff --git a/blueprint/src/figures/fig18e.eps → blueprint-old/src/figures/fig18e.eps b/blueprint/src/figures/fig18e.eps → blueprint-old/src/figures/fig18e.eps
diff --git a/blueprint/src/figures/fig18g.eps → blueprint-old/src/figures/fig18g.eps b/blueprint/src/figures/fig18g.eps → blueprint-old/src/figures/fig18g.eps
diff --git a/blueprint/src/figures/fig19e.eps → blueprint-old/src/figures/fig19e.eps b/blueprint/src/figures/fig19e.eps → blueprint-old/src/figures/fig19e.eps
diff --git a/blueprint/src/figures/fig19g.eps → blueprint-old/src/figures/fig19g.eps b/blueprint/src/figures/fig19g.eps → blueprint-old/src/figures/fig19g.eps
diff --git a/blueprint/src/figures/fig20e.eps → blueprint-old/src/figures/fig20e.eps b/blueprint/src/figures/fig20e.eps → blueprint-old/src/figures/fig20e.eps
diff --git a/blueprint/src/figures/fig20g.eps → blueprint-old/src/figures/fig20g.eps b/blueprint/src/figures/fig20g.eps → blueprint-old/src/figures/fig20g.eps
diff --git a/blueprint/src/figures/fig21e.eps → blueprint-old/src/figures/fig21e.eps b/blueprint/src/figures/fig21e.eps → blueprint-old/src/figures/fig21e.eps
diff --git a/blueprint/src/figures/fig21g.eps → blueprint-old/src/figures/fig21g.eps b/blueprint/src/figures/fig21g.eps → blueprint-old/src/figures/fig21g.eps
diff --git a/blueprint/src/figures/fig22e.eps → blueprint-old/src/figures/fig22e.eps b/blueprint/src/figures/fig22e.eps → blueprint-old/src/figures/fig22e.eps
diff --git a/blueprint/src/figures/fig22g.eps → blueprint-old/src/figures/fig22g.eps b/blueprint/src/figures/fig22g.eps → blueprint-old/src/figures/fig22g.eps
diff --git a/blueprint/src/figures/fig23e.eps → blueprint-old/src/figures/fig23e.eps b/blueprint/src/figures/fig23e.eps → blueprint-old/src/figures/fig23e.eps
diff --git a/blueprint/src/figures/fig23g.eps → blueprint-old/src/figures/fig23g.eps b/blueprint/src/figures/fig23g.eps → blueprint-old/src/figures/fig23g.eps
diff --git a/blueprint/src/figures/fig24e.eps → blueprint-old/src/figures/fig24e.eps b/blueprint/src/figures/fig24e.eps → blueprint-old/src/figures/fig24e.eps
diff --git a/blueprint/src/figures/fig24g.eps → blueprint-old/src/figures/fig24g.eps b/blueprint/src/figures/fig24g.eps → blueprint-old/src/figures/fig24g.eps
diff --git a/blueprint/src/figures/fig25e.eps → blueprint-old/src/figures/fig25e.eps b/blueprint/src/figures/fig25e.eps → blueprint-old/src/figures/fig25e.eps
diff --git a/blueprint/src/figures/fig25g.eps → blueprint-old/src/figures/fig25g.eps b/blueprint/src/figures/fig25g.eps → blueprint-old/src/figures/fig25g.eps
diff --git a/blueprint/src/figures/fig26e.eps → blueprint-old/src/figures/fig26e.eps b/blueprint/src/figures/fig26e.eps → blueprint-old/src/figures/fig26e.eps
diff --git a/blueprint/src/figures/fig26g.eps → blueprint-old/src/figures/fig26g.eps b/blueprint/src/figures/fig26g.eps → blueprint-old/src/figures/fig26g.eps
diff --git a/blueprint/src/figures/fig27e.eps → blueprint-old/src/figures/fig27e.eps b/blueprint/src/figures/fig27e.eps → blueprint-old/src/figures/fig27e.eps
diff --git a/blueprint/src/figures/fig27g.eps → blueprint-old/src/figures/fig27g.eps b/blueprint/src/figures/fig27g.eps → blueprint-old/src/figures/fig27g.eps
diff --git a/blueprint/src/figures/fig28e.eps → blueprint-old/src/figures/fig28e.eps b/blueprint/src/figures/fig28e.eps → blueprint-old/src/figures/fig28e.eps
diff --git a/blueprint/src/figures/fig28g.eps → blueprint-old/src/figures/fig28g.eps b/blueprint/src/figures/fig28g.eps → blueprint-old/src/figures/fig28g.eps
diff --git a/blueprint/src/figures/fig30e.eps → blueprint-old/src/figures/fig30e.eps b/blueprint/src/figures/fig30e.eps → blueprint-old/src/figures/fig30e.eps
diff --git a/blueprint/src/figures/fig30g.eps → blueprint-old/src/figures/fig30g.eps b/blueprint/src/figures/fig30g.eps → blueprint-old/src/figures/fig30g.eps
diff --git a/blueprint/src/figures/fig31e.eps → blueprint-old/src/figures/fig31e.eps b/blueprint/src/figures/fig31e.eps → blueprint-old/src/figures/fig31e.eps
diff --git a/blueprint/src/figures/fig31g.eps → blueprint-old/src/figures/fig31g.eps b/blueprint/src/figures/fig31g.eps → blueprint-old/src/figures/fig31g.eps
diff --git a/blueprint/src/figures/fig32e.eps → blueprint-old/src/figures/fig32e.eps b/blueprint/src/figures/fig32e.eps → blueprint-old/src/figures/fig32e.eps
diff --git a/blueprint/src/figures/fig32g.eps → blueprint-old/src/figures/fig32g.eps b/blueprint/src/figures/fig32g.eps → blueprint-old/src/figures/fig32g.eps
diff --git a/blueprint/src/figures/fig33e.eps → blueprint-old/src/figures/fig33e.eps b/blueprint/src/figures/fig33e.eps → blueprint-old/src/figures/fig33e.eps
diff --git a/blueprint/src/figures/fig33g.eps → blueprint-old/src/figures/fig33g.eps b/blueprint/src/figures/fig33g.eps → blueprint-old/src/figures/fig33g.eps
diff --git a/blueprint/src/figures/fig34e.eps → blueprint-old/src/figures/fig34e.eps b/blueprint/src/figures/fig34e.eps → blueprint-old/src/figures/fig34e.eps
diff --git a/blueprint/src/figures/fig34g.eps → blueprint-old/src/figures/fig34g.eps b/blueprint/src/figures/fig34g.eps → blueprint-old/src/figures/fig34g.eps
diff --git a/blueprint/src/figures/fig35e.eps → blueprint-old/src/figures/fig35e.eps b/blueprint/src/figures/fig35e.eps → blueprint-old/src/figures/fig35e.eps
diff --git a/blueprint/src/figures/fig35g.eps → blueprint-old/src/figures/fig35g.eps b/blueprint/src/figures/fig35g.eps → blueprint-old/src/figures/fig35g.eps
diff --git a/blueprint/src/figures/fig36e.eps → blueprint-old/src/figures/fig36e.eps b/blueprint/src/figures/fig36e.eps → blueprint-old/src/figures/fig36e.eps
diff --git a/blueprint/src/figures/fig36g.eps → blueprint-old/src/figures/fig36g.eps b/blueprint/src/figures/fig36g.eps → blueprint-old/src/figures/fig36g.eps
diff --git a/blueprint/src/figures/fig37e.eps → blueprint-old/src/figures/fig37e.eps b/blueprint/src/figures/fig37e.eps → blueprint-old/src/figures/fig37e.eps
diff --git a/blueprint/src/figures/fig37g.eps → blueprint-old/src/figures/fig37g.eps b/blueprint/src/figures/fig37g.eps → blueprint-old/src/figures/fig37g.eps
diff --git a/blueprint/src/figures/fig38e.eps → blueprint-old/src/figures/fig38e.eps b/blueprint/src/figures/fig38e.eps → blueprint-old/src/figures/fig38e.eps
diff --git a/blueprint/src/figures/fig38g.eps → blueprint-old/src/figures/fig38g.eps b/blueprint/src/figures/fig38g.eps → blueprint-old/src/figures/fig38g.eps
diff --git a/blueprint/src/figures/fig39e.eps → blueprint-old/src/figures/fig39e.eps b/blueprint/src/figures/fig39e.eps → blueprint-old/src/figures/fig39e.eps
diff --git a/blueprint/src/figures/fig39g.eps → blueprint-old/src/figures/fig39g.eps b/blueprint/src/figures/fig39g.eps → blueprint-old/src/figures/fig39g.eps
diff --git a/blueprint/src/figures/fig40e.eps → blueprint-old/src/figures/fig40e.eps b/blueprint/src/figures/fig40e.eps → blueprint-old/src/figures/fig40e.eps
diff --git a/blueprint/src/figures/fig40g.eps → blueprint-old/src/figures/fig40g.eps b/blueprint/src/figures/fig40g.eps → blueprint-old/src/figures/fig40g.eps
diff --git a/blueprint/src/figures/fig41e.eps → blueprint-old/src/figures/fig41e.eps b/blueprint/src/figures/fig41e.eps → blueprint-old/src/figures/fig41e.eps
diff --git a/blueprint/src/figures/fig41g.eps → blueprint-old/src/figures/fig41g.eps b/blueprint/src/figures/fig41g.eps → blueprint-old/src/figures/fig41g.eps
diff --git a/blueprint/src/figures/fig42e.eps → blueprint-old/src/figures/fig42e.eps b/blueprint/src/figures/fig42e.eps → blueprint-old/src/figures/fig42e.eps
diff --git a/blueprint/src/figures/fig42g.eps → blueprint-old/src/figures/fig42g.eps b/blueprint/src/figures/fig42g.eps → blueprint-old/src/figures/fig42g.eps
diff --git a/blueprint/src/figures/fig43e.eps → blueprint-old/src/figures/fig43e.eps b/blueprint/src/figures/fig43e.eps → blueprint-old/src/figures/fig43e.eps
diff --git a/blueprint/src/figures/fig43g.eps → blueprint-old/src/figures/fig43g.eps b/blueprint/src/figures/fig43g.eps → blueprint-old/src/figures/fig43g.eps
diff --git a/blueprint/src/figures/fig44e.eps → blueprint-old/src/figures/fig44e.eps b/blueprint/src/figures/fig44e.eps → blueprint-old/src/figures/fig44e.eps
diff --git a/blueprint/src/figures/fig44g.eps → blueprint-old/src/figures/fig44g.eps b/blueprint/src/figures/fig44g.eps → blueprint-old/src/figures/fig44g.eps
diff --git a/blueprint/src/figures/fig45e.eps → blueprint-old/src/figures/fig45e.eps b/blueprint/src/figures/fig45e.eps → blueprint-old/src/figures/fig45e.eps
diff --git a/blueprint/src/figures/fig45g.eps → blueprint-old/src/figures/fig45g.eps b/blueprint/src/figures/fig45g.eps → blueprint-old/src/figures/fig45g.eps
diff --git a/blueprint/src/figures/fig46e.eps → blueprint-old/src/figures/fig46e.eps b/blueprint/src/figures/fig46e.eps → blueprint-old/src/figures/fig46e.eps
diff --git a/blueprint/src/figures/fig46g.eps → blueprint-old/src/figures/fig46g.eps b/blueprint/src/figures/fig46g.eps → blueprint-old/src/figures/fig46g.eps
diff --git a/blueprint/src/figures/fig47e.eps → blueprint-old/src/figures/fig47e.eps b/blueprint/src/figures/fig47e.eps → blueprint-old/src/figures/fig47e.eps
diff --git a/blueprint/src/figures/fig47g.eps → blueprint-old/src/figures/fig47g.eps b/blueprint/src/figures/fig47g.eps → blueprint-old/src/figures/fig47g.eps
diff --git a/blueprint/src/figures/fig48e.eps → blueprint-old/src/figures/fig48e.eps b/blueprint/src/figures/fig48e.eps → blueprint-old/src/figures/fig48e.eps
diff --git a/blueprint/src/figures/fig48g.eps → blueprint-old/src/figures/fig48g.eps b/blueprint/src/figures/fig48g.eps → blueprint-old/src/figures/fig48g.eps
diff --git a/blueprint/src/figures/proposition_24.png → blueprint-old/src/figures/proposition_24.png b/blueprint/src/figures/proposition_24.png → blueprint-old/src/figures/proposition_24.png
diff --git a/blueprint/src/figures/proposition_7'''.png → ...rint-old/src/figures/proposition_7'''.png b/blueprint/src/figures/proposition_7'''.png → ...rint-old/src/figures/proposition_7'''.png
diff --git a/blueprint/src/figures/proposition_7''.png → ...print-old/src/figures/proposition_7''.png b/blueprint/src/figures/proposition_7''.png → ...print-old/src/figures/proposition_7''.png
diff --git a/blueprint/src/figures/proposition_7'.png → blueprint-old/src/figures/proposition_7'.png b/blueprint/src/figures/proposition_7'.png → blueprint-old/src/figures/proposition_7'.png
diff --git a/blueprint/src/figures/proposition_9.png → blueprint-old/src/figures/proposition_9.png b/blueprint/src/figures/proposition_9.png → blueprint-old/src/figures/proposition_9.png
diff --git a/blueprint/src/intro.tex → blueprint-old/src/intro.tex b/blueprint/src/intro.tex → blueprint-old/src/intro.tex
diff --git a/blueprint-old/src/latexmkrc b/blueprint-old/src/latexmkrc
@@ -0,0 +1,3 @@
+$pdf_mode = 1;
+$pdflatex = 'xelatex -synctex=1 -output-directory=../print/';
+@default_files = ('print.tex');
diff --git a/blueprint/src/main.tex → blueprint-old/src/main.tex b/blueprint/src/main.tex → blueprint-old/src/main.tex
diff --git a/blueprint-old/src/plastex.cfg b/blueprint-old/src/plastex.cfg
@@ -0,0 +1,17 @@
+[general]
+renderer=HTML5
+copy-theme-extras=yes
+plugins=leanblueprint
+
+[document]
+toc-depth=2
+toc-non-files=True
+
+[files]
+directory=../web/
+split-level=0
+
+[html5]
+localtoc-level=0
+extra-css=extra_styles.css
+mathjax-dollars=True
diff --git a/blueprint/src/postulates.tex → blueprint-old/src/postulates.tex b/blueprint/src/postulates.tex → blueprint-old/src/postulates.tex
diff --git a/blueprint/src/preamble/print.tex → blueprint-old/src/preamble/print.tex b/blueprint/src/preamble/print.tex → blueprint-old/src/preamble/print.tex
diff --git a/blueprint/src/preamble/web.tex → blueprint-old/src/preamble/web.tex b/blueprint/src/preamble/web.tex → blueprint-old/src/preamble/web.tex
diff --git a/blueprint-old/src/print.tex b/blueprint-old/src/print.tex
@@ -0,0 +1,36 @@
+% This file makes a printable version of the blueprint
+
+\documentclass[a4paper]{report}
+
+\usepackage[utf8]{inputenc}
+\usepackage[english]{babel}
+\usepackage{charter}
+\usepackage{fancyhdr}
+\usepackage{epsf}
+\usepackage[bookmarks=true]{hyperref}
+\usepackage[textwidth=14cm]{geometry}
+\usepackage{xfrac}
+\usepackage{polyglossia}
+\setdefaultlanguage{english}
+\usepackage{amsmath,amssymb}
+\usepackage{enumitem}
+\usepackage{tikz-cd}
+\usepackage{mathtools}
+\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
+\usepackage{fontspec}
+
+\usepackage[nameinlink, capitalize]{cleveref}
+
+\usepackage{amsthm}
+\usepackage{etexcmds}
+\usepackage{thmtools}
+
+\input{preamble/print}
+
+\title{The First Book of Euclid's Elements---Commentary and Lean Formalization}
+\author{Logan Murphy and Kaiyu Yang}
+
+\begin{document}
+\maketitle
+\input{main}
+\end{document}
diff --git a/blueprint/src/propositions/proposition_1.tex → ...nt-old/src/propositions/proposition_1.tex b/blueprint/src/propositions/proposition_1.tex → ...nt-old/src/propositions/proposition_1.tex
diff --git a/...print/src/propositions/proposition_10.tex → ...t-old/src/propositions/proposition_10.tex b/...print/src/propositions/proposition_10.tex → ...t-old/src/propositions/proposition_10.tex
diff --git a/...print/src/propositions/proposition_11.tex → ...t-old/src/propositions/proposition_11.tex b/...print/src/propositions/proposition_11.tex → ...t-old/src/propositions/proposition_11.tex
diff --git a/...print/src/propositions/proposition_12.tex → ...t-old/src/propositions/proposition_12.tex b/...print/src/propositions/proposition_12.tex → ...t-old/src/propositions/proposition_12.tex
diff --git a/...print/src/propositions/proposition_13.tex → ...t-old/src/propositions/proposition_13.tex b/...print/src/propositions/proposition_13.tex → ...t-old/src/propositions/proposition_13.tex
diff --git a/...print/src/propositions/proposition_14.tex → ...t-old/src/propositions/proposition_14.tex b/...print/src/propositions/proposition_14.tex → ...t-old/src/propositions/proposition_14.tex
diff --git a/...print/src/propositions/proposition_15.tex → ...t-old/src/propositions/proposition_15.tex b/...print/src/propositions/proposition_15.tex → ...t-old/src/propositions/proposition_15.tex
diff --git a/...print/src/propositions/proposition_16.tex → ...t-old/src/propositions/proposition_16.tex b/...print/src/propositions/proposition_16.tex → ...t-old/src/propositions/proposition_16.tex
diff --git a/...print/src/propositions/proposition_17.tex → ...t-old/src/propositions/proposition_17.tex b/...print/src/propositions/proposition_17.tex → ...t-old/src/propositions/proposition_17.tex
diff --git a/...print/src/propositions/proposition_18.tex → ...t-old/src/propositions/proposition_18.tex b/...print/src/propositions/proposition_18.tex → ...t-old/src/propositions/proposition_18.tex
diff --git a/...print/src/propositions/proposition_19.tex → ...t-old/src/propositions/proposition_19.tex b/...print/src/propositions/proposition_19.tex → ...t-old/src/propositions/proposition_19.tex
diff --git a/blueprint/src/propositions/proposition_2.tex → ...nt-old/src/propositions/proposition_2.tex b/blueprint/src/propositions/proposition_2.tex → ...nt-old/src/propositions/proposition_2.tex
diff --git a/...print/src/propositions/proposition_20.tex → ...t-old/src/propositions/proposition_20.tex b/...print/src/propositions/proposition_20.tex → ...t-old/src/propositions/proposition_20.tex
diff --git a/...print/src/propositions/proposition_21.tex → ...t-old/src/propositions/proposition_21.tex b/...print/src/propositions/proposition_21.tex → ...t-old/src/propositions/proposition_21.tex
diff --git a/...print/src/propositions/proposition_22.tex → ...t-old/src/propositions/proposition_22.tex b/...print/src/propositions/proposition_22.tex → ...t-old/src/propositions/proposition_22.tex
diff --git a/...print/src/propositions/proposition_23.tex → ...t-old/src/propositions/proposition_23.tex b/...print/src/propositions/proposition_23.tex → ...t-old/src/propositions/proposition_23.tex
diff --git a/...print/src/propositions/proposition_24.tex → ...t-old/src/propositions/proposition_24.tex b/...print/src/propositions/proposition_24.tex → ...t-old/src/propositions/proposition_24.tex
diff --git a/...print/src/propositions/proposition_25.tex → ...t-old/src/propositions/proposition_25.tex b/...print/src/propositions/proposition_25.tex → ...t-old/src/propositions/proposition_25.tex
diff --git a/...print/src/propositions/proposition_26.tex → ...t-old/src/propositions/proposition_26.tex b/...print/src/propositions/proposition_26.tex → ...t-old/src/propositions/proposition_26.tex
diff --git a/...print/src/propositions/proposition_27.tex → ...t-old/src/propositions/proposition_27.tex b/...print/src/propositions/proposition_27.tex → ...t-old/src/propositions/proposition_27.tex
diff --git a/...print/src/propositions/proposition_28.tex → ...t-old/src/propositions/proposition_28.tex b/...print/src/propositions/proposition_28.tex → ...t-old/src/propositions/proposition_28.tex
diff --git a/...print/src/propositions/proposition_29.tex → ...t-old/src/propositions/proposition_29.tex b/...print/src/propositions/proposition_29.tex → ...t-old/src/propositions/proposition_29.tex
diff --git a/blueprint/src/propositions/proposition_3.tex → ...nt-old/src/propositions/proposition_3.tex b/blueprint/src/propositions/proposition_3.tex → ...nt-old/src/propositions/proposition_3.tex
diff --git a/...print/src/propositions/proposition_30.tex → ...t-old/src/propositions/proposition_30.tex b/...print/src/propositions/proposition_30.tex → ...t-old/src/propositions/proposition_30.tex
diff --git a/...print/src/propositions/proposition_31.tex → ...t-old/src/propositions/proposition_31.tex b/...print/src/propositions/proposition_31.tex → ...t-old/src/propositions/proposition_31.tex
diff --git a/...print/src/propositions/proposition_32.tex → ...t-old/src/propositions/proposition_32.tex b/...print/src/propositions/proposition_32.tex → ...t-old/src/propositions/proposition_32.tex
diff --git a/...print/src/propositions/proposition_33.tex → ...t-old/src/propositions/proposition_33.tex b/...print/src/propositions/proposition_33.tex → ...t-old/src/propositions/proposition_33.tex
diff --git a/...print/src/propositions/proposition_34.tex → ...t-old/src/propositions/proposition_34.tex b/...print/src/propositions/proposition_34.tex → ...t-old/src/propositions/proposition_34.tex
diff --git a/...print/src/propositions/proposition_35.tex → ...t-old/src/propositions/proposition_35.tex b/...print/src/propositions/proposition_35.tex → ...t-old/src/propositions/proposition_35.tex
diff --git a/...print/src/propositions/proposition_36.tex → ...t-old/src/propositions/proposition_36.tex b/...print/src/propositions/proposition_36.tex → ...t-old/src/propositions/proposition_36.tex
diff --git a/...print/src/propositions/proposition_37.tex → ...t-old/src/propositions/proposition_37.tex b/...print/src/propositions/proposition_37.tex → ...t-old/src/propositions/proposition_37.tex
diff --git a/...print/src/propositions/proposition_38.tex → ...t-old/src/propositions/proposition_38.tex b/...print/src/propositions/proposition_38.tex → ...t-old/src/propositions/proposition_38.tex
diff --git a/...print/src/propositions/proposition_39.tex → ...t-old/src/propositions/proposition_39.tex b/...print/src/propositions/proposition_39.tex → ...t-old/src/propositions/proposition_39.tex
diff --git a/blueprint/src/propositions/proposition_4.tex → ...nt-old/src/propositions/proposition_4.tex b/blueprint/src/propositions/proposition_4.tex → ...nt-old/src/propositions/proposition_4.tex
diff --git a/...print/src/propositions/proposition_40.tex → ...t-old/src/propositions/proposition_40.tex b/...print/src/propositions/proposition_40.tex → ...t-old/src/propositions/proposition_40.tex
diff --git a/...print/src/propositions/proposition_41.tex → ...t-old/src/propositions/proposition_41.tex b/...print/src/propositions/proposition_41.tex → ...t-old/src/propositions/proposition_41.tex
diff --git a/...print/src/propositions/proposition_42.tex → ...t-old/src/propositions/proposition_42.tex b/...print/src/propositions/proposition_42.tex → ...t-old/src/propositions/proposition_42.tex
diff --git a/...print/src/propositions/proposition_43.tex → ...t-old/src/propositions/proposition_43.tex b/...print/src/propositions/proposition_43.tex → ...t-old/src/propositions/proposition_43.tex
diff --git a/...print/src/propositions/proposition_44.tex → ...t-old/src/propositions/proposition_44.tex b/...print/src/propositions/proposition_44.tex → ...t-old/src/propositions/proposition_44.tex
diff --git a/...print/src/propositions/proposition_45.tex → ...t-old/src/propositions/proposition_45.tex b/...print/src/propositions/proposition_45.tex → ...t-old/src/propositions/proposition_45.tex
diff --git a/...print/src/propositions/proposition_46.tex → ...t-old/src/propositions/proposition_46.tex b/...print/src/propositions/proposition_46.tex → ...t-old/src/propositions/proposition_46.tex
diff --git a/...print/src/propositions/proposition_47.tex → ...t-old/src/propositions/proposition_47.tex b/...print/src/propositions/proposition_47.tex → ...t-old/src/propositions/proposition_47.tex
diff --git a/...print/src/propositions/proposition_48.tex → ...t-old/src/propositions/proposition_48.tex b/...print/src/propositions/proposition_48.tex → ...t-old/src/propositions/proposition_48.tex
diff --git a/blueprint/src/propositions/proposition_5.tex → ...nt-old/src/propositions/proposition_5.tex b/blueprint/src/propositions/proposition_5.tex → ...nt-old/src/propositions/proposition_5.tex
diff --git a/blueprint/src/propositions/proposition_6.tex → ...nt-old/src/propositions/proposition_6.tex b/blueprint/src/propositions/proposition_6.tex → ...nt-old/src/propositions/proposition_6.tex
diff --git a/blueprint/src/propositions/proposition_7.tex → ...nt-old/src/propositions/proposition_7.tex b/blueprint/src/propositions/proposition_7.tex → ...nt-old/src/propositions/proposition_7.tex
diff --git a/blueprint/src/propositions/proposition_8.tex → ...nt-old/src/propositions/proposition_8.tex b/blueprint/src/propositions/proposition_8.tex → ...nt-old/src/propositions/proposition_8.tex
diff --git a/blueprint/src/propositions/proposition_9.tex → ...nt-old/src/propositions/proposition_9.tex b/blueprint/src/propositions/proposition_9.tex → ...nt-old/src/propositions/proposition_9.tex
diff --git a/blueprint/src/util.sty → blueprint-old/src/util.sty b/blueprint/src/util.sty → blueprint-old/src/util.sty
diff --git a/blueprint/src/web.paux → blueprint-old/src/web.paux b/blueprint/src/web.paux → blueprint-old/src/web.paux
diff --git a/blueprint-old/src/web.tex b/blueprint-old/src/web.tex
@@ -0,0 +1,35 @@
+% This file makes the web version of the blueprint.
+% This file can be built locally.
+
+\documentclass{report}
+
+\usepackage[utf8]{inputenc}
+\usepackage[english]{babel}
+\usepackage{charter}
+\usepackage{fancyhdr}
+\usepackage{epsf}
+\usepackage[bookmarks=true]{hyperref}
+\usepackage{amsmath,amsfonts,amsthm,amssymb}
+\usepackage{graphicx}
+\DeclareGraphicsExtensions{.svg,.png,.jpg}
+\usepackage[capitalize]{cleveref}
+\usepackage[showmore, dep_graph, project=../../]{blueprint}
+\usepackage{tikz-cd}
+\usepackage{tikz}
+
+\input{preamble/web}
+
+\github{https://github.com/loganrjmurphy/lean-geo-lib/}
+\dochome{https://loganrjmurphy.github.io/lean-geo-lib/docs}
+
+\title{The First Book of Euclid's Elements---Commentary and Lean Formalization}
+\author{
+    Logan Murphy$^{1}$, Jack Sun$^{1}$, Zhaoyu Li$^{1}$, Anima Anandkumar$^{2}$, Xujie Si$^{1\,\dagger}$, and Kaiyu Yang$^{2\,\dagger}$\\
+    $^1$University of Toronto, ~$^2$Caltech\\
+    $^\dagger$ Equal advising \\
+}
+
+\begin{document}
+\maketitle
+\input{main}
+\end{document}
diff --git a/blueprint/tasks.py → blueprint-old/tasks.py b/blueprint/tasks.py → blueprint-old/tasks.py
diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty
@@ -0,0 +1,2 @@
+\DeclareOption*{}
+\ProcessOptions
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
@@ -0,0 +1,7 @@
+% In this file you should put the actual content of the blueprint.
+% It will be used both by the web and the print version.
+% It should *not* include the \begin{document}
+%
+% If you want to split the blueprint content into several files then
+% the current file can be a simple sequence of \input. Otherwise It
+% can start with a \section or \chapter for instance.
diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css
@@ -1,3 +1,9 @@
+/* This file contains CSS tweaks for this blueprint.
+ * As an example, we included CSS rules that put
+ * a vertical line on the left of theorem statements
+ * and proofs.
+ * */
+
 div.theorem_thmcontent {
 	border-left: .15rem solid black;
 }
@@ -17,37 +23,3 @@ div.corollary_thmcontent {
 div.proof_content {
 	border-left: .08rem solid grey;
 }
-
-figure.subfloat span.subref {
-	display: none;
-}
-
-nav.local_toc ul {
-	font-size: 1.2rem;
-}
-
-@media (min-width:1024px) {
-    nav.toc {
-        width: 25vw;
-    }
-}
-
-@media (min-width:1024px) {
-    div.with-toc {
-        margin-left:25vw;
-    }
-}
-
-@font-face {
-  font-family: 'Open Sans';
-  font-style: normal;
-  font-weight: 400;
-  font-stretch: 100%;
-  font-display: swap;
-  src: url(https://fonts.gstatic.com/s/opensans/v29/memSYaGs126MiZpBA-UvWbX2vVnXBbObj2OVZyOOSr4dVJWUgsjZ0B4gaVI.woff2) format('woff2');
-  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+2000-206F, U+2074, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
-}
-
-body, h1, h2, h3, h4, h5, h6, p, text {
-  font-family: "Open Sans", "Helvetica Neue", Helvetica, Arial, sans-serif !important;
-}
diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc
@@ -1,3 +1,5 @@
+# This file configures the latexmk command you can use to compile
+# the pdf version of the blueprint
 $pdf_mode = 1;
-$pdflatex = 'xelatex -synctex=1 -output-directory=../print/';
-@default_files = ('print.tex');
+$pdflatex = 'xelatex -synctex=1';
+@default_files = ('print.tex');
diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex
@@ -0,0 +1,3 @@
+% In this file you should put all LaTeX macros to be used
+% both by the pdf version and the web version.
+% This should be most of your macros.
diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex
@@ -0,0 +1,29 @@
+% In this file you should put macros to be used only by
+% the printed version. Of course they should have a corresponding
+% version in macros/web.tex.
+% Typically the printed version could have more fancy decorations.
+% This should be a very short file.
+%
+% This file starts with dummy macros that ensure the pdf
+% compiler will ignore macros provided by plasTeX that make
+% sense only for the web version, such as dependency graph
+% macros.
+
+
+% Dummy macros that make sense only for web version.
+\newcommand{\lean}[1]{}
+\newcommand{\discussion}[1]{}
+\newcommand{\leanok}{}
+\newcommand{\mathlibok}{}
+\newcommand{\notready}{}
+% Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
+% latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
+% It uses LaTeX3 programming, this is why we use the expl3 package.
+\ExplSyntaxOn
+\NewDocumentCommand{\uses}{m}
+ {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
+  \ignorespaces}
+\NewDocumentCommand{\proves}{m}
+ {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
+  \ignorespaces}
+\ExplSyntaxOff
diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex
@@ -0,0 +1,5 @@
+% In this file you should put macros to be used only by
+% the web version. Of course they should have a corresponding
+% version in macros/print.tex.
+% Typically the printed version could have more fancy decorations.
+% This will probably be a very short file.
diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg
@@ -1,17 +1,17 @@
 [general]
 renderer=HTML5
 copy-theme-extras=yes
-plugins=leanblueprint
+plugins=plastexdepgraph  plastexshowmore  leanblueprint
 
 [document]
-toc-depth=2
+toc-depth=3
 toc-non-files=True
 
 [files]
 directory=../web/
-split-level=0
+split-level= 0
 
 [html5]
 localtoc-level=0
 extra-css=extra_styles.css
-mathjax-dollars=True
+mathjax-dollars=False