-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Initial setup of the blueprint, docs and the project page
- Loading branch information
Showing
29 changed files
with
1,368 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,113 @@ | ||
on: | ||
push: | ||
branches: | ||
- master | ||
- blueprint | ||
|
||
# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,41 @@ | ||
# reconstruction | ||
Formalisation of the proof of the 'germs' version of the reconstruction theorem | ||
# Reconstruction | ||
|
||
[![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: | ||
|
||
``` | ||
sudo apt install graphviz libgraphviz-dev | ||
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. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
*.paux | ||
*.aux | ||
*.log | ||
web | ||
__pycache__ | ||
*.fdb_latexmk | ||
*.fls | ||
*.out | ||
*.synctex.gz | ||
*.xdv | ||
*.maf | ||
*.mtc | ||
*.mtc0 | ||
build |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
$pdf_mode = 1; | ||
$pdflatex = 'xelatex -synctex=1 -output-directory=../print/'; | ||
@default_files = ('print.tex'); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
% 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{\N}{\mathbb{N}} | ||
|
||
\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}}} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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}{} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
Oops, something went wrong.