Merge branch 'master' into functor-categories

.github/workflows/ci.yaml

@@ -71,6 +71,17 @@ jobs:
           path: master/_build
           key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
 
+      # Install Python and friends for website generation only where needed
+      - uses: actions/setup-python@v4
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        with:
+          python-version: '3.8'
+          check-latest: true
+          cache: 'pip'
+
+      - run: python3 -m pip install -r master/scripts/requirements.txt
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+
       # We need to run the sources through Agda not only to get the highlighting
       # (which is irrelevant for checking links), but because it flattens the
       # directory structure to a format which is expected in the links we write.
@@ -150,7 +161,7 @@ jobs:
 
       - uses: actions/setup-python@v4
         with:
-          python-version: '3.11.1'
+          python-version: '3.8'
           check-latest: true
           cache: 'pip'
 

.github/workflows/pages.yaml

@@ -40,10 +40,8 @@ jobs:
         uses: actions/checkout@v3
         with:
           path: master
-
-      - uses: r-lib/actions/setup-pandoc@v2
-        with:
-          pandoc-version: '3.0.1'
+          # We need the entire history for contributor information
+          fetch-depth: 0
 
       - name: Setup Agda
         uses: wenkokke/setup-agda@v2.0.0
@@ -88,13 +86,15 @@ jobs:
 
       - uses: actions/setup-python@v4
         with:
-          python-version: '3.11.1'
+          python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r master/scripts/requirements.txt
 
       - name: Generate book
+        env:
+          MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE: 'true'
         run: |
           cd master
           make website

.gitignore

