try adding blueprint

.github/workflows/push.yml

@@ -0,0 +1,97 @@
+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:
+  style_lint:
+    name: Lint style
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check for long lines
+        if: always()
+        run: |
+          ! (find Carleson -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+
+      - name: Don't 'import Mathlib', use precise imports
+        if: always()
+        run: |
+          ! (find Carleson -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
+
+  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.0.0
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build Carleson
+
+      - name: Cache mathlib docs
+        uses: actions/cache@v3
+        with:
+          path: .lake/build/doc/Mathlib
+          key: DocGen4-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            DocGen4-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build Carleson:docs
+
+      - name: Install Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.9'
+          cache: 'pip' # caching pip dependencies
+
+      - name: Install blueprint apt dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+
+      - name: Install blueprint dependencies
+        run: |
+          cd blueprint && pip install -r requirements.txt
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        run: |
+          inv all
+
+      - name: Copy documentation to `docs/docs`
+        run: |
+          mv .lake/build/doc docs/docs
+
+      - name: Bundle dependencies
+        uses: ruby/setup-ruby@v1
+        with:
+          working-directory: docs
+          ruby-version: "3.0" # Not needed with a .ruby-version file
+          bundler-cache: true # runs 'bundle install' and caches installed gems automatically
+
+      - name: Bundle website
+        working-directory: docs
+        run: JEKYLL_ENV=production bundle exec jekyll build
+
+      - name: Upload docs & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/_site
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1

.github/workflows/push_pr.yml

@@ -0,0 +1,21 @@
+on:
+  pull_request:
+
+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.0.0
+
+      - name: Get cache
+        run: ~/.elan/bin/lake exe cache get
+
+      - name: Build project
+        run: ~/.elan/bin/lake build Carleson

README.md

@@ -3,10 +3,35 @@ A (WIP) formalized proof of Carleson's theorem in Lean
 
 ## Contribute
 
-To get the repository, make sure you have [installed Lean](https://leanprover-community.github.io/get_started.html). Then get the repository using `git clone https://github.com/fpvandoorn/carleson.git` and run `lake exe cache get` inside the repository. See the README of [my course repository](https://github.com/fpvandoorn/LeanCourse23) for more detailed instructions.
+To get the repository, make sure you have [installed Lean](https://leanprover-community.github.io/get_started.html). Then get the repository using `git clone https://github.com/fpvandoorn/carleson.git` and run `lake exe cache get` inside the repository. Run `lake build` to build all files in this repository. See the README of [my course repository](https://github.com/fpvandoorn/LeanCourse23) for more detailed instructions.
 
 To publish your changes on Github, you need to be added as a contributor to this repository. Make a Github account if you don't have one already and send your Github account per email to Floris. I will add you.
 
 To push your changes, the easiest method is to use the `Source Control` panel in VSCode.
 Feel free to push unfinished code and code that is work in progress, but make sure that the file(s)
-you've worked have no errors (having `sorry`'s is of course fine).
+you've worked have no errors (having `sorry`'s is of course fine).
+
+## Build the blueprint
+
+To build the web version of the blueprint, you need a working LaTeX installation.
+Furthermore, you need some packages:
+```
+sudo apt install graphviz libgraphviz-dev
+pip3 install invoke pandoc
+cd .. # go to folder where you are happy clone git repos
+git clone [email protected]:plastex/plastex
+pip3 install ./plastex
+git clone [email protected]:PatrickMassot/leanblueprint
+pip3 install ./leanblueprint
+cd sphere-eversion
+```
+
+To actually build the blueprint, run
+```
+lake exe cache get
+lake build
+inv all
+```
+
+To view the web-version of the blueprint locally, run `inv serve` and navigate to
+`http://localhost:8000/` in your favorite browser.

blueprint/.gitignore

@@ -0,0 +1,16 @@
+*.pdf
+*.paux
+*.aux
+*.log
+print
+web
+__pycache__
+*.fdb_latexmk
+*.fls
+*.out
+*.synctex.gz
+*.xdv
+*.maf
+*.mtc
+*.mtc0
+build

blueprint/requirements.txt

@@ -0,0 +1,4 @@
+invoke==1.7.1
+plasTeX @ git+https://github.com/plastex/plastex.git
+leanblueprint @ git+https://github.com/utensil/leanblueprint.git@lean4-only
+watchfiles==0.16.1

blueprint/src/chapter/jensen.tex

@@ -0,0 +1,7 @@
+\chapter{Test}
+
+In this chapter, $h$ denotes the function $h(x) := x \log \frac{1}{x}$ for $x \in [0,1]$.
+
+\begin{lemma}[Concavity]\label{concave}
+  $h$ is strictly concave on $[0,1]$.
+\end{lemma}

blueprint/src/chapter/main.tex

@@ -0,0 +1,5 @@
+% This is the main point of entry to the blueprint.
+% Add chapters of the blueprint here.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
+
+\input{chapter/jensen}

blueprint/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;
+}

blueprint/src/latexmkrc

@@ -0,0 +1,3 @@
+$pdf_mode = 1;  
+$pdflatex = 'xelatex -synctex=1 -output-directory=../print/';
+@default_files = ('print.tex');

blueprint/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

blueprint/src/preamble/common.tex

@@ -0,0 +1,34 @@
+% Put any macro and import needed for the project here.
+% This will be used by both the web and print versions of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
+
+% Letters
+\newcommand{\C}{\mathbb{C}}
+\newcommand{\bbc}{\mathbb{C}}
+\newcommand{\E}{\mathbb{E}}
+\newcommand*{\bbe}{\mathbb{E}}
+\newcommand{\F}{\mathbb{F}}
+\newcommand{\bbf}{\mathbb{F}}
+\newcommand{\bbH}{\mathbb{H}}
+\newcommand{\bbP}{\mathbb{P}}
+\newcommand{\bbI}{\mathbb{I}}
+\newcommand{\bbn}{\mathbb{N}}
+\newcommand{\bbq}{\mathbb{Q}}
+\newcommand{\bbr}{\mathbb{R}}
+\newcommand{\bbt}{\mathbb{T}}
+\newcommand{\bbz}{\mathbb{Z}}
+
+\newcommand{\lo}[1]{\mathcal{L}{#1}}
+
+% Paired delimiters
+\newcommand{\abs}[1]{\left\lvert #1\right\rvert}
+\newcommand{\Abs}[1]{\lvert #1 \rvert}
+\newcommand{\brac}[1]{\left( #1\right)}
+\newcommand{\norm}[1]{\lVert #1\rVert}
+\newcommand{\inn}[1]{\left\langle #1 \right\rangle}
+
+% Operators
+\DeclareMathOperator{\dist}{dist}
+
+\newcommand{\ind}[1]{1_{#1}}
+\providecommand{\tup}[1]{{\vec{#1}}}

blueprint/src/preamble/print.tex

@@ -0,0 +1,16 @@
+% Those macros are used for the print version of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
+
+\declaretheorem[numberwithin=chapter]{theorem}
+\declaretheorem[sibling=theorem]{proposition}
+\declaretheorem[sibling=theorem]{corollary}
+\declaretheorem[sibling=theorem]{remark}
+\declaretheorem[sibling=theorem]{lemma}
+\declaretheorem[sibling=theorem]{definition}
+\declaretheorem[sibling=theorem]{example}
+
+% We neutralise the Plastex commands
+\newcommand{\uses}[1]{}
+\newcommand{\proves}[1]{}
+\newcommand{\lean}[1]{}
+\newcommand{\leanok}{}

blueprint/src/preamble/web.tex

@@ -0,0 +1,11 @@
+% Those macros are used for the web version of the blueprint.
+% This file is not meant to be built. Build src/web.tex or src/print.text instead.
+
+\newtheorem{theorem}{Theorem}[chapter]
+\newtheorem{definition}[theorem]{Definition}
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{sublemma}[theorem]{Sub-lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{remark}[theorem]{Remark}
+\newtheorem{example}[theorem]{Example}

blueprint/src/print.tex

@@ -0,0 +1,40 @@
+% This file makes a printable version of the blueprint
+
+\documentclass[a4paper]{report}
+
+\usepackage[textwidth=14cm]{geometry}
+\usepackage{xfrac}
+\usepackage{polyglossia}
+\setdefaultlanguage{english}
+
+\usepackage{amsmath,amssymb}
+\usepackage{enumitem}
+\usepackage{hyperref}
+
+\usepackage{tikz-cd}
+
+\usepackage{mathtools}
+\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
+\usepackage{fontspec}
+\setmathfont{Latin Modern Math}
+\setmathfont[range=\varnothing]{Asana-Math.otf}
+\setmathfont[range=\pitchfork]{Asana-Math.otf}
+\setmathfont[range=\intprod]{Asana-Math.otf}
+\setmathfont[range=\int]{Latin Modern Math}
+
+\usepackage[nameinlink, capitalize]{cleveref}
+
+\usepackage{amsthm}
+\usepackage{etexcmds}
+\usepackage{thmtools}
+
+\input{preamble/common}
+\input{preamble/print}
+
+\title{Carleson's Theorem Blueprint}
+\author{Terence Tao}
+
+\begin{document}
+\maketitle
+\input{chapter/main}
+\end{document}