From 24751b4ec33b59c9d4ff8759fa703bb5c50ba8a0 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 30 Jul 2024 18:45:20 +0200 Subject: [PATCH] Update --- .github/workflows/blueprint.yml | 123 -------------------------------- blueprint/src/blueprint.sty | 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 | 29 -------- blueprint/src/macros/web.tex | 5 -- blueprint/src/plastex.cfg | 17 ----- blueprint/src/print.tex | 33 --------- blueprint/src/web.tex | 27 ------- 11 files changed, 276 deletions(-) delete mode 100644 .github/workflows/blueprint.yml delete mode 100644 blueprint/src/blueprint.sty delete mode 100644 blueprint/src/content.tex delete mode 100644 blueprint/src/extra_styles.css delete mode 100644 blueprint/src/latexmkrc delete mode 100644 blueprint/src/macros/common.tex delete mode 100644 blueprint/src/macros/print.tex delete mode 100644 blueprint/src/macros/web.tex delete mode 100644 blueprint/src/plastex.cfg delete mode 100644 blueprint/src/print.tex delete mode 100644 blueprint/src/web.tex diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml deleted file mode 100644 index 65e65a4..0000000 --- a/.github/workflows/blueprint.yml +++ /dev/null @@ -1,123 +0,0 @@ -name: Generate Blueprint - -# Trigger the workflow on push events to the main / master branch -on: - push: - branches: ["main"] # Trigger on pushes to the "main" branch (replace "main" with your default branch if different) - workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface - -# Set permissions for the workflow -permissions: - contents: read # Read access to repository contents - pages: write # Write access to GitHub Pages - id-token: write # Write access to ID tokens - -jobs: - build_project: - runs-on: ubuntu-latest - name: Build project - steps: - - name: Checkout project - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all branches and tags - - - name: Install elan - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - - - name: Get cache - run: ~/.elan/bin/lake -Kenv=dev exe cache get || true - - - name: Build project - run: ~/.elan/bin/lake -Kenv=dev build Project - - - name: Cache mathlib documentation - uses: actions/cache@v4 - 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/find - .lake/build/doc/*.* - !.lake/build/doc/declarations/declaration-data-Project* - key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - restore-keys: MathlibDoc- - - - name: Build project documentation - run: ~/.elan/bin/lake -Kenv=dev build Project:docs - - - name: Check for existing `docs` folder - id: check_docs - run: | - if [ -d docs ]; then - echo "The 'docs' folder already exists in the repository." - echo "DOCS_EXIST=true" >> $GITHUB_ENV - else - echo "The 'docs' folder does not exist in the repository." - echo "DOCS_EXIST=false" >> $GITHUB_ENV - fi - - - 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: | - # Install necessary dependencies and build the blueprint - export PIP_BREAK_SYSTEM_PACKAGES=1 - 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 - if [ ! -d docs ]; then mkdir docs; fi - 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: Copy documentation to `docs/docs` - run: | - # Change ownership and copy documentation to the docs directory - sudo chown -R runner docs - cp -r .lake/build/doc docs/docs - - - name: Remove lake files from documentation in `docs/docs` - run: | - # Remove unnecessary trace and hash files from the documentation - find docs/docs -name "*.trace" -delete - find docs/docs -name "*.hash" -delete - - - name: Bundle dependencies - uses: ruby/setup-ruby@v1 - with: - working-directory: docs - ruby-version: "3.0" # Specify Ruby version - bundler-cache: true # Enable caching for bundler - - - name: Bundle website - if: env.DOCS_EXIST == 'true' - working-directory: docs - run: JEKYLL_ENV=production bundle exec jekyll build # Build the website using Jekyll - - - name: Upload docs & blueprint artifact - uses: actions/upload-pages-artifact@v3 - with: - path: ${{ env.DOCS_EXIST == 'true' && 'docs/_site' || 'docs/' }} - - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@v4 # Deploy the site to GitHub Pages - - - name: Make sure the cache works - run: mv docs/docs .lake/build/doc # Verify that the cache is functioning correctly \ No newline at end of file diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty deleted file mode 100644 index 1353f39..0000000 --- a/blueprint/src/blueprint.sty +++ /dev/null @@ -1,2 +0,0 @@ -\DeclareOption*{} -\ProcessOptions \ No newline at end of file diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex deleted file mode 100644 index b5cd27b..0000000 --- a/blueprint/src/content.tex +++ /dev/null @@ -1,7 +0,0 @@ -% 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 deleted file mode 100644 index b96c776..0000000 --- a/blueprint/src/extra_styles.css +++ /dev/null @@ -1,25 +0,0 @@ -/* 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 deleted file mode 100644 index 38d5963..0000000 --- a/blueprint/src/latexmkrc +++ /dev/null @@ -1,5 +0,0 @@ -# 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 deleted file mode 100644 index 131c9f8..0000000 --- a/blueprint/src/macros/common.tex +++ /dev/null @@ -1,3 +0,0 @@ -% 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 deleted file mode 100644 index 668fec1..0000000 --- a/blueprint/src/macros/print.tex +++ /dev/null @@ -1,29 +0,0 @@ -% 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 deleted file mode 100644 index ceee975..0000000 --- a/blueprint/src/macros/web.tex +++ /dev/null @@ -1,5 +0,0 @@ -% 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 deleted file mode 100644 index de3dbae..0000000 --- a/blueprint/src/plastex.cfg +++ /dev/null @@ -1,17 +0,0 @@ -[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 deleted file mode 100644 index a87ed60..0000000 --- a/blueprint/src/print.tex +++ /dev/null @@ -1,33 +0,0 @@ -% 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{Project} -\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 deleted file mode 100644 index a61b177..0000000 --- a/blueprint/src/web.tex +++ /dev/null @@ -1,27 +0,0 @@ -% 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/LeanProject} -\github{https://github.com/pitmonticone/LeanProject} -\dochome{https://pitmonticone.github.io/LeanProject/docs} - -\title{Project} -\author{Pietro Monticone} - -\begin{document} -\maketitle -\input{content} -\end{document} \ No newline at end of file