From b85c5d19ceeaaa22c57c138396141b7270218eb1 Mon Sep 17 00:00:00 2001 From: = Date: Mon, 22 Nov 2021 17:07:38 +0000 Subject: [PATCH] Admin for v1.7.1 release --- CHANGELOG.md | 222 +----------------------------------- README.agda | 5 +- README.md | 3 - agda-stdlib-utils.cabal | 2 +- notes/installation-guide.md | 12 +- standard-library.agda-lib | 2 +- 6 files changed, 13 insertions(+), 233 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 86a4373bda..be186d1d54 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,222 +1,6 @@ -Version 1.7 -=========== +Version 1.7.1 +============= The library has been tested using Agda 2.6.2. -Highlights ----------- - -* New module for making system calls during type checking, `Reflection.External`, - which re-exports `Agda.Builtin.Reflection.External`. - -* New predicate for lists that are enumerations their type in - `Data.List.Relation.Unary.Enumerates`. - -* New weak induction schemes in `Data.Fin.Induction` that allows one to avoid - the complicated use of `Acc`/`inject`/`raise` when proving inductive properties - over finite sets. - -Bug-fixes ---------- - -* Added missing module `Function.Metric` which re-exports - `Function.Metric.(Core/Definitions/Structures/Bundles)`. This module was referred - to in the documentation of its children but until now was not present. - -* Added missing fixity declaration to `_<_` in - `Relation.Binary.Construct.NonStrictToStrict`. - -Non-backwards compatible changes --------------------------------- - -#### Floating-point arithmetic - -* The functions in `Data.Float.Base` were updated following changes upstream, - in `Agda.Builtin.Float`, see . - -* The bitwise binary relations on floating-point numbers (`_<_`, `_≈ᵇ_`, `_==_`) - have been removed without replacement, as they were deeply unintuitive, - e.g., `∀ x → x < -x`. - -#### Reflection - -* The representation of reflected syntax in `Reflection.Term`, - `Reflection.Pattern`, `Reflection.Argument` and - `Reflection.Argument.Information` has been updated to match the new - representation used in Agda 2.6.2. Specifically, the following - changes were made: - - * The type of the `var` constructor of the `Pattern` datatype has - been changed from `(x : String) → Pattern` to `(x : Int) → - Pattern`. - - * The type of the `dot` constructor of the `Pattern` datatype has - been changed from `Pattern` to `(t : Term) → Pattern`. - - * The types of the `clause` and `absurd-clause` constructors of the - `Clause` datatype now take an extra argument `(tel : Telescope)`, - where `Telescope = List (String × Arg Type)`. - - * The following constructors have been added to the `Sort` datatype: - `prop : (t : Term) → Sort`, `propLit : (n : Nat) → Sort`, and - `inf : (n : Nat) → Sort`. - - * In `Reflection.Argument.Information` the function `relevance` was - replaced by `modality`. - - * The type of the `arg-info` constructor is now - `(v : Visibility) (m : Modality) → ArgInfo`. - - * In `Reflection.Argument` (as well as `Reflection`) there is a new - pattern synonym `defaultModality`, and the pattern synonyms - `vArg`, `hArg` and `iArg` have been changed. - - * Two new modules have been added, `Reflection.Argument.Modality` - and `Reflection.Argument.Quantity`. The constructors of the types - `Modality` and `Quantity` are reexported from `Reflection`. - -#### Sized types - -* Sized types are no longer considered safe in Agda 2.6.2. As a - result, all modules that use `--sized-types` no longer have the - `--safe` flag. For a full list of affected modules, refer to the - relevant [commit](https://github.com/agda/agda-stdlib/pull/1465/files#diff-e1c0e3196e4cea6ff808f5d2906031a7657130e10181516206647b83c7014584R91-R131.) - -* In order to maintain the safety of `Data.Nat.Pseudorandom.LCG`, the function - `stream` that relies on the newly unsafe `Codata` modules has - been moved to the new module `Data.Nat.Pseudorandom.LCG.Unsafe`. - -* In order to maintain the safety of the modules in the `Codata.Musical` directory, - the functions `fromMusical` and `toMusical` defined in: - ``` - Codata.Musical.Colist - Codata.Musical.Conat - Codata.Musical.Cofin - Codata.Musical.M - Codata.Musical.Stream - ``` - have been moved to a new module `Codata.Musical.Conversion` and renamed to - `X.fromMusical` and `X.toMusical` for each of `Codata.Musical.X`. - -* In order to maintain the safety of `Data.Container(.Indexed)`, the greatest fixpoint - of containers, `ν`, has been moved from `Data.Container(.Indexed)` to a new module - `Data.Container(.Indexed).Fixpoints.Guarded` which also re-exports the least fixpoint. - -#### Other - -* Replaced existing O(n) implementation of `Data.Nat.Binary.fromℕ` with a new O(log n) - implementation. The old implementation is maintained under `Data.Nat.Binary.fromℕ'` - and proven to be equivalent to the new one. - -* `Data.Maybe.Base` now re-exports the definition of `Maybe` given by - `Agda.Builtin.Maybe`. The `Foreign.Haskell` modules and definitions - corresponding to `Maybe` have been removed. See the release notes of - Agda 2.6.2 for more information. - -Deprecated modules ------------------- - -Deprecated names ----------------- - -New modules ------------ - -* New module for making system calls during type checking: - ```agda - Reflection.External - ``` - -* New modules for universes and annotations of reflected syntax: - ``` - Reflection.Universe - Reflection.Annotated - Reflection.Annotated.Free - ``` - -* Added new module for unary relations over sized types now that `Size` - lives in it's own universe since Agda 2.6.2. - ```agda - Relation.Unary.Sized - ``` - -* Metrics specialised to co-domains with rational numbers: - ``` - Function.Metric.Rational - Function.Metric.Rational.Definitions - Function.Metric.Rational.Structures - Function.Metric.Rational.Bundles - ``` - -* Lists that contain every element of a type: - ``` - Data.List.Relation.Unary.Enumerates.Setoid - Data.List.Relation.Unary.Enumerates.Setoid.Properties - ``` - -* (Unsafe) sized W type: - ``` - Data.W.Sized - ``` - -* (Unsafe) container fixpoints: - ``` - Data.Container.Fixpoints.Sized - ``` - -Other minor additions ---------------------- - -* Added new relations to `Data.Fin.Base`: - ```agda - _≥_ = ℕ._≥_ on toℕ - _>_ = ℕ._>_ on toℕ - ``` - -* Added new proofs to `Data.Fin.Induction`: - ```agda - >-wellFounded : WellFounded {A = Fin n} _>_ - - <-weakInduction : P zero → (∀ i → P (inject₁ i) → P (suc i)) → ∀ i → P i - >-weakInduction : P (fromℕ n) → (∀ i → P (suc i) → P (inject₁ i)) → ∀ i → P i - ``` - -* Added new proofs to `Relation.Binary.Properties.Setoid`: - ```agda - respʳ-flip : _≈_ Respectsʳ (flip _≈_) - respˡ-flip : _≈_ Respectsˡ (flip _≈_) - ``` - -* Added new function to `Data.Fin.Base`: - ```agda - pinch : Fin n → Fin (suc n) → Fin n - ``` - -* Added new proofs to `Data.Fin.Properties`: - ```agda - pinch-surjective : Surjective _≡_ (pinch i) - pinch-mono-≤ : (pinch i) Preserves _≤_ ⟶ _≤_ - ``` - -* Added new proofs to `Data.Nat.Binary.Properties`: - ```agda - fromℕ≡fromℕ' : fromℕ ≗ fromℕ' - toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id - fromℕ'-homo-+ : fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n - ``` - -* Rewrote proofs in `Data.Nat.Binary.Properties` for new implementation of `fromℕ`: - ```agda - toℕ-fromℕ : toℕ ∘ fromℕ ≗ id - fromℕ-homo-+ : fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n - ``` - -* Added new proof to `Data.Nat.DivMod`: - ```agda - m/n≤m : (m / n) {≢0} ≤ m - ``` - -* Added new type in `Size`: - ```agda - SizedSet ℓ = Size → Set ℓ - ``` +* The only change over v1.7 is that the library's Cabal file is now compatible with GHC 9.2. diff --git a/README.agda b/README.agda index 8c0f85c3c3..520a1d6e1f 100644 --- a/README.agda +++ b/README.agda @@ -3,7 +3,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 1.7 +-- The Agda standard library, version 1.7.1 -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, @@ -18,8 +18,7 @@ module README where -- Noam Zeilberger and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.1 and --- 2.6.1.3. +-- This version of the library has been tested using Agda 2.6.2. -- The library comes with a .agda-lib file, for use with the library -- management system. diff --git a/README.md b/README.md index 2196b11fef..16a2f10959 100644 --- a/README.md +++ b/README.md @@ -5,9 +5,6 @@ The Agda standard library ========================= -**NOTE**: The library is currently gearing up for the release of v2.6.2 therefore the -`master` branch is currently only compatible with release candidate 1 of Agda-2.6.2! - The standard library aims to contain all the tools needed to write both programs and proofs easily. While we always try and write efficient code, we prioritize ease of proof over type-checking and normalization diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index 06dfa0b0a5..f836c9279b 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -1,5 +1,5 @@ name: agda-stdlib-utils -version: 1.7 +version: 1.7.1 cabal-version: >= 1.10 build-type: Simple description: Helper programs. diff --git a/notes/installation-guide.md b/notes/installation-guide.md index 04751c61fb..3e9e941842 100644 --- a/notes/installation-guide.md +++ b/notes/installation-guide.md @@ -1,19 +1,19 @@ Installation instructions ========================= -Use version v1.7 of the standard library with Agda 2.6.2. +Use version v1.7.1 of the standard library with Agda 2.6.2. 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v1.7 of the standard library. This can either be +2. Download the tarball of v1.7.1 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.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.1.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `1.7` with any other version of the library you desire. + you can replace `1.7.1` 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: @@ -24,14 +24,14 @@ Use version v1.7 of the standard library with Agda 2.6.2. 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-1.7 + cd agda-stdlib-1.7.1 cabal install ``` 5. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-1.7/standard-library.agda-lib + $HERE/agda-stdlib-1.7.1/standard-library.agda-lib ``` Now, the standard library is ready to be used either: diff --git a/standard-library.agda-lib b/standard-library.agda-lib index eb01ba1fa6..9b4bd0bdfe 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,2 +1,2 @@ -name: standard-library-1.7 +name: standard-library-1.7.1 include: src