From f8af639f122552afb3926a304261eb5af48153f5 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 7 Oct 2023 12:59:30 +0200 Subject: [PATCH 1/8] set `--level-universe` flag --- DESIGN-PRINCIPLES.md | 4 ++-- Makefile | 2 +- agda-unimath.agda-lib | 2 +- scripts/demote_foundation_imports.py | 2 +- scripts/remove_unused_imports.py | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index 99ef5f78c4..ad90b332d0 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -6,8 +6,8 @@ to it. This document aims to provide a clear and concise introduction. ## Postulates and assumptions -The library assumes the `--without-K` and `--exact-split` flags of Agda and -makes use of several postulates. +The library assumes the `--without-K`, `--exact-split`, and `--level-universe` +flags of Agda and makes use of several postulates. 1. We make full use of Agda's `data` types for introducing inductive types. 2. We make full use of Agda's universe levels, including `ω`. However, it should diff --git a/Makefile b/Makefile index d70663f85d..e3633f1ac1 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ -CHECKOPTS := --without-K --exact-split --guardedness +CHECKOPTS := --without-K --exact-split --level-universe --guardedness everythingOpts := $(CHECKOPTS) AGDAVERBOSE ?= -v1 # use "$ export AGDAVERBOSE=20" if you want to see all diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib index b7557d82bd..ff48959cd8 100644 --- 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 +flags: --without-K --exact-split --level-universe --no-import-sorts --auto-inline diff --git a/scripts/demote_foundation_imports.py b/scripts/demote_foundation_imports.py index 40e1974cab..bded56e68a 100644 --- a/scripts/demote_foundation_imports.py +++ b/scripts/demote_foundation_imports.py @@ -129,7 +129,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): root = 'src' temp_dir = 'temp' status = 0 - agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching' + agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching' temp_root = os.path.join(root, temp_dir) shutil.rmtree(temp_root, ignore_errors=True) diff --git a/scripts/remove_unused_imports.py b/scripts/remove_unused_imports.py index decada0fbd..231b61a661 100644 --- a/scripts/remove_unused_imports.py +++ b/scripts/remove_unused_imports.py @@ -95,7 +95,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): root = 'src' temp_dir = 'temp' status = 0 - agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching' + agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching' temp_root = os.path.join(root, temp_dir) shutil.rmtree(temp_root, ignore_errors=True) From e7f688f24907923259d89d8460aac52dfd2bb3a6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 7 Oct 2023 13:02:14 +0200 Subject: [PATCH 2/8] bump agda version to `2.6.4` --- .github/workflows/ci.yaml | 2 +- .github/workflows/pages.yaml | 2 +- HOWTO-INSTALL.md | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index b6964cdae2..fbf9dc9403 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -37,7 +37,7 @@ jobs: strategy: matrix: os: [macOS-latest, ubuntu-latest] - agda: ['2.6.3'] + agda: ['2.6.4'] steps: - name: Checkout our repository uses: actions/checkout@v3 diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml index 570d83db4c..c84621579b 100644 --- a/.github/workflows/pages.yaml +++ b/.github/workflows/pages.yaml @@ -27,7 +27,7 @@ jobs: runs-on: macOS-latest strategy: matrix: - agda: ['2.6.3'] + agda: ['2.6.4'] environment: name: github-pages url: ${{ steps.deployment.outputs.page_url }} diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md index a0eb4d04f2..5826c33cc3 100644 --- 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.3 installed, and a suitable editor such as +need to have `agda` version 2.6.4 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,7 +122,7 @@ working branches when necessary. ## Installing Agda {#installing-agda} -The `agda-unimath` library is built and verified with Agda 2.6.3, and we provide +The `agda-unimath` library is built and verified with Agda 2.6.4, 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 @@ -130,7 +130,7 @@ library across different systems. ### Without Nix -To install Agda 2.6.3 without Nix, follow the +To install Agda 2.6.4 without Nix, follow the [installation guide](https://agda.readthedocs.io/en/latest/getting-started/installation.html) provided on the Agda documentation page. From d6cc5038de436db2087b17e34ca5ef7c61fc3eff Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 17 Oct 2023 01:52:31 +0200 Subject: [PATCH 3/8] Revert `--level-universe` --- DESIGN-PRINCIPLES.md | 3 +-- Makefile | 3 +-- agda-unimath.agda-lib | 2 +- scripts/demote_foundation_imports.py | 2 +- scripts/remove_unused_imports.py | 2 +- 5 files changed, 5 insertions(+), 7 deletions(-) diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index ad90b332d0..b0461571da 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -6,8 +6,7 @@ to it. This document aims to provide a clear and concise introduction. ## Postulates and assumptions -The library assumes the `--without-K`, `--exact-split`, and `--level-universe` -flags of Agda and makes use of several postulates. +The library assumes the `--without-K` and `--exact-split` of Agda and makes use of several postulates. 1. We make full use of Agda's `data` types for introducing inductive types. 2. We make full use of Agda's universe levels, including `ω`. However, it should diff --git a/Makefile b/Makefile index 2985cb7f60..4be42902e7 100644 --- a/Makefile +++ b/Makefile @@ -4,8 +4,7 @@ # files, and if these options are pervasive (i.e. they need to be enabled in all # modules that include the modules that have them enabled), then they need to be # added to the everything file as well. -everythingOpts := --level-universe --guardedness - +everythingOpts := --guardedness # use "$ export AGDAVERBOSE=-v20" if you want to see all AGDAVERBOSE ?= -v1 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print) diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib index ff48959cd8..b7557d82bd 100644 --- a/agda-unimath.agda-lib +++ b/agda-unimath.agda-lib @@ -1,3 +1,3 @@ name: agda-unimath include: src -flags: --without-K --exact-split --level-universe --no-import-sorts --auto-inline +flags: --without-K --exact-split --no-import-sorts --auto-inline diff --git a/scripts/demote_foundation_imports.py b/scripts/demote_foundation_imports.py index bded56e68a..40e1974cab 100644 --- a/scripts/demote_foundation_imports.py +++ b/scripts/demote_foundation_imports.py @@ -129,7 +129,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): root = 'src' temp_dir = 'temp' status = 0 - agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching' + agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching' temp_root = os.path.join(root, temp_dir) shutil.rmtree(temp_root, ignore_errors=True) diff --git a/scripts/remove_unused_imports.py b/scripts/remove_unused_imports.py index 231b61a661..decada0fbd 100644 --- a/scripts/remove_unused_imports.py +++ b/scripts/remove_unused_imports.py @@ -95,7 +95,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): root = 'src' temp_dir = 'temp' status = 0 - agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching' + agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching' temp_root = os.path.join(root, temp_dir) shutil.rmtree(temp_root, ignore_errors=True) From 8796a1e996056aedaa3a6ae8b5d0025e022f3c08 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 18 Oct 2023 18:07:34 +0200 Subject: [PATCH 4/8] fix links --- CODINGSTYLE.md | 2 +- HOME.md | 2 +- MIXFIX-OPERATORS.md | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index b02c0b2eb0..ea05f0a2ff 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -284,7 +284,7 @@ the `agda-unimath` library: need to sort them by hand. - The library doesn't use - [variables](https://agda.readthedocs.io/en/v2.6.3/language/generalization-of-declared-variables.html) + [variables](https://agda.readthedocs.io/en/v2.6.4/language/generalization-of-declared-variables.html) at the moment. All variables are declared either as parameters of an anonymous module or in the type specification of a construction. diff --git a/HOME.md b/HOME.md index 712b274721..2b19543a0f 100644 --- a/HOME.md +++ b/HOME.md @@ -17,7 +17,7 @@ resources for both 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.3 and can be compiled by +The `agda-unimath` library is compatible with Agda 2.6.4 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/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index e2bc34c8a3..a788f03263 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -2,7 +2,7 @@ This document outlines our choices of conventions for setting precedence levels and associativity of -[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html), +[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.4/language/mixfix-operators.html), and provides guidelines for this. ## Mixfix operators in Agda @@ -16,7 +16,7 @@ and mixfix operators in Agda is to make the code more readable by using commonly accepted notation for widely used operators. Mixfix operators can each be assigned a -[precedence level](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#precedence). +[precedence level](https://agda.readthedocs.io/en/v2.6.4/language/mixfix-operators.html#precedence). This can in principle be any signed fractional value, although we prefer them to be non-negative integral values. The higher this value is, the higher precedence the operator has, meaning it is evaluated before operators with lower @@ -32,7 +32,7 @@ is parsed as `x +ℕ (y *ℕ z)`. In addition to a precedence level, every mixfix operator can be defined to be either left or right -[associative](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#associativity). +[associative](https://agda.readthedocs.io/en/v2.6.4/language/mixfix-operators.html#associativity). It can be beneficial to define associativity of operators, to avoid excessively parenthesized expressions. The parenthization should, however, never be omitted when this can make the code more ambiguous or harder to read. From 3e7690766bcceaa2d8177784d6ba66afcae0899c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 18 Oct 2023 18:09:48 +0200 Subject: [PATCH 5/8] pre-commit --- DESIGN-PRINCIPLES.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index b0461571da..1ed21d322d 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -6,7 +6,8 @@ to it. This document aims to provide a clear and concise introduction. ## Postulates and assumptions -The library assumes the `--without-K` and `--exact-split` of Agda and makes use of several postulates. +The library assumes the `--without-K` and `--exact-split` of Agda and makes use +of several postulates. 1. We make full use of Agda's `data` types for introducing inductive types. 2. We make full use of Agda's universe levels, including `ω`. However, it should From 97b1ed3c9422fdfb8a852da5129fca8aa774e15c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 11 Nov 2023 23:00:33 +0100 Subject: [PATCH 6/8] bump `wenkokke/setup-agda` --- .github/workflows/ci.yaml | 2 +- .github/workflows/pages.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 51b3409961..e35520127f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -44,7 +44,7 @@ jobs: with: path: master - name: Setup Agda - uses: wenkokke/setup-agda@v2.0.0 + uses: wenkokke/setup-agda@v2.1.0 with: agda-version: ${{ matrix.agda }} diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml index 2ab4d4549d..b8c8c6b82f 100644 --- a/.github/workflows/pages.yaml +++ b/.github/workflows/pages.yaml @@ -44,7 +44,7 @@ jobs: fetch-depth: 0 - name: Setup Agda - uses: wenkokke/setup-agda@v2.0.0 + uses: wenkokke/setup-agda@v2.1.0 with: agda-version: ${{ matrix.agda }} From 0d579e4230d96ba6369e114a9db048f24927551e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 14 Nov 2023 10:50:28 +0100 Subject: [PATCH 7/8] Update DESIGN-PRINCIPLES.md --- DESIGN-PRINCIPLES.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index 1ed21d322d..99ef5f78c4 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -6,8 +6,8 @@ to it. This document aims to provide a clear and concise introduction. ## Postulates and assumptions -The library assumes the `--without-K` and `--exact-split` of Agda and makes use -of several postulates. +The library assumes the `--without-K` and `--exact-split` flags of Agda and +makes use of several postulates. 1. We make full use of Agda's `data` types for introducing inductive types. 2. We make full use of Agda's universe levels, including `ω`. However, it should From 22229c354d70a3d8c4f1527210216d7df40d3a11 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Tue, 14 Nov 2023 15:50:48 +0100 Subject: [PATCH 8/8] Bump nixpkgs for Agda 2.6.4 I kept the mdbook crates on the same version by pinning the checkout of nixpkgs we were using previously as `nixpkgs-mdbook` --- flake.lock | 23 ++++++++++++++++++++--- flake.nix | 28 ++++++++++++++++------------ 2 files changed, 36 insertions(+), 15 deletions(-) diff --git a/flake.lock b/flake.lock index 4166676b45..8f4f0d5187 100644 --- a/flake.lock +++ b/flake.lock @@ -21,7 +21,7 @@ "mdbook-catppuccin": { "inputs": { "nixpkgs": [ - "nixpkgs" + "nixpkgs-mdbook" ] }, "locked": { @@ -40,6 +40,22 @@ } }, "nixpkgs": { + "locked": { + "lastModified": 1699725108, + "narHash": "sha256-NTiPW4jRC+9puakU4Vi8WpFEirhp92kTOSThuZke+FA=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "911ad1e67f458b6bcf0278fa85e33bb9924fed7e", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-mdbook": { "locked": { "lastModified": 1696526028, "narHash": "sha256-Psqo4j/KNvpk45MKscqdYk/N5lmrLKIV8x4ednfiqnY=", @@ -50,8 +66,8 @@ }, "original": { "owner": "NixOS", - "ref": "nixpkgs-unstable", "repo": "nixpkgs", + "rev": "7fdd1421774a52277fb56d64b26aaf7765e1b3fa", "type": "github" } }, @@ -59,7 +75,8 @@ "inputs": { "flake-utils": "flake-utils", "mdbook-catppuccin": "mdbook-catppuccin", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs", + "nixpkgs-mdbook": "nixpkgs-mdbook" } }, "systems": { diff --git a/flake.nix b/flake.nix index 2862fe4892..7ae3597968 100644 --- a/flake.nix +++ b/flake.nix @@ -2,20 +2,25 @@ description = "agda-unimath"; inputs = { - # Unstable is needed for Agda 2.6.3, latest stable 22.11 only has 2.6.2.2 + # Unstable is needed for Agda 2.6.4, latest stable 23.05 only has 2.6.3 nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; flake-utils.url = "github:numtide/flake-utils"; + # Nixpkgs with tested versions of mdbook crates; + # may be removed once we backport new mdbook assets to our + # modified versions + nixpkgs-mdbook.url = "github:NixOS/nixpkgs?rev=7fdd1421774a52277fb56d64b26aaf7765e1b3fa"; mdbook-catppuccin = { url = "github:catppuccin/mdBook/v1.2.0"; - inputs.nixpkgs.follows = "nixpkgs"; + inputs.nixpkgs.follows = "nixpkgs-mdbook"; }; }; - outputs = { self, nixpkgs, 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}"; 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 @@ -67,17 +72,16 @@ packages = [ # maintanance scripts python - # working on the website - pkgs.mdbook - pkgs.mdbook-katex - pkgs.mdbook-pagetoc - pkgs.mdbook-linkcheck - mdbook-catppuccin.packages."${system}".default # pre-commit checks pkgs.pre-commit - ]; + ] ++ (with pkgs-mdbook; [ + # working on the website + mdbook + mdbook-katex + mdbook-pagetoc + mdbook-linkcheck + mdbook-catppuccin.packages."${system}".default + ]); }; - - devShell = self.devShells."${system}".default; }); }