From 57ab23f6d36b2f0381068234ae935e4b660645ee Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 22 Mar 2024 13:54:53 +0100 Subject: [PATCH] try adding blueprint --- .github/workflows/push.yml | 97 ++++++++++ .github/workflows/push_pr.yml | 21 +++ README.md | 29 ++- blueprint/.gitignore | 16 ++ blueprint/requirements.txt | 4 + blueprint/src/chapter/jensen.tex | 7 + blueprint/src/chapter/main.tex | 5 + blueprint/src/extra_styles.css | 53 ++++++ blueprint/src/latexmkrc | 3 + blueprint/src/plastex.cfg | 17 ++ blueprint/src/preamble/common.tex | 34 ++++ blueprint/src/preamble/print.tex | 16 ++ blueprint/src/preamble/web.tex | 11 ++ blueprint/src/print.tex | 40 +++++ blueprint/src/util.sty | 220 +++++++++++++++++++++++ blueprint/src/web.tex | 28 +++ blueprint/tasks.py | 60 +++++++ docs/.bundle/config | 2 + docs/.gitignore | 8 + docs/404.html | 25 +++ docs/Gemfile | 25 +++ docs/Gemfile.lock | 287 ++++++++++++++++++++++++++++++ docs/_config.yml | 54 ++++++ docs/_includes/mathjax.html | 10 ++ docs/_layouts/default.html | 54 ++++++ docs/assets/css/style.scss | 17 ++ docs/index.md | 55 ++++++ scripts/mk_all.sh | 28 +++ scripts/update_mathlib.bat | 4 + scripts/update_mathlib.sh | 4 + tasks.py | 20 +++ 31 files changed, 1252 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/push.yml create mode 100644 .github/workflows/push_pr.yml create mode 100644 blueprint/.gitignore create mode 100644 blueprint/requirements.txt create mode 100644 blueprint/src/chapter/jensen.tex create mode 100644 blueprint/src/chapter/main.tex create mode 100644 blueprint/src/extra_styles.css create mode 100644 blueprint/src/latexmkrc create mode 100644 blueprint/src/plastex.cfg create mode 100644 blueprint/src/preamble/common.tex create mode 100644 blueprint/src/preamble/print.tex create mode 100644 blueprint/src/preamble/web.tex create mode 100644 blueprint/src/print.tex create mode 100644 blueprint/src/util.sty create mode 100644 blueprint/src/web.tex create mode 100644 blueprint/tasks.py create mode 100644 docs/.bundle/config create mode 100644 docs/.gitignore create mode 100644 docs/404.html create mode 100644 docs/Gemfile create mode 100644 docs/Gemfile.lock create mode 100644 docs/_config.yml create mode 100644 docs/_includes/mathjax.html create mode 100644 docs/_layouts/default.html create mode 100644 docs/assets/css/style.scss create mode 100644 docs/index.md create mode 100644 scripts/mk_all.sh create mode 100644 scripts/update_mathlib.bat create mode 100644 scripts/update_mathlib.sh create mode 100644 tasks.py diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml new file mode 100644 index 00000000..964f9d72 --- /dev/null +++ b/.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 diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml new file mode 100644 index 00000000..e596e0a6 --- /dev/null +++ b/.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 diff --git a/README.md b/README.md index be57d95e..78fe4bc5 100644 --- a/README.md +++ b/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). \ No newline at end of file +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 git@github.com:plastex/plastex +pip3 install ./plastex +git clone git@github.com: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. \ No newline at end of file diff --git a/blueprint/.gitignore b/blueprint/.gitignore new file mode 100644 index 00000000..a50e5c81 --- /dev/null +++ b/blueprint/.gitignore @@ -0,0 +1,16 @@ +*.pdf +*.paux +*.aux +*.log +print +web +__pycache__ +*.fdb_latexmk +*.fls +*.out +*.synctex.gz +*.xdv +*.maf +*.mtc +*.mtc0 +build diff --git a/blueprint/requirements.txt b/blueprint/requirements.txt new file mode 100644 index 00000000..3bdadebf --- /dev/null +++ b/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 diff --git a/blueprint/src/chapter/jensen.tex b/blueprint/src/chapter/jensen.tex new file mode 100644 index 00000000..773b6b84 --- /dev/null +++ b/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} diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex new file mode 100644 index 00000000..2e9868e0 --- /dev/null +++ b/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} diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css new file mode 100644 index 00000000..10e84bf9 --- /dev/null +++ b/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; +} diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc new file mode 100644 index 00000000..a2fe40cd --- /dev/null +++ b/blueprint/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/plastex.cfg b/blueprint/src/plastex.cfg new file mode 100644 index 00000000..e2fa0832 --- /dev/null +++ b/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 diff --git a/blueprint/src/preamble/common.tex b/blueprint/src/preamble/common.tex new file mode 100644 index 00000000..c0ca82b6 --- /dev/null +++ b/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}}} diff --git a/blueprint/src/preamble/print.tex b/blueprint/src/preamble/print.tex new file mode 100644 index 00000000..013b983e --- /dev/null +++ b/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}{} diff --git a/blueprint/src/preamble/web.tex b/blueprint/src/preamble/web.tex new file mode 100644 index 00000000..dcd75d11 --- /dev/null +++ b/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} diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex new file mode 100644 index 00000000..7b20ea0b --- /dev/null +++ b/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} diff --git a/blueprint/src/util.sty b/blueprint/src/util.sty new file mode 100644 index 00000000..f4aefd7c --- /dev/null +++ b/blueprint/src/util.sty @@ -0,0 +1,220 @@ +\ProvidesPackage{util} + +%%%%%%%%%%%%%%%%%%%%% + +% A very opinionated utility package providing a ton of environments and packages for LaTeX files. + +%%%%%%%%%%%%%%%%%%%%% + +\newif\if@compilingfullbook +\DeclareOption{book}{\@compilingfullbooktrue} + +\ProcessOptions\relax + +\usepackage[UKenglish]{babel} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage[a4paper]{geometry} % , margin=20mm +\usepackage{textcomp} % makes the "not defining \perthousand"/"\micro" errors go away by including this first +%\newcommand\hmmax{0} +%\newcommand\bmmax{0} +\usepackage{mathpazo} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{amsfonts} +\usepackage{bbm} +\usepackage{wrapfig} +\usepackage{physics} +\usepackage{bm} +\usepackage{tgpagella} +\DeclareDocumentCommand\mathbf{m}{\bm{\mathrm{#1}}} % make bold work for greek symbols +\DeclareDocumentCommand\vnabla{}{\nabla} % use non-bold nabla for \grad, \curl etc. +% Enabled to unify laplacian symbol between vector and scalar forms +\DeclareDocumentCommand\dotproduct{}{\cdot} % use non-bold dot for scalar product to unify notation +\DeclareDocumentCommand\crossproduct{}{\times} % use non-bold dot for scalar product to unify notation +\usepackage{gensymb} +\usepackage[shortlabels]{enumitem} +\setlist[enumerate,1]{label={(\roman*)}} +\setlist[enumerate,2]{label={(\alph*)}} +\usepackage{mathtools} +\mathtoolsset{mathic} +\usepackage{centernot} +\usepackage{relsize} +\usepackage{mathrsfs} +\usepackage{siunitx} +\usepackage{booktabs} +\usepackage[ruled,vlined]{algorithm2e} +\usepackage{array} +\usepackage{multirow} +% todo: remove \noindent and such now that parskip is enabled +\usepackage[parfill]{parskip} +\usepackage{pgfplots} +\pgfplotsset{width=10cm,compat=1.9} +\usepgfplotslibrary{external} + +\usepackage{etoolbox} +\usepackage{tikz-cd} +\usetikzlibrary{external} +\usetikzlibrary{cd} + +\usepackage{minitoc} +\usepackage{faktor} % TODO: convert group quotients to this style +\usepackage{scalerel} +\usepackage{microtype} +\usepackage[breakable]{tcolorbox} + +\usepackage[pdfa]{hyperref} +\hypersetup{ + colorlinks=true, + linktoc=all, + linkcolor=green!40!black, +} + +\numberwithin{equation}{section} % make equations be numbered 1.1 not 1 + +\newcommand{\tableofcontentsnewpage}{\tableofcontents\newpage} + +% increase spacing between toc number and title +\makeatletter +\renewcommand{\l@subsection}{\@dottedtocline{2}{1.8em}{3.2em}} +\makeatother + +% create the theorem environments +\theoremstyle{definition} +\newtheorem*{definition}{Definition} + +\newtheorem*{claim}{Claim} +\newtheorem*{theorem}{Theorem} +\newtheorem*{proposition}{Proposition} +\newtheorem*{lemma}{Lemma} +\newtheorem*{corollary}{Corollary} +\newtheorem*{example}{Example} % todo: convert `as an example...' to the example environment +\newtheorem*{param}{Model parameters} +\newtheorem*{ih}{Inductive hypothesis} + +\theoremstyle{remark} +\newtheorem*{note}{Note} +\newtheorem*{remark}{Remark} + +\definecolor{lemma_col}{RGB}{170, 217, 255} +\definecolor{thm_col}{RGB}{255, 196, 215} +\definecolor{def_col}{RGB}{120, 232, 190} +\definecolor{param_col}{RGB}{206, 120, 232} +\definecolor{ih_col}{RGB}{232, 191, 120} + +% we don't have `frame hidden` since we can't use `skins` from tcolorbox withou compile errors +\tcolorboxenvironment{definition}{colback=def_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{claim}{colback=lemma_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{proposition}{colback=lemma_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{lemma}{colback=lemma_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{corollary}{colback=lemma_col!30,colframe=white,breakable,arc=0mm} +%\tcolorboxenvironment{example}{colback=green!10,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{theorem}{colback=thm_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{param}{colback=param_col!30,colframe=white,breakable,arc=0mm} +\tcolorboxenvironment{ih}{colback=ih_col!30,colframe=white,breakable,arc=0mm} + +\newcommand{\ddempty}{\mathrm{d}} +\newcommand{\dn}[2]{\mathrm{d}^#1#2} +\newcommand{\st}{\text{ s.t. + }} +\newcommand{\contradiction}{\(\#\)} +\newcommand{\genset}[1]{\left\langle{} #1 \right\rangle} +\newcommand{\ngenset}[1]{\left\langle\!\left\langle{} #1 \right\rangle\!\right\rangle} +\newcommand{\midd}{\,\middle|\,} +\newcommand{\nhat}{\vu{n}} +\newcommand{\rdot}{\dot{\vb{r}}} +\newcommand{\rddot}{\ddot{\vb{r}}} +\newcommand{\transpose}{\intercal} +\newcommand{\acts}{\curvearrowright} +\newcommand{\adjugate}[1]{\widetilde{#1}} +\newcommand{\mathhuge}[1]{\mathlarger{\mathlarger{\mathlarger{#1}}}} +\newcommand{\stcomp}[1]{{#1}^c} % consider \complement? +% Personally I think this looks better, and it's what Wikipedia uses +\newcommand{\prob}[1]{\mathbb{P}\left({#1}\right)} +\newcommand{\psub}[2]{\mathbb{P}_{#1}\left({#2}\right)} +\newcommand{\psubx}[1]{\psub{x}{#1}} +\newcommand{\expect}[1]{\mathbb{E}\left[{#1}\right]} +\newcommand{\esub}[2]{\mathbb{E}_{#1}\left[{#2}\right]} +\newcommand{\esubx}[1]{\esub{x}{#1}} +\newcommand{\Var}[1]{\Varop\left({#1}\right)} +\newcommand{\Varsub}[2]{\Varop_{#1}\left({#2}\right)} +\newcommand{\Cov}[1]{\Covop\left({#1}\right)} +\newcommand{\Corr}[1]{\Corrop\left({#1}\right)} +\newcommand{\convdist}{\xrightarrow{d}} +\newcommand{\convprob}{\xrightarrow{\mathbb{P}}} +\newcommand{\wildcard}{{}\cdot{}} +\newcommand{\inner}[1]{\left\langle{#1}\right\rangle} +\newcommand{\Markov}[1]{\Markovop\left({#1}\right)} +\newcommand{\sstar}{{\star\star}} +\newcommand{\connect}{\mathbin{\#}} +\newcommand{\Mob}{\text{M\"ob}} +\newcommand{\Chat}{\widehat{\mathbb C}} +\newcommand{\bound}{\ooalign{\hidewidth$\partial$\hidewidth\cr/}} +\newcommand{\hhat}[1]{\hat{\hat{#1}}} +\DeclareMathOperator*{\bigconnect}{\scalerel*{\#}{\textstyle\sum}} + +\DeclareMathOperator{\vecspan}{span} +\DeclareMathOperator{\HCF}{HCF} +\DeclareMathOperator{\LCM}{LCM} +\DeclareMathOperator{\ord}{ord} +\DeclareMathOperator{\Sym}{Sym} +\DeclareMathOperator{\nullity}{null} +\DeclareMathOperator{\Orb}{Orb} +\DeclareMathOperator{\Stab}{Stab} +\DeclareMathOperator{\ccl}{ccl} +\DeclareMathOperator{\Varop}{Var} +\DeclareMathOperator{\Covop}{Cov} +\DeclareMathOperator{\Corrop}{Corr} +\DeclareMathOperator{\Markovop}{Markov} +\DeclareMathOperator{\adj}{adj} +\DeclareMathOperator{\sgn}{sgn} +\DeclareMathOperator{\diam}{diam} +\DeclareMathOperator{\id}{id} +\DeclareMathOperator{\Log}{Log} +\DeclareMathOperator{\Iff}{\mathrm{I}} +\DeclareMathOperator{\IIff}{\mathrm{I\!I}} +\DeclareMathOperator{\artanh}{artanh} +\DeclareMathOperator{\Aut}{Aut} +\DeclareMathOperator{\Hom}{Hom} +\DeclareMathOperator{\graft}{graft} +\DeclareMathOperator{\Gal}{Gal} +\DeclareMathOperator{\Instr}{Instr} +\DeclareMathOperator*{\esssup}{ess\ sup} +\DeclareMathOperator{\dom}{dom} +\DeclareMathOperator{\fchar}{char} +\DeclareMathOperator{\code}{code} +\DeclareMathOperator{\coker}{coker} + +\DeclarePairedDelimiter\ceil{\lceil}{\rceil} +\DeclarePairedDelimiter\floor{\lfloor}{\rfloor} +\DeclarePairedDelimiter\Brackets{[\![}{]\!]} + +% for arrows in the middle of the line +\usetikzlibrary{decorations.markings} +\tikzset{->-/.style={decoration={ + markings, + mark=at position #1 with {\arrow{>}}},postaction={decorate}}} +\usetikzlibrary{automata} +\usetikzlibrary{positioning} + +\ifdefined\hideproofs +\usepackage{environ} +\usepackage{calc} +\usepackage{pgf} +\newlength{\parline} +\newlength{\paroutindent} +\newlength{\lineheight} +\setlength{\lineheight}{\heightof{abcdefghijklmnoprstuvwxyz}} +\NewEnviron{killproof}{% +\setlength{\paroutindent}{\expandafter\parindent}% +\setlength{\parline}{\heightof{\noindent\begin{minipage}{\linewidth}% + \setlength{\parindent}{\paroutindent}% + \BODY% + \end{minipage}}}% +\pgfmathparse{int(round(\parline / (0.9*\lineheight)))}% +\textit{Proof hidden (approx.\ \pgfmathresult{} lines).\\} +} +\let\proof\killproof +\let\endproof\endkillproof +\fi diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex new file mode 100644 index 00000000..17e19a0e --- /dev/null +++ b/blueprint/src/web.tex @@ -0,0 +1,28 @@ +% This file makes the web version of the blueprint. +% This file can be built locally. + +\documentclass{report} + +\usepackage{amsmath,amsfonts,amsthm,amssymb} +\usepackage{hyperref} +\usepackage{graphicx} +\DeclareGraphicsExtensions{.svg,.png,.jpg} +\usepackage[capitalize]{cleveref} +\usepackage[showmore, dep_graph, project=../../]{blueprint} + +\usepackage{tikz-cd} +\usepackage{tikz} + +\input{preamble/common} +\input{preamble/web} + +\github{https://github.com/fpvandoorn/carleson} +\dochome{https://fpvandoorn.github.io/carleson/docs} + +\title{Carleson} +\author{} + +\begin{document} +\maketitle +\input{chapter/main} +\end{document} diff --git a/blueprint/tasks.py b/blueprint/tasks.py new file mode 100644 index 00000000..23807328 --- /dev/null +++ b/blueprint/tasks.py @@ -0,0 +1,60 @@ +import os +import random +from pathlib import Path +import http.server +import socketserver + +from invoke import run, task + +BP_DIR = Path(__file__).parent + +@task +def print_bp(ctx): + cwd = os.getcwd() + os.chdir(BP_DIR) + run('mkdir -p print && cd src && xelatex -output-directory=../print print.tex') + os.chdir(cwd) + +@task +def bp(ctx): + cwd = os.getcwd() + os.chdir(BP_DIR) + run('mkdir -p print && cd src && xelatex -output-directory=../print print.tex') + run('cd src && xelatex -output-directory=../print print.tex') + os.chdir(cwd) + +@task +def bptt(ctx): + """ + Build the blueprint PDF file with tectonic and prepare src/web.bbl for task `web` + + NOTE: install tectonic by running `curl --proto '=https' --tlsv1.2 -fsSL https://drop-sh.fullyjustified.net |sh` in + `~/.local/bin/` + """ + + cwd = os.getcwd() + os.chdir(BP_DIR) + run('mkdir -p print && cd src && tectonic -Z shell-escape-cwd=. --keep-intermediates --outdir ../print print.tex') + # run('cp print/print.bbl src/web.bbl') + os.chdir(cwd) + +@task +def web(ctx): + cwd = os.getcwd() + os.chdir(BP_DIR/'src') + run('plastex -c plastex.cfg web.tex') + os.chdir(cwd) + +@task +def serve(ctx, random_port=False): + cwd = os.getcwd() + os.chdir(BP_DIR/'web') + Handler = http.server.SimpleHTTPRequestHandler + if random_port: + port = random.randint(8000, 8100) + print("Serving on port " + str(port)) + else: + port = 8000 + httpd = socketserver.TCPServer(("", port), Handler) + httpd.serve_forever() + os.chdir(cwd) diff --git a/docs/.bundle/config b/docs/.bundle/config new file mode 100644 index 00000000..23692288 --- /dev/null +++ b/docs/.bundle/config @@ -0,0 +1,2 @@ +--- +BUNDLE_PATH: "vendor/bundle" diff --git a/docs/.gitignore b/docs/.gitignore new file mode 100644 index 00000000..e4b7ba1a --- /dev/null +++ b/docs/.gitignore @@ -0,0 +1,8 @@ +_site +.sass-cache +.jekyll-cache +.jekyll-metadata +vendor +blueprint/ +blueprint.pdf +docs/ diff --git a/docs/404.html b/docs/404.html new file mode 100644 index 00000000..086a5c9e --- /dev/null +++ b/docs/404.html @@ -0,0 +1,25 @@ +--- +permalink: /404.html +layout: default +--- + + + +
+

404

+ +

Page not found :(

+

The requested page could not be found.

+
diff --git a/docs/Gemfile b/docs/Gemfile new file mode 100644 index 00000000..a6a5bb05 --- /dev/null +++ b/docs/Gemfile @@ -0,0 +1,25 @@ +source "https://rubygems.org" + +# To upgrade, run `bundle update github-pages`. +gem "github-pages", group: :jekyll_plugins +# If you have any plugins, put them here! +group :jekyll_plugins do + #gem "jekyll-feed", "~> 0.12" +end + +# Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem +# and associated library. +platforms :mingw, :x64_mingw, :mswin, :jruby do + gem "tzinfo", "~> 1.2" + gem "tzinfo-data" +end + +# Performance-booster for watching directories on Windows. +gem "wdm", "~> 0.1.1", :platforms => [:mingw, :x64_mingw, :mswin] + +# Lock `http_parser.rb` gem to `v0.6.x` on JRuby builds since newer versions of the gem +# do not have a Java counterpart. +gem "http_parser.rb", "~> 0.6.0", :platforms => [:jruby] + +# Used for locally serving the website. +gem "webrick", "~> 1.7" diff --git a/docs/Gemfile.lock b/docs/Gemfile.lock new file mode 100644 index 00000000..0239bd65 --- /dev/null +++ b/docs/Gemfile.lock @@ -0,0 +1,287 @@ +GEM + remote: https://rubygems.org/ + specs: + activesupport (6.0.5) + concurrent-ruby (~> 1.0, >= 1.0.2) + i18n (>= 0.7, < 2) + minitest (~> 5.1) + tzinfo (~> 1.1) + zeitwerk (~> 2.2, >= 2.2.2) + addressable (2.8.0) + public_suffix (>= 2.0.2, < 5.0) + coffee-script (2.4.1) + coffee-script-source + execjs + coffee-script-source (1.11.1) + colorator (1.1.0) + commonmarker (0.23.4) + concurrent-ruby (1.1.10) + dnsruby (1.61.9) + simpleidn (~> 0.1) + em-websocket (0.5.3) + eventmachine (>= 0.12.9) + http_parser.rb (~> 0) + ethon (0.15.0) + ffi (>= 1.15.0) + eventmachine (1.2.7) + execjs (2.8.1) + faraday (1.10.0) + faraday-em_http (~> 1.0) + faraday-em_synchrony (~> 1.0) + faraday-excon (~> 1.1) + faraday-httpclient (~> 1.0) + faraday-multipart (~> 1.0) + faraday-net_http (~> 1.0) + faraday-net_http_persistent (~> 1.0) + faraday-patron (~> 1.0) + faraday-rack (~> 1.0) + faraday-retry (~> 1.0) + ruby2_keywords (>= 0.0.4) + faraday-em_http (1.0.0) + faraday-em_synchrony (1.0.0) + faraday-excon (1.1.0) + faraday-httpclient (1.0.1) + faraday-multipart (1.0.3) + multipart-post (>= 1.2, < 3) + faraday-net_http (1.0.1) + faraday-net_http_persistent (1.2.0) + faraday-patron (1.0.0) + faraday-rack (1.0.0) + faraday-retry (1.0.3) + ffi (1.15.5) + forwardable-extended (2.6.0) + gemoji (3.0.1) + github-pages (226) + github-pages-health-check (= 1.17.9) + jekyll (= 3.9.2) + jekyll-avatar (= 0.7.0) + jekyll-coffeescript (= 1.1.1) + jekyll-commonmark-ghpages (= 0.2.0) + jekyll-default-layout (= 0.1.4) + jekyll-feed (= 0.15.1) + jekyll-gist (= 1.5.0) + jekyll-github-metadata (= 2.13.0) + jekyll-include-cache (= 0.2.1) + jekyll-mentions (= 1.6.0) + jekyll-optional-front-matter (= 0.3.2) + jekyll-paginate (= 1.1.0) + jekyll-readme-index (= 0.3.0) + jekyll-redirect-from (= 0.16.0) + jekyll-relative-links (= 0.6.1) + jekyll-remote-theme (= 0.4.3) + jekyll-sass-converter (= 1.5.2) + jekyll-seo-tag (= 2.8.0) + jekyll-sitemap (= 1.4.0) + jekyll-swiss (= 1.0.0) + jekyll-theme-architect (= 0.2.0) + jekyll-theme-cayman (= 0.2.0) + jekyll-theme-dinky (= 0.2.0) + jekyll-theme-hacker (= 0.2.0) + jekyll-theme-leap-day (= 0.2.0) + jekyll-theme-merlot (= 0.2.0) + jekyll-theme-midnight (= 0.2.0) + jekyll-theme-minimal (= 0.2.0) + jekyll-theme-modernist (= 0.2.0) + jekyll-theme-primer (= 0.6.0) + jekyll-theme-slate (= 0.2.0) + jekyll-theme-tactile (= 0.2.0) + jekyll-theme-time-machine (= 0.2.0) + jekyll-titles-from-headings (= 0.5.3) + jemoji (= 0.12.0) + kramdown (= 2.3.2) + kramdown-parser-gfm (= 1.1.0) + liquid (= 4.0.3) + mercenary (~> 0.3) + minima (= 2.5.1) + nokogiri (>= 1.13.4, < 2.0) + rouge (= 3.26.0) + terminal-table (~> 1.4) + github-pages-health-check (1.17.9) + addressable (~> 2.3) + dnsruby (~> 1.60) + octokit (~> 4.0) + public_suffix (>= 3.0, < 5.0) + typhoeus (~> 1.3) + html-pipeline (2.14.1) + activesupport (>= 2) + nokogiri (>= 1.4) + http_parser.rb (0.8.0) + i18n (0.9.5) + concurrent-ruby (~> 1.0) + jekyll (3.9.2) + addressable (~> 2.4) + colorator (~> 1.0) + em-websocket (~> 0.5) + i18n (~> 0.7) + jekyll-sass-converter (~> 1.0) + jekyll-watch (~> 2.0) + kramdown (>= 1.17, < 3) + liquid (~> 4.0) + mercenary (~> 0.3.3) + pathutil (~> 0.9) + rouge (>= 1.7, < 4) + safe_yaml (~> 1.0) + jekyll-avatar (0.7.0) + jekyll (>= 3.0, < 5.0) + jekyll-coffeescript (1.1.1) + coffee-script (~> 2.2) + coffee-script-source (~> 1.11.1) + jekyll-commonmark (1.4.0) + commonmarker (~> 0.22) + jekyll-commonmark-ghpages (0.2.0) + commonmarker (~> 0.23.4) + jekyll (~> 3.9.0) + jekyll-commonmark (~> 1.4.0) + rouge (>= 2.0, < 4.0) + jekyll-default-layout (0.1.4) + jekyll (~> 3.0) + jekyll-feed (0.15.1) + jekyll (>= 3.7, < 5.0) + jekyll-gist (1.5.0) + octokit (~> 4.2) + jekyll-github-metadata (2.13.0) + jekyll (>= 3.4, < 5.0) + octokit (~> 4.0, != 4.4.0) + jekyll-include-cache (0.2.1) + jekyll (>= 3.7, < 5.0) + jekyll-mentions (1.6.0) + html-pipeline (~> 2.3) + jekyll (>= 3.7, < 5.0) + jekyll-optional-front-matter (0.3.2) + jekyll (>= 3.0, < 5.0) + jekyll-paginate (1.1.0) + jekyll-readme-index (0.3.0) + jekyll (>= 3.0, < 5.0) + jekyll-redirect-from (0.16.0) + jekyll (>= 3.3, < 5.0) + jekyll-relative-links (0.6.1) + jekyll (>= 3.3, < 5.0) + jekyll-remote-theme (0.4.3) + addressable (~> 2.0) + jekyll (>= 3.5, < 5.0) + jekyll-sass-converter (>= 1.0, <= 3.0.0, != 2.0.0) + rubyzip (>= 1.3.0, < 3.0) + jekyll-sass-converter (1.5.2) + sass (~> 3.4) + jekyll-seo-tag (2.8.0) + jekyll (>= 3.8, < 5.0) + jekyll-sitemap (1.4.0) + jekyll (>= 3.7, < 5.0) + jekyll-swiss (1.0.0) + jekyll-theme-architect (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-cayman (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-dinky (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-hacker (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-leap-day (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-merlot (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-midnight (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-minimal (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-modernist (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-primer (0.6.0) + jekyll (> 3.5, < 5.0) + jekyll-github-metadata (~> 2.9) + jekyll-seo-tag (~> 2.0) + jekyll-theme-slate (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-tactile (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-theme-time-machine (0.2.0) + jekyll (> 3.5, < 5.0) + jekyll-seo-tag (~> 2.0) + jekyll-titles-from-headings (0.5.3) + jekyll (>= 3.3, < 5.0) + jekyll-watch (2.2.1) + listen (~> 3.0) + jemoji (0.12.0) + gemoji (~> 3.0) + html-pipeline (~> 2.2) + jekyll (>= 3.0, < 5.0) + kramdown (2.3.2) + rexml + kramdown-parser-gfm (1.1.0) + kramdown (~> 2.0) + liquid (4.0.3) + listen (3.7.1) + rb-fsevent (~> 0.10, >= 0.10.3) + rb-inotify (~> 0.9, >= 0.9.10) + mercenary (0.3.6) + minima (2.5.1) + jekyll (>= 3.5, < 5.0) + jekyll-feed (~> 0.9) + jekyll-seo-tag (~> 2.1) + minitest (5.15.0) + multipart-post (2.1.1) + nokogiri (1.13.6-x86_64-linux) + racc (~> 1.4) + octokit (4.22.0) + faraday (>= 0.9) + sawyer (~> 0.8.0, >= 0.5.3) + pathutil (0.16.2) + forwardable-extended (~> 2.6) + public_suffix (4.0.7) + racc (1.6.0) + rb-fsevent (0.11.1) + rb-inotify (0.10.1) + ffi (~> 1.0) + rexml (3.2.5) + rouge (3.26.0) + ruby2_keywords (0.0.5) + rubyzip (2.3.2) + safe_yaml (1.0.5) + sass (3.7.4) + sass-listen (~> 4.0.0) + sass-listen (4.0.0) + rb-fsevent (~> 0.9, >= 0.9.4) + rb-inotify (~> 0.9, >= 0.9.7) + sawyer (0.8.2) + addressable (>= 2.3.5) + faraday (> 0.8, < 2.0) + simpleidn (0.2.1) + unf (~> 0.1.4) + terminal-table (1.8.0) + unicode-display_width (~> 1.1, >= 1.1.1) + thread_safe (0.3.6) + typhoeus (1.4.0) + ethon (>= 0.9.0) + tzinfo (1.2.9) + thread_safe (~> 0.1) + unf (0.1.4) + unf_ext + unf_ext (0.0.8.1) + unicode-display_width (1.8.0) + webrick (1.7.0) + zeitwerk (2.5.4) + +PLATFORMS + x86_64-linux + +DEPENDENCIES + github-pages + http_parser.rb (~> 0.6.0) + tzinfo (~> 1.2) + tzinfo-data + wdm (~> 0.1.1) + webrick (~> 1.7) + +BUNDLED WITH + 2.3.14 diff --git a/docs/_config.yml b/docs/_config.yml new file mode 100644 index 00000000..d94df2bd --- /dev/null +++ b/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 Polynomial Freiman-Ruzsa Conjecture +#email: your-email@example.com +description: A digitisation of the proof of the Polynomial Freiman-Ruzsa Conjecture in Lean 4 +baseurl: "" # the subpath of your site, e.g. /blog +url: "https://fpvandoorn.github.io/carleson/" # the base hostname & protocol for your site, e.g. http://example.com +#twitter_username: jekyllrb +github_username: fpvandoorn +repository: fpvandoorn/carleson + +# 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/ diff --git a/docs/_includes/mathjax.html b/docs/_includes/mathjax.html new file mode 100644 index 00000000..136e1d91 --- /dev/null +++ b/docs/_includes/mathjax.html @@ -0,0 +1,10 @@ + +{% if page.usemathjax %} + + +{% endif %} diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html new file mode 100644 index 00000000..45a7f74c --- /dev/null +++ b/docs/_layouts/default.html @@ -0,0 +1,54 @@ + + + + + + + {% seo %} + + + + + + {% if jekyll.environment == "production" %} + + {% else %} + + {% endif %} + {% include head-custom.html %} + + + + + + + +
+ {{ content }} + +
+ {% if site.github.is_project_page %} + {{ site.github.repository_name }} + is maintained by Terence Tao from UCLA and Yaël Dillies from the University of Cambridge. Visit the repository on GitHub for the list of contributors. + {% endif %} +
+
+ + + diff --git a/docs/assets/css/style.scss b/docs/assets/css/style.scss new file mode 100644 index 00000000..efd52163 --- /dev/null +++ b/docs/assets/css/style.scss @@ -0,0 +1,17 @@ +--- +--- + +@import "{{ site.theme }}"; + +.page-header { + background-image: linear-gradient(120deg, #2d4fdc, #dc2ddc); +} + +.main-content h1, +.main-content h2, +.main-content h3, +.main-content h4, +.main-content h5, +.main-content h6 { + color: #6f1599; +} diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 00000000..ae18f4d4 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,55 @@ +--- +# 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 %} + +# Carleson's theorem + +WIP formalization of a generalized Carleson's theorem + + + +## Build the Lean files + +To build the Lean files of this project, you need to have a working version of Lean. +See [the installation instructions](https://leanprover-community.github.io/get_started.html) (under Regular install). + +To build the project, run `lake exe cache get` and then `lake build`. + +## 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 git@github.com:plastex/plastex +pip3 install ./plastex +git clone git@github.com:PatrickMassot/leanblueprint +pip3 install ./leanblueprint +cd sphere-eversion +``` + +To actually build the blueprint, run +``` +lake exe cache get +lake build +inv all +``` + +## Source reference + +`[GGMT]`: + +[GGMT]: https://arxiv.org/abs/2311.05762 diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh new file mode 100644 index 00000000..5e6c1bac --- /dev/null +++ b/scripts/mk_all.sh @@ -0,0 +1,28 @@ +# TODO: This script currently mishandles the $directory argument + +#!/usr/bin/env bash +# Usage: mk_all.sh [subdirectory] +# +# Examples: +# ./scripts/mk_all.sh +# ./scripts/mk_all.sh data/real +# ./scripts/mk_all.sh ../archive +# +# Makes a $directory/../$directory.lean file importing all files inside $directory. +# If $directory is omitted, creates `Carleson.lean`. + +cd "$( dirname "${BASH_SOURCE[0]}" )"/../Carleson +if [[ $# = 1 ]]; then + dir="${1%/}" # remove trailing slash if present +else + dir="." +fi + +# remove an initial `./` +# replace an initial `../test/` with just `.` (similarly for `roadmap`/`archive`/...) +# replace all `/` with `».«` +# replace the `.lean` suffix with `»` +# prepend `import «` +find "$dir" -name \*.lean -not -name Carleson.lean \ + | sed 's,^\./,,;s,^\.\./[^/]*,,;s,/,.,g;s,\.lean$,,;s,^,import Carleson.,' \ + | sort >"$dir"/../Carleson.lean diff --git a/scripts/update_mathlib.bat b/scripts/update_mathlib.bat new file mode 100644 index 00000000..cdeac411 --- /dev/null +++ b/scripts/update_mathlib.bat @@ -0,0 +1,4 @@ +rem Update mathlib and the lean toolchain. +curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain +lake -Kenv=dev update rem The `-Kenv=dev` is making sure we also update doc-gen +lake exe cache get diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh new file mode 100644 index 00000000..ef768d93 --- /dev/null +++ b/scripts/update_mathlib.sh @@ -0,0 +1,4 @@ +# Update mathlib and the lean toolchain. +curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain +lake -Kenv=dev update # The `-Kenv=dev` is making sure we also update doc-gen +lake exe cache get diff --git a/tasks.py b/tasks.py new file mode 100644 index 00000000..a3327295 --- /dev/null +++ b/tasks.py @@ -0,0 +1,20 @@ +import os +import shutil +import subprocess +from pathlib import Path +from invoke import run, task + +from blueprint.tasks import web, bp, print_bp, serve + +ROOT = Path(__file__).parent + +@task(bp, web) +def all(ctx): + shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True) + shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint') + shutil.copy2(ROOT/'blueprint'/'print'/'print.pdf', ROOT/'docs'/'blueprint.pdf') + +@task(web) +def html(ctx): + shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True) + shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')