Basic properties of the flat modality

.github/workflows/ci.yaml

@@ -118,13 +118,22 @@ jobs:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
+      # Install Python and friends for website generation only where needed
+      - uses: actions/setup-python@v4
+        with:
+          python-version: '3.8'
+          check-latest: true
+          cache: 'pip'
+
+      - run: python3 -m pip install -r master/scripts/requirements.txt
+
       - uses: actions/cache/restore@v3
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
 
       # Tell mdbook to use only the linkcheck backend
-      - name: Check website links
+      - name: Check website links and bibtex references
         env:
           MDBOOK_OUTPUT: '{"linkcheck":{}}'
         run: |

.vscode/settings.json

@@ -106,6 +106,9 @@
 
   "[python]": {
     "editor.tabSize": 4,
-    "editor.defaultFormatter": "ms-python.python"
+    "editor.defaultFormatter": null,
+    "editor.formatOnSave": false,
+    "editor.formatOnType": false,
+    "editor.formatOnPaste": false
   }
 }

CITING-SOURCES.md

@@ -0,0 +1,41 @@
+# Citing sources
+
+All of the references and sources of the agda-unimath library are managed in a
+[BibLaTeX](https://www.ctan.org/pkg/biblatex) file `references.bib`, and we have
+a custom set of macros to work with them.
+
+The macros are as follows:
+
+<!--
+We have inserted an invisible whitespace character between the first and second
+opening curly braces in the below examples to block the citation preprocessor
+from detecting them as macros.
+-->
+
+- `{­{#cite referenceXYZ}}` will insert a citation to the reference labeled
+  `referenceXYZ` (which must be defined in the `references.bib` file) at the
+  current location, and add that reference to the current page's bibliography.
+- `{­{#reference referenceXYZ}}` will add the reference labeled `referenceXYZ`
+  to the current page's bibliography without inserting a citation.
+- `{­{#bibliography}}` is a marker for where the bibliography of the current
+  page should be inserted. If no such marker is found and the bibliography is
+  inhabited, it will be inserted at the bottom of the page in a new section
+  titled `References`.
+
+Note that entries in the BibLaTeX file are expected to have all of the
+apropriate fields defined according to their type. For instance, `@book`s _must_
+have a defined field for `publisher` and `year`. If this information is not
+available, please define them as empty fields. E.g. `publisher = {},`.
+
+If you are unsure about how to structure your BibLaTeX entry, it may be useful
+to know that the references are checked by the `linkcheck` GitHub workflow, so
+when you post your pull request to `agda-unimath` you can refer to the CI for
+possible issues.
+
+**Note:** If the citation label of your reference is not being generated
+properly, we support a custom `citeas` field that can be used to overwrite it.
+For instance, _Homotopy Type Theory: Univalent Foundations of Mathematics_
+should be cited as {{#cite UF13}}, and to make it so we have set
+`citeas = {UF13}` for its BibLaTeX entry. Keep in mind that if the citation
+label is not being generated properly, then it is likely that the author list is
+not being parsed properly either.

HOWTO-INSTALL.md

@@ -21,8 +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. The python libraries `pre-commit`, `requests` and `tomli`. Those can be
-   installed by running
+4. The python libraries `pre-commit`, `pybtex`, `requests` and `tomli`. Those
+   can be installed by running
    ```shell
    python3 -m pip install -r scripts/requirements.txt
    ```

Makefile

@@ -34,6 +34,7 @@ TIME ?= time
 METAFILES := \
 	ART.md \
 	CITE-THIS-LIBRARY.md \
+	CITING-SOURCES.md \
 	CODINGSTYLE.md \
 	CONTRIBUTING.md \
 	CONTRIBUTORS.md \
@@ -49,7 +50,7 @@ METAFILES := \
 	STATEMENT-OF-INCLUSION.md \
 	SUMMARY.md \
 	TEMPLATE.lagda.md \
-	USERS.md \
+	USERS.md
 
 .PHONY: agdaFiles
 agdaFiles:

README.md

@@ -15,3 +15,4 @@ welcome contributions to the library about any topic in mathematics.
 1. [The agda-unimath website](https://unimath.github.io/agda-unimath/)
 2. [Discord](https://discord.gg/Zp2e8hYsuX)
 3. [Twitch](https://www.twitch.tv/agdaunimath)
+4. [Benchmarks](https://agda-unimath-benchmarks.netlify.app/)

TEMPLATE.lagda.md

@@ -50,9 +50,3 @@ concept-subconcept = ...
 
 - An instructive example of a file with the expected structure is
   [`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).
-
-## References
-
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
-   of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
-   [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))

book.toml

@@ -51,6 +51,14 @@ output-file = "docs/concept_index.json"
 mathswitch-template = "https://mathswitch.xyz/concept/Wd/{wikidata_id}"
 wikidata-template = "https://www.wikidata.org/entity/{wikidata_id}"
 
+[preprocessor.citations]
+command = "python3 ./scripts/preprocessor_citations.py"
+bibtex_file = "references.bib"
+citation_style = "alpha"
+citation_label_style = "custom_alpha"
+error_on_unmatched_keys = true
+before = [ "git-metadata" ]
+
 [output.linkcheck]
 follow-web-links = false
 
@@ -62,6 +70,7 @@ additional-css = [
   "website/css/Agda.css",
   "website/css/Agda-highlight.css",
   "website/css/agda-logo.css",
+  "website/css/bibliography.css",
   "theme/catppuccin.css",
   "theme/catppuccin-admonish.css",
   "theme/pagetoc.css",

flake.nix

@@ -24,6 +24,7 @@
           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
+            pybtex
             requests
             tomli
           ]);
@@ -74,6 +75,7 @@
               python
               # pre-commit checks
               pkgs.pre-commit
+              pkgs.nodejs
             ] ++ (with pkgs-mdbook; [
               # working on the website
               mdbook