Skip to content

Commit 1ccf053

Browse files
jcreedcmujcreedcmu
committed
Setup blueprint
1 parent 361b323 commit 1ccf053

File tree

21 files changed

+827
-11
lines changed

21 files changed

+827
-11
lines changed

‎.github/workflows/blueprint.yml‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
name: Compile blueprint
2+
3+
on:
4+
push:
5+
branches:
6+
- main # Trigger on pushes to the default branch
7+
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
8+
9+
# Cancel previous runs if a new commit is pushed to the same PR or branch
10+
concurrency:
11+
group: ${{ github.ref }} # Group runs by the ref (branch or PR)
12+
cancel-in-progress: true # Cancel any ongoing runs in the same group
13+
14+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
15+
permissions:
16+
contents: read # Read access to repository contents
17+
pages: write # Write access to GitHub Pages
18+
id-token: write # Write access to ID tokens
19+
20+
jobs:
21+
build_project:
22+
runs-on: ubuntu-latest
23+
name: Build project
24+
steps:
25+
- name: Checkout project
26+
uses: actions/checkout@v4
27+
with:
28+
fetch-depth: 0 # Fetch all history for all branches and tags
29+
30+
- name: Install elan
31+
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
32+
33+
- name: Get Mathlib cache
34+
run: ~/.elan/bin/lake exe cache get || true
35+
36+
- name: Build project
37+
run: ~/.elan/bin/lake build BlueprintDebug
38+
39+
- name: Cache API docs
40+
uses: actions/cache@v4
41+
with:
42+
path: |
43+
.lake/build/doc/Aesop
44+
.lake/build/doc/Batteries
45+
.lake/build/doc/find
46+
.lake/build/doc/Init
47+
.lake/build/doc/Lake
48+
.lake/build/doc/Lean
49+
.lake/build/doc/Mathlib
50+
.lake/build/doc/Std
51+
key: Docs-${{ hashFiles('lake-manifest.json') }}
52+
53+
- name: Build project API documentation
54+
run: ~/.elan/bin/lake -R -Kenv=dev build BlueprintDebug:docs
55+
56+
- name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
57+
id: check_home_page
58+
run: |
59+
if [ -d home_page ]; then
60+
echo "The 'home_page' folder exists in the repository."
61+
echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
62+
else
63+
echo "The 'home_page' folder does not exist in the repository."
64+
echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
65+
fi
66+
67+
- name: Build blueprint and copy to `home_page/blueprint`
68+
uses: xu-cheng/texlive-action@v2
69+
with:
70+
docker_image: ghcr.io/xu-cheng/texlive-full:20250101
71+
run: |
72+
# Install necessary dependencies and build the blueprint
73+
apk update
74+
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
75+
git config --global --add safe.directory $GITHUB_WORKSPACE
76+
git config --global --add safe.directory `pwd`
77+
python3 -m venv env
78+
source env/bin/activate
79+
pip install --upgrade pip requests wheel
80+
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
81+
pip install leanblueprint
82+
leanblueprint pdf
83+
mkdir -p home_page
84+
cp blueprint/print/print.pdf home_page/blueprint.pdf
85+
leanblueprint web
86+
cp -r blueprint/web home_page/blueprint
87+
88+
- name: Check declarations mentioned in the blueprint exist in Lean code
89+
run: |
90+
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
91+
92+
- name: Copy API documentation to `home_page/docs`
93+
run: cp -r .lake/build/doc home_page/docs
94+
95+
- name: Remove unnecessary lake files from documentation in `home_page/docs`
96+
run: |
97+
find home_page/docs -name "*.trace" -delete
98+
find home_page/docs -name "*.hash" -delete
99+
100+
- name: Bundle dependencies
101+
uses: ruby/setup-ruby@v1
102+
with:
103+
working-directory: home_page
104+
ruby-version: "3.0" # Specify Ruby version
105+
bundler-cache: true # Enable caching for bundler
106+
107+
- name: Build website using Jekyll
108+
if: env.HOME_PAGE_EXISTS == 'true'
109+
working-directory: home_page
110+
env:
111+
JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
112+
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
113+
114+
- name: "Upload website (API documentation, blueprint and any home page)"
115+
uses: actions/upload-pages-artifact@v3
116+
with:
117+
path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
118+
119+
- name: Deploy to GitHub Pages
120+
id: deployment
121+
uses: actions/deploy-pages@v4
122+
123+
- name: Make sure the API documentation cache works
124+
run: mv home_page/docs .lake/build/doc
125+

‎blueprint/src/blueprint.sty‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
\DeclareOption*{}
2+
\ProcessOptions
3+
4+
\newcommand{\graphcolor}[3]{}

‎blueprint/src/content.tex‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
% In this file you should put the actual content of the blueprint.
2+
% It will be used both by the web and the print version.
3+
% It should *not* include the \begin{document}
4+
%
5+
% If you want to split the blueprint content into several files then
6+
% the current file can be a simple sequence of \input. Otherwise It
7+
% can start with a \section or \chapter for instance.

