Setup blueprint

.github/workflows/blueprint.yml

@@ -0,0 +1,92 @@
+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: Update checkdecls
+        run: ~/.elan/bin/lake update checkdecls
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build FLT3
+
+      - 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-FLT3*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build FLT3: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

.gitignore

@@ -9,3 +9,5 @@
 /lakefile.olean
 # After v4.3.0-rc2 lake stores its files here:
 /.lake/
+# Python virtual environment 
+/.venv/

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.

blueprint/src/extra_styles.css

@@ -0,0 +1,25 @@
+/* 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;
+}
+
+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;
+}

blueprint/src/latexmkrc

@@ -0,0 +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';
+@default_files = ('print.tex');

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.

blueprint/src/macros/print.tex

@@ -0,0 +1,28 @@
+% 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}{}
+% 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

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.

blueprint/src/plastex.cfg

@@ -0,0 +1,17 @@
+[general]
+renderer=HTML5
+copy-theme-extras=yes
+plugins=plastexdepgraph  plastexshowmore  leanblueprint
+
+[document]
+toc-depth=3
+toc-non-files=True
+
+[files]
+directory=../web/
+split-level= 0
+
+[html5]
+localtoc-level=0
+extra-css=extra_styles.css
+mathjax-dollars=False

blueprint/src/print.tex

@@ -0,0 +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{geometry}
+
+\usepackage{expl3}
+
+\usepackage{amssymb, amsthm, mathtools}
+\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}
+
+\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
+
+\input{macros/common}
+\input{macros/print}
+
+\title{Fermat's Last Theorem for Exponent 3}
+\author{Pietro Monticone}
+
+\begin{document}
+\maketitle
+\input{content}
+\end{document}

blueprint/src/web.tex

@@ -0,0 +1,27 @@
+% 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{amssymb, amsthm, amsmath}
+\usepackage{hyperref}
+\usepackage[showmore, dep_graph]{blueprint}
+
+
+\input{macros/common}
+\input{macros/web}
+
+\home{https://pitmonticone.github.io/FLT3}
+\github{https://github.com/pitmonticone/FLT3}
+\dochome{https://pitmonticone.github.io/FLT3/docs}
+
+\title{Fermat's Last Theorem for Exponent 3}
+\author{Pietro Monticone}
+
+\begin{document}
+\maketitle
+\input{content}
+\end{document}

docs/_config.yml

@@ -0,0 +1,54 @@
+# Welcome to Jekyll!
+#
+# This config file is meant for settings that affect your whole blog, values
+# which you are expected to set up once and rarely edit after that. If you find
+# yourself editing this file very often, consider using Jekyll's data files
+# feature for the data you need to update frequently.
+#
+# For technical reasons, this file is *NOT* reloaded automatically when you use
+# 'bundle exec jekyll serve'. If you change this file, please restart the server process.
+#
+# If you need help with YAML syntax, here are some quick references for you:
+# https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml
+# https://learnxinyminutes.com/docs/yaml/
+#
+# Site settings
+# These are used to personalize your new site. If you look in the HTML files,
+# you will see them accessed via {{ site.title }}, {{ site.email }}, and so on.
+# You can create any custom variable you would like, and they will be accessible
+# in the templates via {{ site.myvariable }}.
+
+title: The Fermat's Last Theorem for Exponent 3
+#email: your-email@example.com
+description: A formalisation of the proof of the Fermat's Last Theorem for exponent 3 in Lean 4
+baseurl: "" # the subpath of your site, e.g. /blog
+url: "https://github.com/pitmonticone/FLT3" # the base hostname & protocol for your site, e.g. http://example.com
+#twitter_username: jekyllrb
+github_username: pitmonticone
+repository: pitmonticone/FLT3
+
+# Build settings
+remote_theme: pages-themes/cayman@v0.2.0
+plugins:
+  - jekyll-remote-theme
+
+markdown: kramdown
+# Exclude from processing.
+# The following items will not be processed, by default.
+# Any item listed under the `exclude:` key here will be automatically added to
+# the internal "default list".
+#
+# Excluded items can be processed by explicitly listing the directories or
+# their entries' file path in the `include:` list.
+#
+# exclude:
+#   - .sass-cache/
+#   - .jekyll-cache/
+#   - gemfiles/
+#   - Gemfile
+#   - Gemfile.lock
+#   - node_modules/
+#   - vendor/bundle/
+#   - vendor/cache/
+#   - vendor/gems/
+#   - vendor/ruby/

docs/index.md

@@ -0,0 +1,11 @@
+---
+# Feel free to add content and custom Front Matter to this file.
+# To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults
+
+# layout: home
+usemathjax: true
+---
+
+{% include mathjax.html %}
+
+# The Fermat's Last Theorem for Exponent 3

lake-manifest.json

@@ -63,6 +63,15 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "FLT3",
  "lakeDir": ".lake"}

lakefile.lean

@@ -33,3 +33,9 @@ lean_lib «FLT3» where
   moreLeanArgs := moreLeanArgs
   weakLeanArgs := weakLeanArgs
   -- add any library configuration options here
+
+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"