Setup the blueprint

.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 -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build PhiCalculus
+
+      - 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-PhiCalculus*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build PhiCalculus: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 git+https://github.com/PatrickMassot/leanblueprint.git@client
+            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

blueprint/.gitignore

@@ -0,0 +1,2 @@
+web/
+*.paux

blueprint/lean_decls

@@ -0,0 +1,2 @@
+Term
+incLocatorsFrom

blueprint/src/content.tex

@@ -0,0 +1,25 @@
+\chapter{$\varphi$-calculus}
+
+\begin{definition}[$\varphi$-term]
+  \label{phiterm}
+  \lean{Term}\leanok
+  \begin{center}
+    \includegraphics[width=4in]{figures/syntax.png}
+  \end{center}
+\end{definition}
+
+\begin{definition}[Locator Increment]
+  \label{incLocatorsFrom}
+  \lean{incLocatorsFrom}\leanok
+  % \uses{phiterm}
+  \begin{center}
+    \includegraphics[width=2.5in]{figures/increment.png}
+  \end{center}
+ \end{definition}
+
+
+\chapter{Confluence}
+
+\section{Parallel Reduction}
+
+\section{Complete Development}

blueprint/src/plastex.cfg

@@ -0,0 +1,17 @@
+[general]
+renderer=HTML5
+copy-theme-extras=yes
+plugins=plastexdepgraph  plastexshowmore  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

blueprint/src/web.tex

@@ -0,0 +1,30 @@
+\documentclass{report}
+
+\usepackage{amssymb, amsthm, amsmath}
+\usepackage{hyperref}
+\usepackage[showmore, dep_graph]{blueprint}
+
+\usepackage{graphicx}
+
+% \input{macros/common}
+% \input{macros/web}
+
+\home{https://objectionary.github.io/proof}
+\github{https://github.com/objectionary/proof}
+\dochome{https://objectionary.github.io/proof/docs}
+
+\title{Confluence of minimal φ-calculus}
+\author{}
+
+\newtheorem*{definition}{Definition}
+\newtheorem*{theorem}{Theorem}
+\newtheorem*{lemma}{Lemma}
+\newtheorem*{corollary}{Corollary}
+
+% \newcommand{\mkObject}[1]{\llbracket #1 \rrbracket}
+\newcommand{\mkObject}[1]{[[ #1 ]]}
+\newcommand{\inct}[2]{#2\uparrow{}^{#1}}
+\begin{document}
+\maketitle
+\input{content}
+\end{document}

lake-manifest.json

@@ -90,6 +90,15 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "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": "«phi-calculus»",
  "lakeDir": ".lake"}

lakefile.lean

@@ -15,3 +15,5 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 lean_lib PhiCalculus
 
 lean_lib Minimal
+
+require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"