Raise minimal supported Python version to 3.10

.github/workflows/ci.yaml

@@ -89,7 +89,7 @@ jobs:
       # Install Python and friends for website generation only where needed
       - uses: actions/setup-python@v5
         with:
-          python-version: '3.8'
+          python-version: '3.10'
           check-latest: true
           cache: 'pip'
 
@@ -110,7 +110,7 @@ jobs:
 
       - uses: actions/setup-python@v5
         with:
-          python-version: '3.8'
+          python-version: '3.10'
           check-latest: true
           cache: 'pip'
 

.github/workflows/pages.yaml

@@ -89,7 +89,7 @@ jobs:
 
       - uses: actions/setup-python@v5
         with:
-          python-version: '3.8'
+          python-version: '3.10'
           check-latest: true
           cache: 'pip'
 

.pre-commit-config.yaml

@@ -2,16 +2,18 @@ fail_fast: false
 
 repos:
   - repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v3.2.0
+    rev: v6.0.0
     hooks:
       - id: trailing-whitespace
       - id: end-of-file-fixer
       - id: mixed-line-ending
+      # Behavior depends on the Python version you're running with,
+      # there's no way to tell it to target a fixed minimum version
       # - id: double-quote-string-fixer
       - id: check-ast
       - id: check-yaml
       # - id: check-json # Doesn't accept json with comments
-      # - id: requirements-txt-fixer # Can't handle comments
+      - id: requirements-txt-fixer
 
   - repo: https://github.com/codespell-project/codespell
     rev: v2.4.1
@@ -114,21 +116,22 @@ repos:
       #   types_or: [markdown, text]
       #   require_serial: false
 
+  # Run these checks after files are generated by the rules above
   - repo: https://github.com/pre-commit/pre-commit-hooks
-    rev: v3.2.0
+    rev: v6.0.0
     hooks:
       - id: check-case-conflict
       - id: check-merge-conflict
 
-  # - repo: https://github.com/pre-commit/mirrors-autopep8
-  #   rev: 'v2.0.2'
-  #   hooks:
-  #     - id: autopep8
-  #       name: Python scripts formatting
-  #       args: ['-i', '--global-config', '/dev/null']
+  - repo: https://github.com/hhatto/autopep8
+    rev: 'v2.3.2'
+    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'
+    rev: 'v4.0.0-alpha.8'
     hooks:
       - id: prettier
         name: CSS, JS, YAML and Markdown (no codeblocks) formatting

docs/CODINGSTYLE.md

@@ -110,7 +110,6 @@ agda-unimath project.
   definition. This contradicts our objective of organizing the library into
   compact, reusable components. If a `where` block is deemed necessary, follow
   these conventions:
-
   - Opt for `where` blocks over `let` expressions.
   - Indent the `where` keyword by two spaces and align their content with the
     `where` keyword.
@@ -136,7 +135,6 @@ agda-unimath project.
 
   There are multiple syntaxes for writing lambda expressions in Agda. Generally,
   you have the following options:
-
   1. Regular lambda expressions without pattern matching:
 
      ```agda
@@ -402,7 +400,6 @@ library:
 - In order to improve the readability on the agda-unimath website, we use a
   standard line length of 80 characters. There are only a few exceptions that
   enable us to have names that are more than 80 characters long:
-
   - Named `module` declarations
   - `open import` statements
   - Lines consisting of a single, possibly parenthesized (`(){}`), token that is

docs/HOWTO-INSTALL.md

@@ -20,9 +20,9 @@ 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`, `pybtex`, `requests`, `tomli`, and
-   `graphviz`. These can be installed by running
+3. `python` version 3.10 or newer
+4. The python libraries `pre-commit`, `pybtex`, `tomli`, and `graphviz`. These
+   can be installed by running
    ```shell
    python3 -m pip install -r scripts/requirements.txt
    ```
@@ -316,7 +316,7 @@ will need to install the `pre-commit` tool and the hooks' Python dependencies.
 The easiest way to accomplish this is by using the Python package manager `pip`.
 
 First, make sure that you have the latest version of Python and pip installed on
-your computer; the hooks require Python 3.8 or newer. Then run the following
+your computer; the hooks require Python 3.10 or newer. Then run the following
 command from the repository's main folder:
 
 ```shell
@@ -392,7 +392,6 @@ This issue can arise if the `pre-commit` executable gets placed in the
    `ls ~/.local/bin | grep pre-commit` to see if the executable is present.
 
 2. **Update your `PATH`**:
-
    - If you're using the bash terminal, open your `.bashrc` file with a text
      editor like `nano`:
 
@@ -409,7 +408,6 @@ This issue can arise if the `pre-commit` executable gets placed in the
    - Save the file and close the editor.
 
 3. **Reload your `.bashrc`**:
-
    - Run the following command to apply the changes:
 
      ```bash

