From 0b18cfe931f8bdfffb64b750c159707ba992c394 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 31 Mar 2024 00:38:17 +0100 Subject: [PATCH] Setup blueprint --- .github/workflows/blueprint.yml | 92 +++++++++++++++++++++++++++++++++ .gitignore | 2 + blueprint/src/content.tex | 7 +++ blueprint/src/extra_styles.css | 25 +++++++++ blueprint/src/latexmkrc | 5 ++ blueprint/src/macros/common.tex | 3 ++ blueprint/src/macros/print.tex | 28 ++++++++++ blueprint/src/macros/web.tex | 5 ++ blueprint/src/plastex.cfg | 17 ++++++ blueprint/src/print.tex | 33 ++++++++++++ blueprint/src/web.tex | 27 ++++++++++ docs/_config.yml | 54 +++++++++++++++++++ docs/index.md | 11 ++++ lake-manifest.json | 9 ++++ lakefile.lean | 6 +++ 15 files changed, 324 insertions(+) create mode 100644 .github/workflows/blueprint.yml create mode 100644 blueprint/src/content.tex create mode 100644 blueprint/src/extra_styles.css create mode 100644 blueprint/src/latexmkrc create mode 100644 blueprint/src/macros/common.tex create mode 100644 blueprint/src/macros/print.tex create mode 100644 blueprint/src/macros/web.tex create mode 100644 blueprint/src/plastex.cfg create mode 100644 blueprint/src/print.tex create mode 100644 blueprint/src/web.tex create mode 100644 docs/_config.yml create mode 100644 docs/index.md diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml new file mode 100644 index 0000000..397fef1 --- /dev/null +++ b/.github/workflows/blueprint.yml @@ -0,0 +1,92 @@ +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: + 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.5.0 + + - name: Update checkdecls + run: ~/.elan/bin/lake update checkdecls + + - name: Get cache + run: ~/.elan/bin/lake -Kenv=dev exe cache get || true + + - name: Build project + run: ~/.elan/bin/lake -Kenv=dev build FLT3 + + - 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 + !.lake/build/doc/declarations/declaration-data-FLT3* + key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + restore-keys: | + MathlibDoc- + + - name: Build documentation + run: ~/.elan/bin/lake -Kenv=dev build FLT3:docs + + - name: Build blueprint and copy to `docs/blueprint` + uses: xu-cheng/texlive-action@v2 + with: + docker_image: ghcr.io/xu-cheng/texlive-full:20231201 + run: | + apk update + 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 venv env + source env/bin/activate + pip install --upgrade pip requests wheel + pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" + pip install leanblueprint + leanblueprint pdf + mkdir docs + cp blueprint/print/print.pdf docs/blueprint.pdf + leanblueprint web + cp -r blueprint/web docs/blueprint + + - name: Check declarations + run: | + ~/.elan/bin/lake exe checkdecls blueprint/lean_decls + + - name: Move documentation to `docs/docs` + run: | + sudo chown -R runner docs + cp -r .lake/build/doc docs/docs + + - name: Upload docs & blueprint artifact + uses: actions/upload-pages-artifact@v1 + with: + path: docs/ + + - 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 \ No newline at end of file diff --git a/.gitignore b/.gitignore index 9f41205..f2517ca 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,5 @@ /lakefile.olean # After v4.3.0-rc2 lake stores its files here: /.lake/ +# Python virtual environment +/.venv/ diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex new file mode 100644 index 0000000..b5cd27b --- /dev/null +++ b/blueprint/src/content.tex @@ -0,0 +1,7 @@ +% In this file you should put the actual content of the blueprint. +% It will be used both by the web and the print version. +% It should *not* include the \begin{document} +% +% If you want to split the blueprint content into several files then +% the current file can be a simple sequence of \input. Otherwise It +% can start with a \section or \chapter for instance. \ No newline at end of file diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css new file mode 100644 index 0000000..b96c776 --- /dev/null +++ b/blueprint/src/extra_styles.css @@ -0,0 +1,25 @@ +/* This file contains CSS tweaks for this blueprint. + * As an example, we included CSS rules that put + * a vertical line on the left of theorem statements + * and proofs. + * */ + +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; +} diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc new file mode 100644 index 0000000..38d5963 --- /dev/null +++ b/blueprint/src/latexmkrc @@ -0,0 +1,5 @@ +# This file configures the latexmk command you can use to compile +# the pdf version of the blueprint +$pdf_mode = 1; +$pdflatex = 'xelatex -synctex=1'; +@default_files = ('print.tex'); \ No newline at end of file diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex new file mode 100644 index 0000000..131c9f8 --- /dev/null +++ b/blueprint/src/macros/common.tex @@ -0,0 +1,3 @@ +% In this file you should put all LaTeX macros to be used +% both by the pdf version and the web version. +% This should be most of your macros. \ No newline at end of file diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex new file mode 100644 index 0000000..e43bf73 --- /dev/null +++ b/blueprint/src/macros/print.tex @@ -0,0 +1,28 @@ +% In this file you should put macros to be used only by +% the printed version. Of course they should have a corresponding +% version in macros/web.tex. +% Typically the printed version could have more fancy decorations. +% This should be a very short file. +% +% This file starts with dummy macros that ensure the pdf +% compiler will ignore macros provided by plasTeX that make +% sense only for the web version, such as dependency graph +% macros. + + +% Dummy macros that make sense only for web version. +\newcommand{\lean}[1]{} +\newcommand{\discussion}[1]{} +\newcommand{\leanok}{} +\newcommand{\mathlibok}{} +% Make sure that arguments of \uses and \proves are real labels, by using invisible refs: +% latex prints a warning if the label is not defined, but nothing is shown in the pdf file. +% It uses LaTeX3 programming, this is why we use the expl3 package. +\ExplSyntaxOn +\NewDocumentCommand{\uses}{m} + {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% + \ignorespaces} +\NewDocumentCommand{\proves}{m} + {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% + \ignorespaces} +\ExplSyntaxOff \ No newline at end of file diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex new file mode 100644 index 0000000..ceee975 --- /dev/null +++ b/blueprint/src/macros/web.tex @@ -0,0 +1,5 @@ +% In this file you should put macros to be used only by +% the web version. Of course they should have a corresponding +% version in macros/print.tex. +% Typically the printed version could have more fancy decorations. +% This will probably be a very short file. \ No newline at end of file diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg new file mode 100644 index 0000000..de3dbae --- /dev/null +++ b/blueprint/src/plastex.cfg @@ -0,0 +1,17 @@ +[general] +renderer=HTML5 +copy-theme-extras=yes +plugins=plastexdepgraph plastexshowmore leanblueprint + +[document] +toc-depth=3 +toc-non-files=True + +[files] +directory=../web/ +split-level= 0 + +[html5] +localtoc-level=0 +extra-css=extra_styles.css +mathjax-dollars=False \ No newline at end of file diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex new file mode 100644 index 0000000..b4b3069 --- /dev/null +++ b/blueprint/src/print.tex @@ -0,0 +1,33 @@ +% This file makes a printable version of the blueprint +% It should include all the \usepackage needed for the pdf version. +% The template version assume you want to use a modern TeX compiler +% such as xeLaTeX or luaLaTeX including support for unicode +% and Latin Modern Math font with standard bugfixes applied. +% It also uses expl3 in order to support macros related to the dependency graph. +% It also includes standard AMS packages (and their improved version +% mathtools) as well as support for links with a sober decoration +% (no ugly rectangles around links). +% It is otherwise a very minimal preamble (you should probably at least +% add cleveref and tikz-cd). + +\documentclass[a4paper]{report} + +\usepackage{geometry} + +\usepackage{expl3} + +\usepackage{amssymb, amsthm, mathtools} +\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref} + +\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math} + +\input{macros/common} +\input{macros/print} + +\title{Fermat's Last Theorem for Exponent 3} +\author{Pietro Monticone} + +\begin{document} +\maketitle +\input{content} +\end{document} \ No newline at end of file diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex new file mode 100644 index 0000000..0e6a204 --- /dev/null +++ b/blueprint/src/web.tex @@ -0,0 +1,27 @@ +% This file makes a web version of the blueprint +% It should include all the \usepackage needed for this version. +% The template includes standard AMS packages. +% It is otherwise a very minimal preamble (you should probably at least +% add cleveref and tikz-cd). + +\documentclass{report} + +\usepackage{amssymb, amsthm, amsmath} +\usepackage{hyperref} +\usepackage[showmore, dep_graph]{blueprint} + + +\input{macros/common} +\input{macros/web} + +\home{https://pitmonticone.github.io/FLT3} +\github{https://github.com/pitmonticone/FLT3} +\dochome{https://pitmonticone.github.io/FLT3/docs} + +\title{Fermat's Last Theorem for Exponent 3} +\author{Pietro Monticone} + +\begin{document} +\maketitle +\input{content} +\end{document} \ No newline at end of file diff --git a/docs/_config.yml b/docs/_config.yml new file mode 100644 index 0000000..703ed9e --- /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 Fermat's Last Theorem for Exponent 3 +#email: your-email@example.com +description: A formalisation of the proof of the Fermat's Last Theorem for exponent 3 in Lean 4 +baseurl: "" # the subpath of your site, e.g. /blog +url: "https://github.com/pitmonticone/FLT3" # the base hostname & protocol for your site, e.g. http://example.com +#twitter_username: jekyllrb +github_username: pitmonticone +repository: pitmonticone/FLT3 + +# 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/ \ No newline at end of file diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..8686492 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,11 @@ +--- +# 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 %} + +# The Fermat's Last Theorem for Exponent 3 \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index b7571a1..3d527cc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -63,6 +63,15 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "rev": "2ee81a0269048010900117b675876a1d8db5883c", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, "configFile": "lakefile.lean"}], "name": "FLT3", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 6eddbc8..a7da164 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -33,3 +33,9 @@ lean_lib «FLT3» where moreLeanArgs := moreLeanArgs weakLeanArgs := weakLeanArgs -- add any library configuration options here + +require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" + +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file