Agda version 2.7.0 (#1238)

I think it's about time we consider updating the library to Agda 2.7.0. It's very unfortunate that the newest version is still not hosted with homebrew, but considering it's been over 5 months now and [nothing's happening](Homebrew/homebrew-core#193315), we should consider moving away from depending on it. --------- Co-authored-by: VojtechStep <[email protected]>
UniMath · Jan 19, 2025 · 77decd8 · 77decd8
1 parent 13af1cf
commit 77decd8
Show file tree

Hide file tree

Showing 10 changed files with 63 additions and 26 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -31,14 +31,14 @@ jobs:
     strategy:
       matrix:
         os: [macOS-13, ubuntu-latest]
-        agda: ['2.6.4']
+        agda: ['2.7.0']
     steps:
       - name: Checkout our repository
         uses: actions/checkout@v3
         with:
           path: master
       - name: Setup Agda
-        uses: wenkokke/setup-agda@v2.1.0
+        uses: wenkokke/setup-agda@v2.5.0
         with:
           agda-version: ${{ matrix.agda }}
 
@@ -57,6 +57,7 @@ jobs:
       - name: Typecheck library
         run: |
           cd master
+          agda --version
           make check
 
       - name: Save Agda build cache

diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -22,7 +22,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        agda: ['2.6.4']
+        agda: ['2.7.0']
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
@@ -39,7 +39,7 @@ jobs:
           fetch-depth: 0
 
       - name: Setup Agda
-        uses: wenkokke/setup-agda@v2.1.0
+        uses: wenkokke/setup-agda@v2.5.0
         with:
           agda-version: ${{ matrix.agda }}
 

diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml
@@ -15,7 +15,7 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest]
-        agda: ['2.6.4']
+        agda: ['2.7.0']
 
     steps:
       - name: Checkout our repository
@@ -24,13 +24,14 @@ jobs:
           path: repo
 
       - name: Setup Agda
-        uses: wenkokke/setup-agda@v2.1.0
+        uses: wenkokke/setup-agda@v2.5.0
         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
 

diff --git a/HOME.md b/HOME.md
@@ -21,7 +21,7 @@ working and learning mathematicians. Our library is designed to work towards
 this goal, and we welcome contributions to the library within any topic in
 mathematics.
 
-The agda-unimath library is compatible with Agda 2.6.4 and can be compiled by
+The agda-unimath library is compatible with Agda 2.7.0 and can be compiled by
 running `make check` from the root directory of the repository. Learn more about
 using the library locally in our [installation guide](HOWTO-INSTALL.md).
 

diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
@@ -5,7 +5,7 @@
 ### Quick setup
 
 To work or experiment with the agda-unimath library on your machine, you will
-need to have `agda` version 2.6.4 installed, and a suitable editor such as
+need to have `agda` version 2.7.0 installed, and a suitable editor such as
 [Emacs](https://www.gnu.org/software/emacs/) or
 [Visual Studio Code](https://code.visualstudio.com/). The following instructions
 will help you on your way right away:
@@ -122,15 +122,15 @@ working branches when necessary.
 
 ## Installing Agda {#installing-agda}
 
-The agda-unimath library is built and verified with Agda 2.6.4, and we provide
+The agda-unimath library is built and verified with Agda 2.7.0, and we provide
 two methods for installation: with or without the package manager
 [Nix](https://nixos.org/). Nix streamlines the installation of Agda and its
 dependencies, providing a consistent and reproducible environment for the
 library across different systems.
 
 ### Without Nix
 
-To install Agda 2.6.4 without Nix, follow the
+To install Agda 2.7.0 without Nix, follow the
 [installation guide](https://agda.readthedocs.io/en/latest/getting-started/installation.html)
 provided on the Agda documentation page.
 

diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib
@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline -WnoWithoutKFlagPrimEraseEquality
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,9 +2,13 @@
   description = "agda-unimath";
 
   inputs = {
-    # Unstable is needed for Agda 2.6.4, latest stable 23.05 only has 2.6.3
-    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+    # Stable 24.11 has Agda 2.7.0.1
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
     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
@@ -15,13 +19,14 @@
     };
   };
 
-  outputs = { self, nixpkgs, nixpkgs-mdbook, flake-utils, mdbook-catppuccin }:
+  outputs = { self, nixpkgs, nixpkgs-mdbook, nixpkgs-python, flake-utils, mdbook-catppuccin }:
     flake-utils.lib.eachDefaultSystem
       (system:
         let
           pkgs = nixpkgs.legacyPackages."${system}";
           pkgs-mdbook = nixpkgs-mdbook.legacyPackages."${system}";
-          python = pkgs.python38.withPackages (p: with p; [
+          pkgs-python = nixpkgs-python.legacyPackages."${system}";
+          python = pkgs-python.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

diff --git a/src/reflection/definitions.lagda.md b/src/reflection/definitions.lagda.md
@@ -34,13 +34,24 @@ The `Definition-Agda` type represents a definition in Agda.
 
 ```agda
 data Definition-Agda : UU lzero where
-  function-Definition-Agda : list Clause-Agda → Definition-Agda
-  data-type-Definition-Agda : ℕ → list Name-Agda → Definition-Agda
+
+  function-Definition-Agda :
+    list Clause-Agda → Definition-Agda
+
+  data-type-Definition-Agda :
+    ℕ → list Name-Agda → Definition-Agda
+
   record-type-Definition-Agda :
     Name-Agda → list (Argument-Agda Name-Agda) → Definition-Agda
-  data-constructor-Definition-Agda : Name-Agda → Definition-Agda
-  postulate-Definition-Agda : Definition-Agda
-  primitive-function-Definition-Agda : Definition-Agda
+
+  data-constructor-Definition-Agda :
+    Name-Agda → Quantity-Argument-Agda → Definition-Agda
+
+  postulate-Definition-Agda :
+    Definition-Agda
+
+  primitive-function-Definition-Agda :
+    Definition-Agda
 ```
 
 ## Bindings

diff --git a/src/reflection/type-checking-monad.lagda.md b/src/reflection/type-checking-monad.lagda.md
@@ -161,7 +161,9 @@ postulate
   declare-data :
     Name-Agda → ℕ → Term-Agda → type-Type-Checker unit
   define-data :
-    Name-Agda → list (Name-Agda × Term-Agda) → type-Type-Checker unit
+    Name-Agda →
+    list (Name-Agda × Quantity-Argument-Agda × Term-Agda) →
+    type-Type-Checker unit
 ```
 
 ## Bindings