‎blueprint/src/extra_styles.css‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
/* This file contains CSS tweaks for this blueprint.
2+
* As an example, we included CSS rules that put
3+
* a vertical line on the left of theorem statements
4+
* and proofs.
5+
* */
6+
7+
div.theorem_thmcontent {
8+
border-left: .15rem solid black;
9+
}
10+
11+
div.proposition_thmcontent {
12+
border-left: .15rem solid black;
13+
}
14+
15+
div.lemma_thmcontent {
16+
border-left: .1rem solid black;
17+
}
18+
19+
div.corollary_thmcontent {
20+
border-left: .1rem solid black;
21+
}
22+
23+
div.proof_content {
24+
border-left: .08rem solid grey;
25+
}

‎blueprint/src/latexmkrc‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# This file configures the latexmk command you can use to compile
2+
# the pdf version of the blueprint
3+
$pdf_mode = 1;
4+
$pdflatex = 'xelatex -synctex=1';
5+
@default_files = ('print.tex');

‎blueprint/src/macros/common.tex‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
% In this file you should put all LaTeX macros and settings to be used both by
2+
% the pdf version and the web version.
3+
% This should be most of your macros.
4+
5+
% The theorem-like environments defined below are those that appear by default
6+
% in the dependency graph. See the README of leanblueprint if you need help to
7+
% customize this.
8+
% The configuration below use the theorem counter for all those environments
9+
% (this is what the [theorem] arguments mean) and never resets it.
10+
% If you want for instance to number them within chapters then you can add
11+
% [chapter] at the end of the next line.
12+
\newtheorem{theorem}{Theorem}
13+
\newtheorem{proposition}[theorem]{Proposition}
14+
\newtheorem{lemma}[theorem]{Lemma}
15+
\newtheorem{corollary}[theorem]{Corollary}
16+
17+
\theoremstyle{definition}
18+
\newtheorem{definition}[theorem]{Definition}

‎blueprint/src/macros/print.tex‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
% In this file you should put macros to be used only by
2+
% the printed version. Of course they should have a corresponding
3+
% version in macros/web.tex.
4+
% Typically the printed version could have more fancy decorations.
5+
% This should be a very short file.
6+
%
7+
% This file starts with dummy macros that ensure the pdf
8+
% compiler will ignore macros provided by plasTeX that make
9+
% sense only for the web version, such as dependency graph
10+
% macros.
11+
12+
13+
% Dummy macros that make sense only for web version.
14+
\newcommand{\lean}[1]{}
15+
\newcommand{\discussion}[1]{}
16+
\newcommand{\leanok}{}
17+
\newcommand{\mathlibok}{}
18+
\newcommand{\notready}{}
19+
% Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
20+
% latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
21+
% It uses LaTeX3 programming, this is why we use the expl3 package.
22+
\ExplSyntaxOn
23+
\NewDocumentCommand{\uses}{m}
24+
{\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
25+
\ignorespaces}
26+
\NewDocumentCommand{\proves}{m}
27+
{\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
28+
\ignorespaces}
29+
\ExplSyntaxOff

‎blueprint/src/macros/web.tex‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
% In this file you should put macros to be used only by
2+
% the web version. Of course they should have a corresponding
3+
% version in macros/print.tex.
4+
% Typically the printed version could have more fancy decorations.
5+
% This will probably be a very short file.

‎blueprint/src/plastex.cfg‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
[general]
2+
renderer=HTML5
3+
copy-theme-extras=yes
4+
plugins=plastexdepgraph plastexshowmore leanblueprint
5+
6+
[document]
7+
toc-depth=3
8+
toc-non-files=True
9+
10+
[files]
11+
directory=../web/
12+
split-level= 0
13+
14+
[html5]
15+
localtoc-level=0
16+
extra-css=extra_styles.css
17+
mathjax-dollars=False

‎blueprint/src/print.tex‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
% This file makes a printable version of the blueprint
2+
% It should include all the \usepackage needed for the pdf version.
3+
% The template version assume you want to use a modern TeX compiler
4+
% such as xeLaTeX or luaLaTeX including support for unicode
5+
% and Latin Modern Math font with standard bugfixes applied.
6+
% It also uses expl3 in order to support macros related to the dependency graph.
7+
% It also includes standard AMS packages (and their improved version
8+
% mathtools) as well as support for links with a sober decoration
9+
% (no ugly rectangles around links).
10+
% It is otherwise a very minimal preamble (you should probably at least
11+
% add cleveref and tikz-cd).
12+
13+
\documentclass[a4paper]{report}
14+
15+
\usepackage{geometry}
16+
17+
\usepackage{expl3}
18+
19+
\usepackage{amssymb, amsthm, mathtools}
20+
\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}
21+
22+
\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
23+
24+
\input{macros/common}
25+
\input{macros/print}
26+
27+
\title{Blueprint Debug}
28+
\author{Jason Reed}
29+
30+
\begin{document}
31+
\maketitle
32+
\input{content}
33+
\end{document}

0 commit comments

Comments
 (0)
⚡