@@ -419,10 +419,13 @@ node_modules/*
 .rvmrc
 package-lock.json
 
-# mdbook
+# mdbook, automatically generated files
 docs/
 html/
 book/
 src/temp/
 src/everything.lagda.md
 SUMMARY.md
+CONTRIBUTORS.md
+MAINTAINERS.md
+/website/css/Agda-highlight.css

.pre-commit-config.yaml

@@ -101,6 +101,7 @@ repos:
     hooks:
       - id: autopep8
         name: Python scripts formatting
+        args: ['-i', '--global-config', '/dev/null']
 
   - repo: https://github.com/pre-commit/mirrors-prettier
     rev: 'v3.0.0-alpha.6'

ART.md

@@ -2,7 +2,7 @@
 
 <div align="center" style="margin: 2em 0;">
   <figure>
-    <img src="agda-unimath-black-and-gold.png" alt="The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023" width="95%" style="border-radius: 10px;">
+    <img src="website/images/agda-unimath-black-and-gold.png" alt="The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023" width="95%" style="border-radius: 10px;">
     <figcaption>The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023</figcaption>
   </figure>
 </div>

HOME.md

@@ -5,7 +5,7 @@ at formalizing mathematics from a univalent point of view using the dependently
 typed programming language [Agda](https://github.com/agda/agda).
 
 <a href="https://github.com/unimath/agda-unimath">
-<img align="right" width="300" alt="agda-unimath" src="agda-unimath-logo.svg" />
+<img class="invertible-image" align="right" width="300" alt="agda-unimath" src="website/images/agda-unimath-logo.svg" />
 </a>
 
 The library project was created by Elisabeth Bonnevier, Jonathan Prieto-Cubides,
@@ -34,7 +34,3 @@ Follow the instructions in our [installation guide](HOWTO-INSTALL.md) to set up
 the project. After you have completed your formalization, submit it via a pull
 request. We will review your contribution and work towards incorporating it into
 the `agda-unimath` library.
-
-{{#include SUMMARY.md}}
-
-{{#include CONTRIBUTORS.md}}

HOWTO-INSTALL.md

@@ -21,7 +21,8 @@ In order to contribute to the `agda-unimath` library you will additionally need:
 1. `git`
 2. `make`
 3. `python` version 3.8 or newer
-4. `pre-commit` and `request`. Those two programs can be installed by running
+4. The python libraries `pre-commit`, `requests` and `tomli`. Those can be
+   installed by running
    ```shell
    python3 -m pip install -r scripts/requirements.txt
    ```

Makefile

@@ -5,6 +5,7 @@ AGDAVERBOSE ?= -v1
 # use "$ export AGDAVERBOSE=20" if you want to see all
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)
 AGDAMDFILES := $(subst src/,docs/,$(AGDAFILES:.lagda.md=.md))
+CONTRIBUTORS_FILE := ./scripts/contributors_data.toml
 
 AGDAHTMLFLAGS ?= --html --html-highlight=code --html-dir=docs --css=Agda.css --only-scope-checking
 AGDA ?= agda $(AGDAVERBOSE)
@@ -68,14 +69,25 @@ agda-html: ./src/everything.lagda.md
 	@mkdir -p ./docs/
 	@${AGDA} ${AGDAHTMLFLAGS} ./src/everything.lagda.md
 
-SUMMARY.md: ${AGDAFILES}
+SUMMARY.md: ${AGDAFILES} ./scripts/generate_main_index_file.py
 	@python3 ./scripts/generate_main_index_file.py
 
+MAINTAINERS.md: ${CONTRIBUTORS_FILE} ./scripts/generate_maintainers.py
+	@python3 ./scripts/generate_maintainers.py
+
+CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./scripts/generate_contributors.py
+	@python3 ./scripts/generate_contributors.py
+
+website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppuccin.css
+	@python3 ./scripts/generate_agda_css.py
+
 .PHONY: website-prepare
-website-prepare: agda-html ./SUMMARY.md
+website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md ./website/css/Agda-highlight.css
 	@cp $(METAFILES) ./docs/
-	@cp ./theme/images/agda-unimath-logo.svg ./docs/
-	@cp ./theme/images/agda-unimath-black-and-gold.png ./docs/
+	@mkdir -p ./docs/website
+	@cp -r ./website/images ./docs/website/
+	@cp -r ./website/css ./docs/website/
+	@cp -r ./website/js ./docs/website/
 
 .PHONY: website
 website: website-prepare

book.toml

@@ -6,6 +6,7 @@ title = "agda-unimath"
 
 [build]
 create-missing = true
+
 [preprocessor.index]
 
 [preprocessor.links]
@@ -18,28 +19,58 @@ static-css = false
 include-src = false
 block-delimiter = {left = "$$", right = "$$"}
 inline-delimiter = {left = "$", right = "$"}
-macros = "theme/latex-macros.txt"
+macros = "website/latex-macros.txt"
 
 [preprocessor.catppuccin]
 assets_version = "0.2.1" # DO NOT EDIT: Managed by `mdbook-catppuccin install`
 
+[preprocessor.git-metadata]
+command = "python3 ./scripts/preprocessor_git_metadata.py"
+# Disable by default - it takes a non-trivial amount of time
+# Can be overriden by running
+# `export MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE=true` in your shell
+enable = false
+# Only show "Content created by" on Agda source files
+attribute_file_extensions = [ ".lagda.md" ]
+# Don't add anything to the "non-content" pages,
+# i.e. top-level markdown files which aren't guides
+suppress_processing = [
+  "HOME.md",
+  "MAINTAINERS.md",
+  "CONTRIBUTORS.md",
+  "STATEMENT-OF-INCLUSION",
+  "USERS.md",
+  "GRANT-ACKNOWLEDGEMENTS.md",
+  "SUMMARY.md",
+  "ART.md"
+]
+
 [output.linkcheck]
 follow-web-links = false
 
 [output.html]
 default-theme = "light"
 preferred-dark-theme = "Ayu"
 copy-fonts = true
-additional-css = ["theme/Agda.css", "theme/pagetoc.css", "theme/agda-logo.css", "./theme/catppuccin.css", "./theme/catppuccin-highlight.css"]
-additional-js = ["theme/js/custom.js", "theme/pagetoc.js"]
+additional-css = [
+  "website/css/Agda.css",
+  "website/css/Agda-highlight.css",
+  "website/css/agda-logo.css",
+  "theme/catppuccin.css",
+  "theme/catppuccin-highlight.css",
+  "theme/pagetoc.css",
+]
+additional-js = [
+  "website/js/custom.js",
+  "theme/pagetoc.js"
+]
 no-section-label = false
 site-url = "/agda-unimath/"
 git-repository-url = "https://github.com/UniMath/agda-unimath"
 git-repository-icon = "fa-github"
 
 [output.html.print]
-enable = true    # include support for printable output
-page-break = true # insert page-break after each chapter
+enable = false
 
 [output.html.fold]
 enable = true    # whether or not to enable section folding

flake.nix

@@ -18,7 +18,9 @@
           pkgs = nixpkgs.legacyPackages."${system}";
           python = pkgs.python38.withPackages (p: with p; [
             # Keep in sync with scripts/requirements.txt
+            # pre-commit <- not installed as a Python package but as a binary below
             requests
+            tomli
           ]);
 
           agda-unimath-package = { lib, mkDerivation, time }: mkDerivation {