diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml new file mode 100644 index 0000000..0ce4d2a --- /dev/null +++ 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 \ No newline at end of file diff --git a/blueprint/requirements.txt b/blueprint-old/requirements.txt similarity index 100% rename from blueprint/requirements.txt rename to blueprint-old/requirements.txt diff --git a/blueprint/src/common_notions.tex b/blueprint-old/src/common_notions.tex similarity index 100% rename from blueprint/src/common_notions.tex rename to blueprint-old/src/common_notions.tex diff --git a/blueprint/src/definitions.tex b/blueprint-old/src/definitions.tex similarity index 100% rename from blueprint/src/definitions.tex rename to blueprint-old/src/definitions.tex diff --git a/blueprint-old/src/extra_styles.css b/blueprint-old/src/extra_styles.css new file mode 100644 index 0000000..10e84bf --- /dev/null +++ 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 b/blueprint-old/src/figures/fig01e.eps similarity index 100% rename from blueprint/src/figures/fig01e.eps rename to blueprint-old/src/figures/fig01e.eps diff --git a/blueprint/src/figures/fig01g.eps b/blueprint-old/src/figures/fig01g.eps similarity index 100% rename from blueprint/src/figures/fig01g.eps rename to blueprint-old/src/figures/fig01g.eps diff --git a/blueprint/src/figures/fig02e.eps b/blueprint-old/src/figures/fig02e.eps similarity index 100% rename from blueprint/src/figures/fig02e.eps rename to blueprint-old/src/figures/fig02e.eps diff --git a/blueprint/src/figures/fig02g.eps b/blueprint-old/src/figures/fig02g.eps similarity index 100% rename from blueprint/src/figures/fig02g.eps rename to blueprint-old/src/figures/fig02g.eps diff --git a/blueprint/src/figures/fig03e.eps b/blueprint-old/src/figures/fig03e.eps similarity index 100% rename from blueprint/src/figures/fig03e.eps rename to blueprint-old/src/figures/fig03e.eps diff --git a/blueprint/src/figures/fig03g.eps b/blueprint-old/src/figures/fig03g.eps similarity index 100% rename from blueprint/src/figures/fig03g.eps rename to blueprint-old/src/figures/fig03g.eps diff --git a/blueprint/src/figures/fig04e.eps b/blueprint-old/src/figures/fig04e.eps similarity index 100% rename from blueprint/src/figures/fig04e.eps rename to blueprint-old/src/figures/fig04e.eps diff --git a/blueprint/src/figures/fig04g.eps b/blueprint-old/src/figures/fig04g.eps similarity index 100% rename from blueprint/src/figures/fig04g.eps rename to blueprint-old/src/figures/fig04g.eps diff --git a/blueprint/src/figures/fig05e.eps b/blueprint-old/src/figures/fig05e.eps similarity index 100% rename from blueprint/src/figures/fig05e.eps rename to blueprint-old/src/figures/fig05e.eps diff --git a/blueprint/src/figures/fig05g.eps b/blueprint-old/src/figures/fig05g.eps similarity index 100% rename from blueprint/src/figures/fig05g.eps rename to blueprint-old/src/figures/fig05g.eps diff --git a/blueprint/src/figures/fig06e.eps b/blueprint-old/src/figures/fig06e.eps similarity index 100% rename from blueprint/src/figures/fig06e.eps rename to blueprint-old/src/figures/fig06e.eps diff --git a/blueprint/src/figures/fig06g.eps b/blueprint-old/src/figures/fig06g.eps similarity index 100% rename from blueprint/src/figures/fig06g.eps rename to blueprint-old/src/figures/fig06g.eps diff --git a/blueprint/src/figures/fig07e.eps b/blueprint-old/src/figures/fig07e.eps similarity index 100% rename from blueprint/src/figures/fig07e.eps rename to blueprint-old/src/figures/fig07e.eps diff --git a/blueprint/src/figures/fig07g.eps b/blueprint-old/src/figures/fig07g.eps similarity index 100% rename from blueprint/src/figures/fig07g.eps rename to blueprint-old/src/figures/fig07g.eps diff --git a/blueprint/src/figures/fig08e.eps b/blueprint-old/src/figures/fig08e.eps similarity index 100% rename from blueprint/src/figures/fig08e.eps rename to blueprint-old/src/figures/fig08e.eps diff --git a/blueprint/src/figures/fig08g.eps b/blueprint-old/src/figures/fig08g.eps similarity index 100% rename from blueprint/src/figures/fig08g.eps rename to blueprint-old/src/figures/fig08g.eps diff --git a/blueprint/src/figures/fig09e.eps b/blueprint-old/src/figures/fig09e.eps similarity index 100% rename from blueprint/src/figures/fig09e.eps rename to blueprint-old/src/figures/fig09e.eps diff --git a/blueprint/src/figures/fig09g.eps b/blueprint-old/src/figures/fig09g.eps similarity index 100% rename from blueprint/src/figures/fig09g.eps rename to blueprint-old/src/figures/fig09g.eps diff --git a/blueprint/src/figures/fig10e.eps b/blueprint-old/src/figures/fig10e.eps similarity index 100% rename from blueprint/src/figures/fig10e.eps rename to blueprint-old/src/figures/fig10e.eps diff --git a/blueprint/src/figures/fig10g.eps b/blueprint-old/src/figures/fig10g.eps similarity index 100% rename from blueprint/src/figures/fig10g.eps rename to blueprint-old/src/figures/fig10g.eps diff --git a/blueprint/src/figures/fig11e.eps b/blueprint-old/src/figures/fig11e.eps similarity index 100% rename from blueprint/src/figures/fig11e.eps rename to blueprint-old/src/figures/fig11e.eps diff --git a/blueprint/src/figures/fig11g.eps b/blueprint-old/src/figures/fig11g.eps similarity index 100% rename from blueprint/src/figures/fig11g.eps rename to blueprint-old/src/figures/fig11g.eps diff --git a/blueprint/src/figures/fig12e.eps b/blueprint-old/src/figures/fig12e.eps similarity index 100% rename from blueprint/src/figures/fig12e.eps rename to blueprint-old/src/figures/fig12e.eps diff --git a/blueprint/src/figures/fig12g.eps b/blueprint-old/src/figures/fig12g.eps similarity index 100% rename from blueprint/src/figures/fig12g.eps rename to blueprint-old/src/figures/fig12g.eps diff --git a/blueprint/src/figures/fig13e.eps b/blueprint-old/src/figures/fig13e.eps similarity index 100% rename from blueprint/src/figures/fig13e.eps rename to blueprint-old/src/figures/fig13e.eps diff --git a/blueprint/src/figures/fig13g.eps b/blueprint-old/src/figures/fig13g.eps similarity index 100% rename from blueprint/src/figures/fig13g.eps rename to blueprint-old/src/figures/fig13g.eps diff --git a/blueprint/src/figures/fig14e.eps b/blueprint-old/src/figures/fig14e.eps similarity index 100% rename from blueprint/src/figures/fig14e.eps rename to blueprint-old/src/figures/fig14e.eps diff --git a/blueprint/src/figures/fig14g.eps b/blueprint-old/src/figures/fig14g.eps similarity index 100% rename from blueprint/src/figures/fig14g.eps rename to blueprint-old/src/figures/fig14g.eps diff --git a/blueprint/src/figures/fig15e.eps b/blueprint-old/src/figures/fig15e.eps similarity index 100% rename from blueprint/src/figures/fig15e.eps rename to blueprint-old/src/figures/fig15e.eps diff --git a/blueprint/src/figures/fig15g.eps b/blueprint-old/src/figures/fig15g.eps similarity index 100% rename from blueprint/src/figures/fig15g.eps rename to blueprint-old/src/figures/fig15g.eps diff --git a/blueprint/src/figures/fig16e.eps b/blueprint-old/src/figures/fig16e.eps similarity index 100% rename from blueprint/src/figures/fig16e.eps rename to blueprint-old/src/figures/fig16e.eps diff --git a/blueprint/src/figures/fig16g.eps b/blueprint-old/src/figures/fig16g.eps similarity index 100% rename from blueprint/src/figures/fig16g.eps rename to blueprint-old/src/figures/fig16g.eps diff --git a/blueprint/src/figures/fig17e.eps b/blueprint-old/src/figures/fig17e.eps similarity index 100% rename from blueprint/src/figures/fig17e.eps rename to blueprint-old/src/figures/fig17e.eps diff --git a/blueprint/src/figures/fig17g.eps b/blueprint-old/src/figures/fig17g.eps similarity index 100% rename from blueprint/src/figures/fig17g.eps rename to blueprint-old/src/figures/fig17g.eps diff --git a/blueprint/src/figures/fig18e.eps b/blueprint-old/src/figures/fig18e.eps similarity index 100% rename from blueprint/src/figures/fig18e.eps rename to blueprint-old/src/figures/fig18e.eps diff --git a/blueprint/src/figures/fig18g.eps b/blueprint-old/src/figures/fig18g.eps similarity index 100% rename from blueprint/src/figures/fig18g.eps rename to blueprint-old/src/figures/fig18g.eps diff --git a/blueprint/src/figures/fig19e.eps b/blueprint-old/src/figures/fig19e.eps similarity index 100% rename from blueprint/src/figures/fig19e.eps rename to blueprint-old/src/figures/fig19e.eps diff --git a/blueprint/src/figures/fig19g.eps b/blueprint-old/src/figures/fig19g.eps similarity index 100% rename from blueprint/src/figures/fig19g.eps rename to blueprint-old/src/figures/fig19g.eps diff --git a/blueprint/src/figures/fig20e.eps b/blueprint-old/src/figures/fig20e.eps similarity index 100% rename from blueprint/src/figures/fig20e.eps rename to blueprint-old/src/figures/fig20e.eps diff --git a/blueprint/src/figures/fig20g.eps b/blueprint-old/src/figures/fig20g.eps similarity index 100% rename from blueprint/src/figures/fig20g.eps rename to blueprint-old/src/figures/fig20g.eps diff --git a/blueprint/src/figures/fig21e.eps b/blueprint-old/src/figures/fig21e.eps similarity index 100% rename from blueprint/src/figures/fig21e.eps rename to blueprint-old/src/figures/fig21e.eps diff --git a/blueprint/src/figures/fig21g.eps b/blueprint-old/src/figures/fig21g.eps similarity index 100% rename from blueprint/src/figures/fig21g.eps rename to blueprint-old/src/figures/fig21g.eps diff --git a/blueprint/src/figures/fig22e.eps b/blueprint-old/src/figures/fig22e.eps similarity index 100% rename from blueprint/src/figures/fig22e.eps rename to blueprint-old/src/figures/fig22e.eps diff --git a/blueprint/src/figures/fig22g.eps b/blueprint-old/src/figures/fig22g.eps similarity index 100% rename from blueprint/src/figures/fig22g.eps rename to blueprint-old/src/figures/fig22g.eps diff --git a/blueprint/src/figures/fig23e.eps b/blueprint-old/src/figures/fig23e.eps similarity index 100% rename from blueprint/src/figures/fig23e.eps rename to blueprint-old/src/figures/fig23e.eps diff --git a/blueprint/src/figures/fig23g.eps b/blueprint-old/src/figures/fig23g.eps similarity index 100% rename from blueprint/src/figures/fig23g.eps rename to blueprint-old/src/figures/fig23g.eps diff --git a/blueprint/src/figures/fig24e.eps b/blueprint-old/src/figures/fig24e.eps similarity index 100% rename from blueprint/src/figures/fig24e.eps rename to blueprint-old/src/figures/fig24e.eps diff --git a/blueprint/src/figures/fig24g.eps b/blueprint-old/src/figures/fig24g.eps similarity index 100% rename from blueprint/src/figures/fig24g.eps rename to blueprint-old/src/figures/fig24g.eps diff --git a/blueprint/src/figures/fig25e.eps b/blueprint-old/src/figures/fig25e.eps similarity index 100% rename from blueprint/src/figures/fig25e.eps rename to blueprint-old/src/figures/fig25e.eps diff --git a/blueprint/src/figures/fig25g.eps b/blueprint-old/src/figures/fig25g.eps similarity index 100% rename from blueprint/src/figures/fig25g.eps rename to blueprint-old/src/figures/fig25g.eps diff --git a/blueprint/src/figures/fig26e.eps b/blueprint-old/src/figures/fig26e.eps similarity index 100% rename from blueprint/src/figures/fig26e.eps rename to blueprint-old/src/figures/fig26e.eps diff --git a/blueprint/src/figures/fig26g.eps b/blueprint-old/src/figures/fig26g.eps similarity index 100% rename from blueprint/src/figures/fig26g.eps rename to blueprint-old/src/figures/fig26g.eps diff --git a/blueprint/src/figures/fig27e.eps b/blueprint-old/src/figures/fig27e.eps similarity index 100% rename from blueprint/src/figures/fig27e.eps rename to blueprint-old/src/figures/fig27e.eps diff --git a/blueprint/src/figures/fig27g.eps b/blueprint-old/src/figures/fig27g.eps similarity index 100% rename from blueprint/src/figures/fig27g.eps rename to blueprint-old/src/figures/fig27g.eps diff --git a/blueprint/src/figures/fig28e.eps b/blueprint-old/src/figures/fig28e.eps similarity index 100% rename from blueprint/src/figures/fig28e.eps rename to blueprint-old/src/figures/fig28e.eps diff --git a/blueprint/src/figures/fig28g.eps b/blueprint-old/src/figures/fig28g.eps similarity index 100% rename from blueprint/src/figures/fig28g.eps rename to blueprint-old/src/figures/fig28g.eps diff --git a/blueprint/src/figures/fig30e.eps b/blueprint-old/src/figures/fig30e.eps similarity index 100% rename from blueprint/src/figures/fig30e.eps rename to blueprint-old/src/figures/fig30e.eps diff --git a/blueprint/src/figures/fig30g.eps b/blueprint-old/src/figures/fig30g.eps similarity index 100% rename from blueprint/src/figures/fig30g.eps rename to blueprint-old/src/figures/fig30g.eps diff --git a/blueprint/src/figures/fig31e.eps b/blueprint-old/src/figures/fig31e.eps similarity index 100% rename from blueprint/src/figures/fig31e.eps rename to blueprint-old/src/figures/fig31e.eps diff --git a/blueprint/src/figures/fig31g.eps b/blueprint-old/src/figures/fig31g.eps similarity index 100% rename from blueprint/src/figures/fig31g.eps rename to blueprint-old/src/figures/fig31g.eps diff --git a/blueprint/src/figures/fig32e.eps b/blueprint-old/src/figures/fig32e.eps similarity index 100% rename from blueprint/src/figures/fig32e.eps rename to blueprint-old/src/figures/fig32e.eps diff --git a/blueprint/src/figures/fig32g.eps b/blueprint-old/src/figures/fig32g.eps similarity index 100% rename from blueprint/src/figures/fig32g.eps rename to blueprint-old/src/figures/fig32g.eps diff --git a/blueprint/src/figures/fig33e.eps b/blueprint-old/src/figures/fig33e.eps similarity index 100% rename from blueprint/src/figures/fig33e.eps rename to blueprint-old/src/figures/fig33e.eps diff --git a/blueprint/src/figures/fig33g.eps b/blueprint-old/src/figures/fig33g.eps similarity index 100% rename from blueprint/src/figures/fig33g.eps rename to blueprint-old/src/figures/fig33g.eps diff --git a/blueprint/src/figures/fig34e.eps b/blueprint-old/src/figures/fig34e.eps similarity index 100% rename from blueprint/src/figures/fig34e.eps rename to blueprint-old/src/figures/fig34e.eps diff --git a/blueprint/src/figures/fig34g.eps b/blueprint-old/src/figures/fig34g.eps similarity index 100% rename from blueprint/src/figures/fig34g.eps rename to blueprint-old/src/figures/fig34g.eps diff --git a/blueprint/src/figures/fig35e.eps b/blueprint-old/src/figures/fig35e.eps similarity index 100% rename from blueprint/src/figures/fig35e.eps rename to blueprint-old/src/figures/fig35e.eps diff --git a/blueprint/src/figures/fig35g.eps b/blueprint-old/src/figures/fig35g.eps similarity index 100% rename from blueprint/src/figures/fig35g.eps rename to blueprint-old/src/figures/fig35g.eps diff --git a/blueprint/src/figures/fig36e.eps b/blueprint-old/src/figures/fig36e.eps similarity index 100% rename from blueprint/src/figures/fig36e.eps rename to blueprint-old/src/figures/fig36e.eps diff --git a/blueprint/src/figures/fig36g.eps b/blueprint-old/src/figures/fig36g.eps similarity index 100% rename from blueprint/src/figures/fig36g.eps rename to blueprint-old/src/figures/fig36g.eps diff --git a/blueprint/src/figures/fig37e.eps b/blueprint-old/src/figures/fig37e.eps similarity index 100% rename from blueprint/src/figures/fig37e.eps rename to blueprint-old/src/figures/fig37e.eps diff --git a/blueprint/src/figures/fig37g.eps b/blueprint-old/src/figures/fig37g.eps similarity index 100% rename from blueprint/src/figures/fig37g.eps rename to blueprint-old/src/figures/fig37g.eps diff --git a/blueprint/src/figures/fig38e.eps b/blueprint-old/src/figures/fig38e.eps similarity index 100% rename from blueprint/src/figures/fig38e.eps rename to blueprint-old/src/figures/fig38e.eps diff --git a/blueprint/src/figures/fig38g.eps b/blueprint-old/src/figures/fig38g.eps similarity index 100% rename from blueprint/src/figures/fig38g.eps rename to blueprint-old/src/figures/fig38g.eps diff --git a/blueprint/src/figures/fig39e.eps b/blueprint-old/src/figures/fig39e.eps similarity index 100% rename from blueprint/src/figures/fig39e.eps rename to blueprint-old/src/figures/fig39e.eps diff --git a/blueprint/src/figures/fig39g.eps b/blueprint-old/src/figures/fig39g.eps similarity index 100% rename from blueprint/src/figures/fig39g.eps rename to blueprint-old/src/figures/fig39g.eps diff --git a/blueprint/src/figures/fig40e.eps b/blueprint-old/src/figures/fig40e.eps similarity index 100% rename from blueprint/src/figures/fig40e.eps rename to blueprint-old/src/figures/fig40e.eps diff --git a/blueprint/src/figures/fig40g.eps b/blueprint-old/src/figures/fig40g.eps similarity index 100% rename from blueprint/src/figures/fig40g.eps rename to blueprint-old/src/figures/fig40g.eps diff --git a/blueprint/src/figures/fig41e.eps b/blueprint-old/src/figures/fig41e.eps similarity index 100% rename from blueprint/src/figures/fig41e.eps rename to blueprint-old/src/figures/fig41e.eps diff --git a/blueprint/src/figures/fig41g.eps b/blueprint-old/src/figures/fig41g.eps similarity index 100% rename from blueprint/src/figures/fig41g.eps rename to blueprint-old/src/figures/fig41g.eps diff --git a/blueprint/src/figures/fig42e.eps b/blueprint-old/src/figures/fig42e.eps similarity index 100% rename from blueprint/src/figures/fig42e.eps rename to blueprint-old/src/figures/fig42e.eps diff --git a/blueprint/src/figures/fig42g.eps b/blueprint-old/src/figures/fig42g.eps similarity index 100% rename from blueprint/src/figures/fig42g.eps rename to blueprint-old/src/figures/fig42g.eps diff --git a/blueprint/src/figures/fig43e.eps b/blueprint-old/src/figures/fig43e.eps similarity index 100% rename from blueprint/src/figures/fig43e.eps rename to blueprint-old/src/figures/fig43e.eps diff --git a/blueprint/src/figures/fig43g.eps b/blueprint-old/src/figures/fig43g.eps similarity index 100% rename from blueprint/src/figures/fig43g.eps rename to blueprint-old/src/figures/fig43g.eps diff --git a/blueprint/src/figures/fig44e.eps b/blueprint-old/src/figures/fig44e.eps similarity index 100% rename from blueprint/src/figures/fig44e.eps rename to blueprint-old/src/figures/fig44e.eps diff --git a/blueprint/src/figures/fig44g.eps b/blueprint-old/src/figures/fig44g.eps similarity index 100% rename from blueprint/src/figures/fig44g.eps rename to blueprint-old/src/figures/fig44g.eps diff --git a/blueprint/src/figures/fig45e.eps b/blueprint-old/src/figures/fig45e.eps similarity index 100% rename from blueprint/src/figures/fig45e.eps rename to blueprint-old/src/figures/fig45e.eps diff --git a/blueprint/src/figures/fig45g.eps b/blueprint-old/src/figures/fig45g.eps similarity index 100% rename from blueprint/src/figures/fig45g.eps rename to blueprint-old/src/figures/fig45g.eps diff --git a/blueprint/src/figures/fig46e.eps b/blueprint-old/src/figures/fig46e.eps similarity index 100% rename from blueprint/src/figures/fig46e.eps rename to blueprint-old/src/figures/fig46e.eps diff --git a/blueprint/src/figures/fig46g.eps b/blueprint-old/src/figures/fig46g.eps similarity index 100% rename from blueprint/src/figures/fig46g.eps rename to blueprint-old/src/figures/fig46g.eps diff --git a/blueprint/src/figures/fig47e.eps b/blueprint-old/src/figures/fig47e.eps similarity index 100% rename from blueprint/src/figures/fig47e.eps rename to blueprint-old/src/figures/fig47e.eps diff --git a/blueprint/src/figures/fig47g.eps b/blueprint-old/src/figures/fig47g.eps similarity index 100% rename from blueprint/src/figures/fig47g.eps rename to blueprint-old/src/figures/fig47g.eps diff --git a/blueprint/src/figures/fig48e.eps b/blueprint-old/src/figures/fig48e.eps similarity index 100% rename from blueprint/src/figures/fig48e.eps rename to blueprint-old/src/figures/fig48e.eps diff --git a/blueprint/src/figures/fig48g.eps b/blueprint-old/src/figures/fig48g.eps similarity index 100% rename from blueprint/src/figures/fig48g.eps rename to blueprint-old/src/figures/fig48g.eps diff --git a/blueprint/src/figures/proposition_24.png b/blueprint-old/src/figures/proposition_24.png similarity index 100% rename from blueprint/src/figures/proposition_24.png rename to blueprint-old/src/figures/proposition_24.png diff --git a/blueprint/src/figures/proposition_7'''.png b/blueprint-old/src/figures/proposition_7'''.png similarity index 100% rename from blueprint/src/figures/proposition_7'''.png rename to blueprint-old/src/figures/proposition_7'''.png diff --git a/blueprint/src/figures/proposition_7''.png b/blueprint-old/src/figures/proposition_7''.png similarity index 100% rename from blueprint/src/figures/proposition_7''.png rename to blueprint-old/src/figures/proposition_7''.png diff --git a/blueprint/src/figures/proposition_7'.png b/blueprint-old/src/figures/proposition_7'.png similarity index 100% rename from blueprint/src/figures/proposition_7'.png rename to blueprint-old/src/figures/proposition_7'.png diff --git a/blueprint/src/figures/proposition_9.png b/blueprint-old/src/figures/proposition_9.png similarity index 100% rename from blueprint/src/figures/proposition_9.png rename to blueprint-old/src/figures/proposition_9.png diff --git a/blueprint/src/intro.tex b/blueprint-old/src/intro.tex similarity index 100% rename from blueprint/src/intro.tex rename to blueprint-old/src/intro.tex diff --git a/blueprint-old/src/latexmkrc b/blueprint-old/src/latexmkrc new file mode 100644 index 0000000..3196896 --- /dev/null +++ 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 b/blueprint-old/src/main.tex similarity index 100% rename from blueprint/src/main.tex rename to blueprint-old/src/main.tex diff --git a/blueprint-old/src/plastex.cfg b/blueprint-old/src/plastex.cfg new file mode 100644 index 0000000..e2fa083 --- /dev/null +++ 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 b/blueprint-old/src/postulates.tex similarity index 100% rename from blueprint/src/postulates.tex rename to blueprint-old/src/postulates.tex diff --git a/blueprint/src/preamble/print.tex b/blueprint-old/src/preamble/print.tex similarity index 100% rename from blueprint/src/preamble/print.tex rename to blueprint-old/src/preamble/print.tex diff --git a/blueprint/src/preamble/web.tex b/blueprint-old/src/preamble/web.tex similarity index 100% rename from blueprint/src/preamble/web.tex rename to blueprint-old/src/preamble/web.tex diff --git a/blueprint-old/src/print.tex b/blueprint-old/src/print.tex new file mode 100644 index 0000000..d45747b --- /dev/null +++ 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 b/blueprint-old/src/propositions/proposition_1.tex similarity index 100% rename from blueprint/src/propositions/proposition_1.tex rename to blueprint-old/src/propositions/proposition_1.tex diff --git a/blueprint/src/propositions/proposition_10.tex b/blueprint-old/src/propositions/proposition_10.tex similarity index 100% rename from blueprint/src/propositions/proposition_10.tex rename to blueprint-old/src/propositions/proposition_10.tex diff --git a/blueprint/src/propositions/proposition_11.tex b/blueprint-old/src/propositions/proposition_11.tex similarity index 100% rename from blueprint/src/propositions/proposition_11.tex rename to blueprint-old/src/propositions/proposition_11.tex diff --git a/blueprint/src/propositions/proposition_12.tex b/blueprint-old/src/propositions/proposition_12.tex similarity index 100% rename from blueprint/src/propositions/proposition_12.tex rename to blueprint-old/src/propositions/proposition_12.tex diff --git a/blueprint/src/propositions/proposition_13.tex b/blueprint-old/src/propositions/proposition_13.tex similarity index 100% rename from blueprint/src/propositions/proposition_13.tex rename to blueprint-old/src/propositions/proposition_13.tex diff --git a/blueprint/src/propositions/proposition_14.tex b/blueprint-old/src/propositions/proposition_14.tex similarity index 100% rename from blueprint/src/propositions/proposition_14.tex rename to blueprint-old/src/propositions/proposition_14.tex diff --git a/blueprint/src/propositions/proposition_15.tex b/blueprint-old/src/propositions/proposition_15.tex similarity index 100% rename from blueprint/src/propositions/proposition_15.tex rename to blueprint-old/src/propositions/proposition_15.tex diff --git a/blueprint/src/propositions/proposition_16.tex b/blueprint-old/src/propositions/proposition_16.tex similarity index 100% rename from blueprint/src/propositions/proposition_16.tex rename to blueprint-old/src/propositions/proposition_16.tex diff --git a/blueprint/src/propositions/proposition_17.tex b/blueprint-old/src/propositions/proposition_17.tex similarity index 100% rename from blueprint/src/propositions/proposition_17.tex rename to blueprint-old/src/propositions/proposition_17.tex diff --git a/blueprint/src/propositions/proposition_18.tex b/blueprint-old/src/propositions/proposition_18.tex similarity index 100% rename from blueprint/src/propositions/proposition_18.tex rename to blueprint-old/src/propositions/proposition_18.tex diff --git a/blueprint/src/propositions/proposition_19.tex b/blueprint-old/src/propositions/proposition_19.tex similarity index 100% rename from blueprint/src/propositions/proposition_19.tex rename to blueprint-old/src/propositions/proposition_19.tex diff --git a/blueprint/src/propositions/proposition_2.tex b/blueprint-old/src/propositions/proposition_2.tex similarity index 100% rename from blueprint/src/propositions/proposition_2.tex rename to blueprint-old/src/propositions/proposition_2.tex diff --git a/blueprint/src/propositions/proposition_20.tex b/blueprint-old/src/propositions/proposition_20.tex similarity index 100% rename from blueprint/src/propositions/proposition_20.tex rename to blueprint-old/src/propositions/proposition_20.tex diff --git a/blueprint/src/propositions/proposition_21.tex b/blueprint-old/src/propositions/proposition_21.tex similarity index 100% rename from blueprint/src/propositions/proposition_21.tex rename to blueprint-old/src/propositions/proposition_21.tex diff --git a/blueprint/src/propositions/proposition_22.tex b/blueprint-old/src/propositions/proposition_22.tex similarity index 100% rename from blueprint/src/propositions/proposition_22.tex rename to blueprint-old/src/propositions/proposition_22.tex diff --git a/blueprint/src/propositions/proposition_23.tex b/blueprint-old/src/propositions/proposition_23.tex similarity index 100% rename from blueprint/src/propositions/proposition_23.tex rename to blueprint-old/src/propositions/proposition_23.tex diff --git a/blueprint/src/propositions/proposition_24.tex b/blueprint-old/src/propositions/proposition_24.tex similarity index 100% rename from blueprint/src/propositions/proposition_24.tex rename to blueprint-old/src/propositions/proposition_24.tex diff --git a/blueprint/src/propositions/proposition_25.tex b/blueprint-old/src/propositions/proposition_25.tex similarity index 100% rename from blueprint/src/propositions/proposition_25.tex rename to blueprint-old/src/propositions/proposition_25.tex diff --git a/blueprint/src/propositions/proposition_26.tex b/blueprint-old/src/propositions/proposition_26.tex similarity index 100% rename from blueprint/src/propositions/proposition_26.tex rename to blueprint-old/src/propositions/proposition_26.tex diff --git a/blueprint/src/propositions/proposition_27.tex b/blueprint-old/src/propositions/proposition_27.tex similarity index 100% rename from blueprint/src/propositions/proposition_27.tex rename to blueprint-old/src/propositions/proposition_27.tex diff --git a/blueprint/src/propositions/proposition_28.tex b/blueprint-old/src/propositions/proposition_28.tex similarity index 100% rename from blueprint/src/propositions/proposition_28.tex rename to blueprint-old/src/propositions/proposition_28.tex diff --git a/blueprint/src/propositions/proposition_29.tex b/blueprint-old/src/propositions/proposition_29.tex similarity index 100% rename from blueprint/src/propositions/proposition_29.tex rename to blueprint-old/src/propositions/proposition_29.tex diff --git a/blueprint/src/propositions/proposition_3.tex b/blueprint-old/src/propositions/proposition_3.tex similarity index 100% rename from blueprint/src/propositions/proposition_3.tex rename to blueprint-old/src/propositions/proposition_3.tex diff --git a/blueprint/src/propositions/proposition_30.tex b/blueprint-old/src/propositions/proposition_30.tex similarity index 100% rename from blueprint/src/propositions/proposition_30.tex rename to blueprint-old/src/propositions/proposition_30.tex diff --git a/blueprint/src/propositions/proposition_31.tex b/blueprint-old/src/propositions/proposition_31.tex similarity index 100% rename from blueprint/src/propositions/proposition_31.tex rename to blueprint-old/src/propositions/proposition_31.tex diff --git a/blueprint/src/propositions/proposition_32.tex b/blueprint-old/src/propositions/proposition_32.tex similarity index 100% rename from blueprint/src/propositions/proposition_32.tex rename to blueprint-old/src/propositions/proposition_32.tex diff --git a/blueprint/src/propositions/proposition_33.tex b/blueprint-old/src/propositions/proposition_33.tex similarity index 100% rename from blueprint/src/propositions/proposition_33.tex rename to blueprint-old/src/propositions/proposition_33.tex diff --git a/blueprint/src/propositions/proposition_34.tex b/blueprint-old/src/propositions/proposition_34.tex similarity index 100% rename from blueprint/src/propositions/proposition_34.tex rename to blueprint-old/src/propositions/proposition_34.tex diff --git a/blueprint/src/propositions/proposition_35.tex b/blueprint-old/src/propositions/proposition_35.tex similarity index 100% rename from blueprint/src/propositions/proposition_35.tex rename to blueprint-old/src/propositions/proposition_35.tex diff --git a/blueprint/src/propositions/proposition_36.tex b/blueprint-old/src/propositions/proposition_36.tex similarity index 100% rename from blueprint/src/propositions/proposition_36.tex rename to blueprint-old/src/propositions/proposition_36.tex diff --git a/blueprint/src/propositions/proposition_37.tex b/blueprint-old/src/propositions/proposition_37.tex similarity index 100% rename from blueprint/src/propositions/proposition_37.tex rename to blueprint-old/src/propositions/proposition_37.tex diff --git a/blueprint/src/propositions/proposition_38.tex b/blueprint-old/src/propositions/proposition_38.tex similarity index 100% rename from blueprint/src/propositions/proposition_38.tex rename to blueprint-old/src/propositions/proposition_38.tex diff --git a/blueprint/src/propositions/proposition_39.tex b/blueprint-old/src/propositions/proposition_39.tex similarity index 100% rename from blueprint/src/propositions/proposition_39.tex rename to blueprint-old/src/propositions/proposition_39.tex diff --git a/blueprint/src/propositions/proposition_4.tex b/blueprint-old/src/propositions/proposition_4.tex similarity index 100% rename from blueprint/src/propositions/proposition_4.tex rename to blueprint-old/src/propositions/proposition_4.tex diff --git a/blueprint/src/propositions/proposition_40.tex b/blueprint-old/src/propositions/proposition_40.tex similarity index 100% rename from blueprint/src/propositions/proposition_40.tex rename to blueprint-old/src/propositions/proposition_40.tex diff --git a/blueprint/src/propositions/proposition_41.tex b/blueprint-old/src/propositions/proposition_41.tex similarity index 100% rename from blueprint/src/propositions/proposition_41.tex rename to blueprint-old/src/propositions/proposition_41.tex diff --git a/blueprint/src/propositions/proposition_42.tex b/blueprint-old/src/propositions/proposition_42.tex similarity index 100% rename from blueprint/src/propositions/proposition_42.tex rename to blueprint-old/src/propositions/proposition_42.tex diff --git a/blueprint/src/propositions/proposition_43.tex b/blueprint-old/src/propositions/proposition_43.tex similarity index 100% rename from blueprint/src/propositions/proposition_43.tex rename to blueprint-old/src/propositions/proposition_43.tex diff --git a/blueprint/src/propositions/proposition_44.tex b/blueprint-old/src/propositions/proposition_44.tex similarity index 100% rename from blueprint/src/propositions/proposition_44.tex rename to blueprint-old/src/propositions/proposition_44.tex diff --git a/blueprint/src/propositions/proposition_45.tex b/blueprint-old/src/propositions/proposition_45.tex similarity index 100% rename from blueprint/src/propositions/proposition_45.tex rename to blueprint-old/src/propositions/proposition_45.tex diff --git a/blueprint/src/propositions/proposition_46.tex b/blueprint-old/src/propositions/proposition_46.tex similarity index 100% rename from blueprint/src/propositions/proposition_46.tex rename to blueprint-old/src/propositions/proposition_46.tex diff --git a/blueprint/src/propositions/proposition_47.tex b/blueprint-old/src/propositions/proposition_47.tex similarity index 100% rename from blueprint/src/propositions/proposition_47.tex rename to blueprint-old/src/propositions/proposition_47.tex diff --git a/blueprint/src/propositions/proposition_48.tex b/blueprint-old/src/propositions/proposition_48.tex similarity index 100% rename from blueprint/src/propositions/proposition_48.tex rename to blueprint-old/src/propositions/proposition_48.tex diff --git a/blueprint/src/propositions/proposition_5.tex b/blueprint-old/src/propositions/proposition_5.tex similarity index 100% rename from blueprint/src/propositions/proposition_5.tex rename to blueprint-old/src/propositions/proposition_5.tex diff --git a/blueprint/src/propositions/proposition_6.tex b/blueprint-old/src/propositions/proposition_6.tex similarity index 100% rename from blueprint/src/propositions/proposition_6.tex rename to blueprint-old/src/propositions/proposition_6.tex diff --git a/blueprint/src/propositions/proposition_7.tex b/blueprint-old/src/propositions/proposition_7.tex similarity index 100% rename from blueprint/src/propositions/proposition_7.tex rename to blueprint-old/src/propositions/proposition_7.tex diff --git a/blueprint/src/propositions/proposition_8.tex b/blueprint-old/src/propositions/proposition_8.tex similarity index 100% rename from blueprint/src/propositions/proposition_8.tex rename to blueprint-old/src/propositions/proposition_8.tex diff --git a/blueprint/src/propositions/proposition_9.tex b/blueprint-old/src/propositions/proposition_9.tex similarity index 100% rename from blueprint/src/propositions/proposition_9.tex rename to blueprint-old/src/propositions/proposition_9.tex diff --git a/blueprint/src/util.sty b/blueprint-old/src/util.sty similarity index 100% rename from blueprint/src/util.sty rename to blueprint-old/src/util.sty diff --git a/blueprint/src/web.paux b/blueprint-old/src/web.paux similarity index 100% rename from blueprint/src/web.paux rename to blueprint-old/src/web.paux diff --git a/blueprint-old/src/web.tex b/blueprint-old/src/web.tex new file mode 100644 index 0000000..4bab828 --- /dev/null +++ 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 b/blueprint-old/tasks.py similarity index 100% rename from blueprint/tasks.py rename to blueprint-old/tasks.py diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty new file mode 100644 index 0000000..1353f39 --- /dev/null +++ b/blueprint/src/blueprint.sty @@ -0,0 +1,2 @@ +\DeclareOption*{} +\ProcessOptions \ No newline at end of file diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex new file mode 100644 index 0000000..b5cd27b --- /dev/null +++ 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. \ No newline at end of file diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css index 10e84bf..b96c776 100644 --- 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 index 3196896..38d5963 100644 --- 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'); \ No newline at end of file diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex new file mode 100644 index 0000000..131c9f8 --- /dev/null +++ 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. \ No newline at end of file diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex new file mode 100644 index 0000000..668fec1 --- /dev/null +++ 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 \ No newline at end of file diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex new file mode 100644 index 0000000..ceee975 --- /dev/null +++ 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. \ No newline at end of file diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg index e2fa083..de3dbae 100644 --- 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 \ No newline at end of file diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index d45747b..12f061b 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -1,36 +1,33 @@ % This file makes a printable version of the blueprint +% It should include all the \usepackage needed for the pdf version. +% The template version assume you want to use a modern TeX compiler +% such as xeLaTeX or luaLaTeX including support for unicode +% and Latin Modern Math font with standard bugfixes applied. +% It also uses expl3 in order to support macros related to the dependency graph. +% It also includes standard AMS packages (and their improved version +% mathtools) as well as support for links with a sober decoration +% (no ugly rectangles around links). +% It is otherwise a very minimal preamble (you should probably at least +% add cleveref and tikz-cd). \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{geometry} + +\usepackage{expl3} -\usepackage[nameinlink, capitalize]{cleveref} +\usepackage{amssymb, amsthm, mathtools} +\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref} -\usepackage{amsthm} -\usepackage{etexcmds} -\usepackage{thmtools} +\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math} -\input{preamble/print} +\input{macros/common} +\input{macros/print} -\title{The First Book of Euclid's Elements---Commentary and Lean Formalization} -\author{Logan Murphy and Kaiyu Yang} +\title{LeanEuclid} +\author{Logan Murphy \and Kaiyu Yang} \begin{document} \maketitle -\input{main} -\end{document} +\input{content} +\end{document} \ No newline at end of file diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index 4bab828..bec1e15 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -1,35 +1,27 @@ -% This file makes the web version of the blueprint. -% This file can be built locally. +% This file makes a web version of the blueprint +% It should include all the \usepackage needed for this version. +% The template includes standard AMS packages. +% It is otherwise a very minimal preamble (you should probably at least +% add cleveref and tikz-cd). \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} +\usepackage{amssymb, amsthm, amsmath} +\usepackage{hyperref} +\usepackage[showmore, dep_graph]{blueprint} -\input{preamble/web} -\github{https://github.com/loganrjmurphy/lean-geo-lib/} -\dochome{https://loganrjmurphy.github.io/lean-geo-lib/docs} +\input{macros/common} +\input{macros/web} -\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 \\ -} +\home{https://loganrjmurphy.github.io/LeanEuclid} +\github{https://github.com/loganrjmurphy/LeanEuclid} +\dochome{https://loganrjmurphy.github.io/LeanEuclid/docs} + +\title{LeanEuclid} +\author{Logan Murphy \and Kaiyu Yang} \begin{document} \maketitle -\input{main} -\end{document} +\input{content} +\end{document} \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index fd88cc5..349b311 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -73,6 +73,15 @@ "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, {"url": "https://github.com/xubaiw/CMark.lean", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index 78d9cd9..d6d4c42 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -22,9 +22,6 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4" require smt from git "https://github.com/yangky11/lean-smt.git" @ "main" -meta if get_config? env = some "dev" then -- dev is so not everyone has to build it -require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" - def tmpFileDir := "tmp" def checkAvailable (cmd : String) : IO Unit := do @@ -64,3 +61,9 @@ script aggregate do println! codeAll return 0 + +require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" + +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file