docs/MIXFIX-OPERATORS.md

@@ -177,8 +177,8 @@ Below, we outline a list of general rules when assigning associativities.
 | 16               | Right homotopy whiskering `_·r_`                                                                                                                                                                   |
 | 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, `_*_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
 | 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                                    |
-| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
-| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                               |
+| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                             |
+| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                             |
 | 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                             |
 | 0-1              | Reasoning syntaxes                                                                                                                                                                                 |
 | -∞               | Function type formation `_→_`                                                                                                                                                                      |

flake.nix

@@ -5,10 +5,6 @@
     # Unstable has Agda 2.8.0
     nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
     flake-utils.url = "github:numtide/flake-utils";
-    # We aim to support Python 3.8 as long as Ubuntu 20.24 has LTS,
-    # since it ships with that version. Python 3.8 itself is already
-    # EOL, so it was dropped from nixpkgs 24.05
-    nixpkgs-python.url = "github:NixOS/nixpkgs/nixos-23.11";
     # Nixpkgs with tested versions of mdbook crates;
     # may be removed once we backport new mdbook assets to our
     # modified versions
@@ -19,21 +15,25 @@
     };
   };
 
-  outputs = { self, nixpkgs, nixpkgs-mdbook, nixpkgs-python, flake-utils, mdbook-catppuccin }:
+  outputs = { self, nixpkgs, nixpkgs-mdbook, flake-utils, mdbook-catppuccin }:
     flake-utils.lib.eachDefaultSystem
       (system:
         let
           pkgs = nixpkgs.legacyPackages."${system}";
           pkgs-mdbook = nixpkgs-mdbook.legacyPackages."${system}";
-          pkgs-python = nixpkgs-python.legacyPackages."${system}";
-          python = pkgs-python.python38.withPackages (p: with p; [
+          # We aim to support Python 3.10 as long as Ubuntu 22.24 has LTS,
+          # since it ships with that version
+          python = pkgs.python310.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
             graphviz
           ]);
+          # Make sure pre-commit also uses Python 3.10
+          pre-commit = pkgs.pre-commit.override {
+            python3Packages = pkgs.python310Packages;
+          };
 
           agda-unimath-package = { lib, mkDerivation, time }: mkDerivation {
             pname = "agda-unimath";
@@ -44,7 +44,7 @@
 
             # We can reference the directory since we're using flakes,
             # which copies the version-tracked files into the nix store
-            # before evaluation, # so we don't run into the issue with
+            # before evaluation, so we don't run into the issue with
             # nonreproducible source paths as outlined here:
             # https://nix.dev/recipes/best-practices#reproducible-source-paths
             src = ./.;
@@ -80,7 +80,7 @@
               # maintenance scripts
               python
               # pre-commit checks
-              pkgs.pre-commit
+              pre-commit
               pkgs.nodejs
             ] ++ (with pkgs-mdbook; [
               # working on the website

scripts/generate_contributors.py

@@ -44,8 +44,10 @@ def format_contributor(contributor):
 if __name__ == '__main__':
     parser = argparse.ArgumentParser(
         description='Generate contributors markdown content. Usage: generate_contributors.py <CONTRIBUTORS_FILE> <OUTPUT_FILE>')
-    parser.add_argument('contributors_file', help='Path to the CONTRIBUTORS.toml file.')
-    parser.add_argument('output_file', help='Output file path to write the generated contributors markdown content to.')
+    parser.add_argument('contributors_file',
+                        help='Path to the CONTRIBUTORS.toml file.')
+    parser.add_argument(
+        'output_file', help='Output file path to write the generated contributors markdown content to.')
     args = parser.parse_args()
 
     contributors_data = parse_contributors_file(args.contributors_file)
@@ -62,7 +64,8 @@ def format_contributor(contributor):
         git_log_output, contributors_data)
 
     if skipped_authors:
-        print_skipping_contributors_warning(skipped_authors, args.contributors_file)
+        print_skipping_contributors_warning(
+            skipped_authors, args.contributors_file)
 
     output = template.format(
         names='\n'.join((format_contributor(c) for c in sorted_authors)),
@@ -71,7 +74,8 @@ def format_contributor(contributor):
 
     out_path = args.output_file
     if os.path.isdir(out_path):
-        print(f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr)
+        print(
+            f'Error: {out_path!r} is a directory; please provide a path including the filename.', file=sys.stderr)
         sys.exit(2)
     parent = os.path.dirname(out_path)
     if parent: