Initial setup of the blueprint, docs and the project page

.github/workflows/push.yml

@@ -0,0 +1,112 @@
+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 Reconstruction -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 Reconstruction -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: Print files to upstream
+        run: |
+          grep -r --files-without-match 'import Reconstruction' Reconstruction | sort > 1.txt
+          grep -r --files-with-match 'sorry' Reconstruction | sort > 2.txt
+          mkdir -p docs/_includes
+          comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/hairer\/Reconstruction\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
+          rm 1.txt 2.txt
+
+      - 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 Reconstruction
+
+      - 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
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build Reconstruction:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          scheme: full
+          run: |
+            apk update
+            apk add --update make py3-pip git
+            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 pip install --upgrade pip requests wheel
+            python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install -r blueprint/requirements.txt
+            python3 -m pip install invoke
+            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
+
+      - name: Make sure the cache works
+        run: |
+          mv docs/docs .lake/build/doc

.github/workflows/push_pr.yml

@@ -0,0 +1,38 @@
+on:
+  pull_request:
+  push:
+    branches-ignore:
+      - master
+
+jobs:
+  style_lint:
+    name: Lint style
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check for long lines
+        if: always()
+        run: |
+          ! (find Reconstruction -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 Reconstruction -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 exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake build Reconstruction

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 *.olean
+.lake

README.md

@@ -1,2 +1,51 @@
 # reconstruction
-Formalisation of the proof of the 'germs' version of the reconstruction theorem
+
+[![Website](https://img.shields.io/badge/Website-ready-green)](https://hairer.github.io/reconstruction/) [![Documentation](https://img.shields.io/badge/Documentation-passing-green)](https://hairer.github.io/reconstruction/docs/) [![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://hairer.github.io/reconstruction/blueprint/)  [![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://hairer.github.io/reconstruction/blueprint.pdf) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/hairer/reconstruction)
+
+Formalisation of the proof of the 'germs' version of the reconstruction 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:
+
+```
+# On Ubuntu
+sudo apt install graphviz libgraphviz-dev
+# On Mac
+brew install graphviz
+```
+
+For other systems, see [PyGraphviz: Install](https://pygraphviz.github.io/documentation/stable/install.html).
+
+Then, you need to install the Python dependencies:
+
+```
+pip uninstall -y leanblueprint
+pip install -r blueprint/requirements.txt
+```
+
+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.
+
+Or you can just run `inv dev` instead of `inv all` and `inv serve`, after each edit to the LaTeX,
+it will automatically rebuild the blueprint, you just need to refresh the web page to see the rendered result.
+
+Note: If you have something wrong in your LaTeX file, and the LaTeX compilation fails,
+LaTeX will stuck and ask for commands, you'll need to type `X` then return to exit LaTeX,
+then fix the LaTeX error, and run `inv dev` again.
+

Reconstruction.lean

@@ -1 +1,8 @@
-def hello := "world"
+def one := 1
+
+def two := 2
+
+theorem one_plus_one_eq_two : one + one = two := by
+  rfl
+
+def one_plus_one_eq_two_with_def : Prop := one + one = two

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,6 @@
+# https://github.com/pyinvoke/invoke/issues/891
+invoke==2.2.0
+plasTeX @ git+https://github.com/plastex/plastex.git
+leanblueprint @ git+https://github.com/PatrickMassot/leanblueprint.git
+watchfiles==0.16.1
+pandoc==2.3

blueprint/src/chapter/intro.tex

@@ -0,0 +1,48 @@
+\chapter{Introduction}
+\label{chap:intro}
+
+\def\R{\mathbb{R}}
+\def\CD{\mathcal{D}}
+\def\s{\mathfrak{s}}
+
+Formalisation of the proof of the 'germs' version of the reconstruction theorem.
+Throughout we fix the following ingredients and notations.
+\begin{itemize}
+\item A Euclidean space $E = \R^d$ endowed with a scaling $\s \in \R_+^d$.
+\item Given $x \in E$ and $\lambda \in \R_+$, we write $\lambda x$ for the vector with components
+$\lambda^{\s_i} x_i$.
+\item We write $\CD$ for the space of 
+\end{itemize}
+
+
+\begin{definition}[One]
+\label{one}
+\lean{one}
+\leanok
+
+
+\end{definition}
+
+\begin{definition}[Two]
+\label{two}
+\lean{two}
+\leanok
+
+    two is 2.
+
+\end{definition}
+
+\begin{lemma}[One plus one is two]
+\label{one_plus_one_eq_two}
+\lean{one_plus_one_eq_two}
+\uses{one, two}
+\leanok
+
+one + one = two
+
+\end{lemma}
+
+\begin{proof}
+\leanok
+It is obvious.
+\end{proof}

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/intro}

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