diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml new file mode 100644 index 0000000..666406a --- /dev/null +++ b/.github/workflows/blueprint.yml @@ -0,0 +1,89 @@ +on: + push: + branches: + - main + +# 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: Get cache + run: ~/.elan/bin/lake exe cache get || true + + - name: Build project + run: ~/.elan/bin/lake build OrderedSemigroups + + - 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-OrderedSemigroups* + key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} + restore-keys: | + MathlibDoc- + + - name: Build documentation + run: ~/.elan/bin/lake -R -Kenv=dev build OrderedSemigroups: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/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty new file mode 100644 index 0000000..1353f39 --- /dev/null +++ b/blueprint/src/blueprint.sty @@ -0,0 +1,2 @@ +\DeclareOption*{} +\ProcessOptions \ No newline at end of file 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..668fec1 --- /dev/null +++ b/blueprint/src/macros/print.tex @@ -0,0 +1,29 @@ +% 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}{} +\newcommand{\notready}{} +% 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..1c8eb80 --- /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{OrderedSemigroups} +\author{Eric P} + +\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..c641e56 --- /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://ericluap.github.io/OrderedSemigroups} +\github{https://github.com/ericluap/OrderedSemigroups} +\dochome{https://ericluap.github.io/OrderedSemigroups/docs} + +\title{OrderedSemigroups} +\author{Eric P} + +\begin{document} +\maketitle +\input{content} +\end{document} \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index ff6e9c2..3247318 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -70,6 +70,56 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "9148a0a7506099963925cf239c491fcda5ed0044", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f93115d0209de6db335725dee900d379f40c0317", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, "configFile": "lakefile.lean"}], "name": "ordered_semigroups", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 8b7ad29..49f9aba 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,3 +14,9 @@ require mathlib from git @[default_target] lean_lib «OrderedSemigroups» where -- 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