Merge branch 'master' into homotopy-groups

.github/workflows/ci.yaml

@@ -25,30 +25,24 @@ concurrency:
   group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}'
   cancel-in-progress: true
 
-env:
-  AGDAHTMLFLAGS:
-    --only-scope-checking --html --html-highlight=code --html-dir=docs
-    --css=docs/Agda.css
-  AGDA: agda
-
 jobs:
   typecheck:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macOS-latest, ubuntu-latest]
-        agda: ['2.6.3']
+        os: [macOS-13, ubuntu-latest]
+        agda: ['2.7.0']
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
       - name: Setup Agda
-        uses: wenkokke/setup-agda@v2.0.0
+        uses: wenkokke/setup-agda@v2.5.0
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -60,19 +54,20 @@ jobs:
             ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-
             ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}-
 
-      - name: Typecheck the whole formalization
+      - name: Typecheck library
         run: |
           cd master
+          agda --version
           make check
 
       - name: Save Agda build cache
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           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
+      - uses: actions/setup-python@v5
         if: ${{ matrix.os == 'ubuntu-latest' }}
         with:
           python-version: '3.8'
@@ -97,7 +92,7 @@ jobs:
       # keep the same key for a branch and update it on pushes.
       - name: Save pre-website cache
         if: ${{ matrix.os == 'ubuntu-latest' }}
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -111,26 +106,35 @@ jobs:
       actions: write
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           path: master
 
-      - uses: peaceiris/actions-mdbook@v1
+      - uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
-      - uses: baptiste0928/cargo-install@v2
+      - uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
-      - uses: actions/cache/restore@v3
+      # Install Python and friends for website generation only where needed
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.8'
+          check-latest: true
+          cache: 'pip'
+
+      - run: python3 -m pip install -r master/scripts/requirements.txt
+
+      - uses: actions/cache/restore@v4
         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: |
@@ -158,14 +162,14 @@ jobs:
   pre-commit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r scripts/requirements.txt
 
-      - uses: pre-commit/[email protected].0
+      - uses: pre-commit/[email protected].1

.github/workflows/clean-up.yaml

@@ -1,4 +1,4 @@
-name: cleanup caches generated by pull requests
+name: Clean up caches generated by pull requests
 on:
   pull_request:
     types:
@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Cleanup
         run: |

.github/workflows/pages.yaml

@@ -1,4 +1,4 @@
-name: Formalization website
+name: Build and deploy library website
 on:
   # To run this workflow manually
   workflow_dispatch:
@@ -17,17 +17,12 @@ concurrency:
   group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}'
   cancel-in-progress: true
 
-env:
-  AGDAHTMLFLAGS:
-    --html --html-highlight=auto --html-dir=docs --only-scope-checking
-    --css=Agda.css
-  AGDA: agda
 jobs:
   website:
-    runs-on: macOS-latest
+    runs-on: ubuntu-latest
     strategy:
       matrix:
-        agda: ['2.6.3']
+        agda: ['2.7.0']
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
@@ -37,18 +32,18 @@ jobs:
       id-token: write # to verify the deployment originates from an appropriate source
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
           # We need the entire history for contributor information
           fetch-depth: 0
 
       - name: Setup Agda
-        uses: wenkokke/setup-agda@v2.0.0
+        uses: wenkokke/setup-agda@v2.5.0
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -61,35 +56,35 @@ jobs:
 
       # Keep versions in sync with the Makefile
       - name: MDBook setup
-        uses: peaceiris/actions-mdbook@v1
+        uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
       - name: Install mdbook-pagetoc
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-pagetoc
           version: '0.1.7'
 
       - name: Install mdbook-katex
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-katex
           version: '0.5.7'
 
       - name: Install mdbook-linkcheck
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       - name: Install mdbook-catppuccin
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-catppuccin
           version: '1.2.0'
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -105,21 +100,21 @@ jobs:
           make website
 
       - name: Setup Pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v5
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
         with:
           path: master/book/html
 
       - name: Deploy to GitHub Pages
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v4
         id: deployment
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==

.github/workflows/profiling.yaml

@@ -0,0 +1,81 @@
+name: Profile Library Typechecking
+
+on:
+  push:
+    branches:
+      - master
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: false
+
+jobs:
+  typecheck-performance:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        agda: ['2.7.0']
+
+    steps:
+      - name: Checkout our repository
+        uses: actions/checkout@v4
+        with:
+          path: repo
+
+      - name: Setup Agda
+        uses: wenkokke/[email protected]
+        with:
+          agda-version: ${{ matrix.agda }}
+
+      - name: Typecheck library with profiling
+        run: |
+          cd repo
+          agda --version
+          mkdir -p temp
+          make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt
+
+      - name: Download previous typechecking profile
+        run: |
+          mkdir -p benchmark-cache
+          curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json
+          # Stop if there is no initial data (the server gave us an HTML instead of a JSON)
+          (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || { rm benchmark-cache/data.json; exit 0; }
+          curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv
+
+      - name: Process new profiling data
+        run: |
+          cd repo
+          python3 scripts/typechecking_profile_parser.py \
+            temp/benchmark-results.txt temp/memory-results.txt \
+            temp/benchmark-results.json ../benchmark-cache/data.csv \
+            ${{ github.sha }}
+
+      - name: Merge JSON profiling data
+        uses: rhysd/github-action-benchmark@v1
+        with:
+          tool: 'customSmallerIsBetter'
+          # Location of the new data
+          output-file-path: './repo/temp/benchmark-results.json'
+          # Location of the aggregate data
+          external-data-json-path: './benchmark-cache/data.json'
+
+      - name: Publish the profiling CSV as an artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: 'Library profiling history'
+          path: './benchmark-cache/data.csv'
+
+      - name: Prepare new revision of the profiling website
+        run: |
+          mkdir -p benchmark-website
+          cp repo/website/benchmarks/index.html benchmark-website/
+          cp benchmark-cache/data.* benchmark-website/
+          echo 'window.BENCHMARK_DATA =' | cat - benchmark-cache/data.json > benchmark-website/data.js
+
+      - name: Deploy the new profiling website
+        env:
+          NETLIFY_SITE_ID: ${{ secrets.PERF_SITE_ID }}
+          NETLIFY_AUTH_TOKEN: ${{ secrets.PERF_SITE_KEY }}
+        run: |
+          npx netlify-cli deploy --prod --dir=benchmark-website

.gitignore

@@ -423,6 +423,7 @@ package-lock.json
 docs/
 html/
 book/
+temp/
 src/temp/
 src/everything.lagda.md
 SUMMARY.md

.pre-commit-config.yaml

@@ -7,7 +7,7 @@ repos:
       - id: trailing-whitespace
       - id: end-of-file-fixer
       - id: mixed-line-ending
-      - id: double-quote-string-fixer
+      # - id: double-quote-string-fixer
       - id: check-ast
       - id: check-yaml
       # - id: check-json # Doesn't accept json with comments
@@ -96,12 +96,12 @@ repos:
       - 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/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/pre-commit/mirrors-prettier
     rev: 'v3.0.0-alpha.6'