From cbd9f0bf9f5f0fe66130bdef50fe5dbc485a19cf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 21 Oct 2023 15:19:42 +0100 Subject: [PATCH 1/7] missing comma! --- README.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.agda b/README.agda index cc436d0848..41b536a0d0 100644 --- a/README.agda +++ b/README.agda @@ -7,7 +7,7 @@ module README where -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, --- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy Joachim Breitner, +-- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy, Joachim Breitner, -- Samuel Bronson, Daniel Brown, Jacques Carette, James Chapman, -- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő, -- Zack Grannan, Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu, From cdd592b86f7220f277e990b3527f734ba9459392 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 21 Oct 2023 16:21:48 +0100 Subject: [PATCH 2/7] corrected reference to `README.Design.Decidability` --- src/Relation/Nullary/Decidable/Core.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 166b1f264e..ff73c6af20 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -35,8 +35,8 @@ private -- reflects the boolean result. This definition allows the boolean -- part of the decision procedure to compute independently from the -- proof. This leads to better computational behaviour when we only care --- about the result and not the proof. See README.Decidability for --- further details. +-- about the result and not the proof. See README.Design.Decidability +-- for further details. infix 2 _because_ From 34899cb66da1044613241977d7ef9691bbb7df13 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Oct 2023 10:56:48 +0100 Subject: [PATCH 3/7] typo: capitalisation --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9d9f403d64..05fdf904fd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2761,7 +2761,7 @@ Additions to existing modules * Added new definitions and proofs to `Data.Nat.Primality`: ```agda Composite : ℕ → Set - composite? : Decidable composite + composite? : Decidable Composite composite⇒¬prime : Composite n → ¬ Prime n ¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n prime⇒¬composite : Prime n → ¬ Composite n From 842f3cd788e9eb85cd3a6f985eef52902977955f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Oct 2023 10:58:30 +0100 Subject: [PATCH 4/7] updated `installation-guide` --- notes/installation-guide.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/notes/installation-guide.md b/notes/installation-guide.md index f05f21ed90..67d1685ad9 100644 --- a/notes/installation-guide.md +++ b/notes/installation-guide.md @@ -3,19 +3,19 @@ Installation instructions Note: the full story on installing Agda libraries can be found at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html). -Use version v1.7.2 of the standard library with Agda 2.6.3. +Use version v2.0 of the standard library with Agda 2.6.4. 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v1.7.2 of the standard library. This can either be +2. Download the tarball of v2.0 of the standard library. This can either be done manually by visiting the Github repository for the library, or via the command line as follows: ``` - wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.2.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.0.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `1.7.2` with any other version of the library you desire. + you can replace `2.0` with any other version of the library you desire. 3. Extract the standard library from the tarball. Again this can either be done manually or via the command line as follows: @@ -26,7 +26,7 @@ Use version v1.7.2 of the standard library with Agda 2.6.3. 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-1.7.2 + cd agda-stdlib-2.0 cabal install ``` @@ -40,7 +40,7 @@ Use version v1.7.2 of the standard library with Agda 2.6.3. 6. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-1.7.2/standard-library.agda-lib + $HERE/agda-stdlib-2.0/standard-library.agda-lib ``` Now, the standard library is ready to be used either: From c84665ef531bc49bc52aaa09c6d9486936ba640c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Oct 2023 16:54:17 +0100 Subject: [PATCH 5/7] added word to `NonZero` section heading --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 05fdf904fd..ff21ab1c98 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -504,7 +504,7 @@ Non-backwards compatible changes and `Codata.Guarded.Stream.Relation.Binary.Pointwise`, the proofs called `lookup` have been renamed `lookup⁺`. -#### Changes to `Data.(Nat/Integer/Rational)` proofs of `NonZero`/`Positive`/`Negative` to instance arguments +#### Changes to `Data.(Nat/Integer/Rational)` proofs of `NonZero`/`Positive`/`Negative` to use instance arguments * Many numeric operations in the library require their arguments to be non-zero, and various proofs require their arguments to be non-zero/positive/negative etc. From 138509e38076245a650cd959dbb7e48e8d9b2e22 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Mon, 30 Oct 2023 11:57:40 +0900 Subject: [PATCH 6/7] Run workflows on any PR --- .github/workflows/ci-ubuntu.yml | 3 --- .github/workflows/haskell-ci.yml | 3 --- 2 files changed, 6 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 2ecc969589..7a13f97fae 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -5,9 +5,6 @@ on: - master - experimental pull_request: - branches: - - master - - experimental ######################################################################## ## CONFIGURATION diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index b8c55c19be..c81c8572de 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -24,9 +24,6 @@ on: - cabal.haskell-ci - "*.hs" pull_request: - branches: - - master - - experimental paths: - .github/workflows/haskell-ci.yml - agda-stdlib-utils.cabal From 80f19aff55063d892e484e167092cf0e76ef0ca6 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Mon, 30 Oct 2023 13:53:31 +0900 Subject: [PATCH 7/7] Add merge-group trigger to workflows --- .github/workflows/ci-ubuntu.yml | 4 ++++ .github/workflows/haskell-ci.yml | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 7a13f97fae..0f723e005a 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -5,6 +5,10 @@ on: - master - experimental pull_request: + branches: + - master + - experimental + merge_group: ######################################################################## ## CONFIGURATION diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index c81c8572de..d4a05fc9bd 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -24,11 +24,15 @@ on: - cabal.haskell-ci - "*.hs" pull_request: + branches: + - master + - experimental paths: - .github/workflows/haskell-ci.yml - agda-stdlib-utils.cabal - cabal.haskell-ci - "*.hs" + merge_group: jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }}