diff --git a/CHANGELOG.md b/CHANGELOG.md index 0183ec654f..8de9bf14ee 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,9 +1,18 @@ -Version 1.7.2 +Version 1.7.3 ============= -The library has been tested using Agda 2.6.3. +The library has been tested using Agda 2.6.4. -* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used - the `--without-K` flag now use the `--cubical-compatible` flag instead. - -* Updated the code using `primFloatToWord64` - the library API has remained unchanged. +* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4, + universe levels have been increased in the following definitions: + - `Data.Star.Decoration.DecoratedWith` + - `Data.Star.Pointer.Pointer` + - `Reflection.AnnotatedAST.Typeₐ` + - `Reflection.AnnotatedAST.AnnotationFun` + +* The following aliases have been added: + - `IO.Primitive.pure` as alias for `IO.Primitive.return` + - modules `Effect.*` as aliases for modules `Category.*` + + These allow to address said objects with the new name they will have in v2.0 of the library, + to ease the transition from v1.7.3 to v2.0. diff --git a/CHANGELOG/v1.7.2.md b/CHANGELOG/v1.7.2.md new file mode 100644 index 0000000000..0183ec654f --- /dev/null +++ b/CHANGELOG/v1.7.2.md @@ -0,0 +1,9 @@ +Version 1.7.2 +============= + +The library has been tested using Agda 2.6.3. + +* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used + the `--without-K` flag now use the `--cubical-compatible` flag instead. + +* Updated the code using `primFloatToWord64` - the library API has remained unchanged. diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000000..78e63bd810 --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,8 @@ +cff-version: 1.2.0 +message: "If you use this software, please cite it as below." +authors: +- name: "The Agda Community" +title: "Agda Standard Library" +version: 1.7.3 +date-released: 2023-10-15 +url: "https://github.com/agda/agda-stdlib" \ No newline at end of file diff --git a/README.agda b/README.agda index 1406d70967..1b5bc7f351 100644 --- a/README.agda +++ b/README.agda @@ -3,7 +3,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 1.7.2 +-- The Agda standard library, version 1.7.3 -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, @@ -18,7 +18,7 @@ module README where -- Noam Zeilberger and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.2. +-- This version of the library has been tested using Agda 2.6.4. -- The library comes with a .agda-lib file, for use with the library -- management system. diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index 6e8bc7b33b..b3860888ab 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -1,5 +1,5 @@ name: agda-stdlib-utils -version: 1.7.2 +version: 1.7.3 cabal-version: >= 1.10 build-type: Simple description: Helper programs. @@ -11,24 +11,26 @@ tested-with: GHC == 8.0.2 GHC == 8.8.4 GHC == 8.10.7 GHC == 9.0.2 - GHC == 9.2.1 - GHC == 9.4.4 + GHC == 9.2.8 + GHC == 9.4.7 + GHC == 9.6.3 + GHC == 9.8.1 executable GenerateEverything hs-source-dirs: . main-is: GenerateEverything.hs default-language: Haskell2010 default-extensions: PatternGuards, PatternSynonyms - build-depends: base >= 4.9.0.0 && < 4.18 + build-depends: base >= 4.9.0.0 && < 4.20 , directory >= 1.0.0.0 && < 1.4 , filemanip >= 0.3.6.2 && < 0.4 , filepath >= 1.4.1.0 && < 1.5 - , mtl >= 2.2.2 && < 2.3 + , mtl >= 2.2.2 && < 2.4 executable AllNonAsciiChars hs-source-dirs: . main-is: AllNonAsciiChars.hs default-language: Haskell2010 - build-depends: base >= 4.9.0.0 && < 4.18 + build-depends: base >= 4.9.0.0 && < 4.20 , filemanip >= 0.3.6.2 && < 0.4 - , text >= 1.2.3.0 && < 2.1 + , text >= 1.2.3.0 && < 2.2 diff --git a/notes/installation-guide.md b/notes/installation-guide.md index e51088aa6a..0086700170 100644 --- a/notes/installation-guide.md +++ b/notes/installation-guide.md @@ -1,19 +1,19 @@ Installation instructions ========================= -Use version v1.7.2 of the standard library with Agda 2.6.2. +Use version v1.7.3 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 v1.7.3 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/v1.7.3.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 `1.7.3` 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.2 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.2 + cd agda-stdlib-1.7.3 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.2/standard-library.agda-lib + $HERE/agda-stdlib-1.7.3/standard-library.agda-lib ``` Now, the standard library is ready to be used either: diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda index 24428a5843..170b5abb07 100644 --- a/src/Data/Star/Decoration.agda +++ b/src/Data/Star/Decoration.agda @@ -28,7 +28,7 @@ data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r) -- Decorating an edge with more information. data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T) - : Rel (NonEmpty (Star T)) p where + : Rel (NonEmpty (Star T)) (ℓ ⊔ r ⊔ p) where ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs) diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda index 6214e3e7dc..70dfdb94be 100644 --- a/src/Data/Star/Pointer.agda +++ b/src/Data/Star/Pointer.agda @@ -21,7 +21,7 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive data Pointer {r p q} {T : Rel I r} (P : EdgePred p T) (Q : EdgePred q T) - : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where + : Rel (Maybe (NonEmpty (Star T))) (ℓ ⊔ r ⊔ p ⊔ q) where step : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs))) (just (nonEmpty xs)) diff --git a/src/Effect/Applicative.agda b/src/Effect/Applicative.agda new file mode 100644 index 0000000000..859131b8a6 --- /dev/null +++ b/src/Effect/Applicative.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative where + +open import Category.Applicative public diff --git a/src/Effect/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda new file mode 100644 index 0000000000..58a7c6418a --- /dev/null +++ b/src/Effect/Applicative/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative.Indexed where + +open import Category.Applicative.Indexed public diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda new file mode 100644 index 0000000000..b28c57598f --- /dev/null +++ b/src/Effect/Applicative/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative.Predicate where + +open import Category.Applicative.Predicate public diff --git a/src/Effect/Comonad.agda b/src/Effect/Comonad.agda new file mode 100644 index 0000000000..45ea111c5a --- /dev/null +++ b/src/Effect/Comonad.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Comonad` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Comonad where + +open import Category.Comonad public diff --git a/src/Effect/Functor.agda b/src/Effect/Functor.agda new file mode 100644 index 0000000000..5c276929b6 --- /dev/null +++ b/src/Effect/Functor.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor where + +open import Category.Functor public diff --git a/src/Effect/Functor/Indexed.agda b/src/Effect/Functor/Indexed.agda new file mode 100644 index 0000000000..9d4efdef1f --- /dev/null +++ b/src/Effect/Functor/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor.Indexed where + +open import Category.Functor.Indexed public diff --git a/src/Effect/Functor/Predicate.agda b/src/Effect/Functor/Predicate.agda new file mode 100644 index 0000000000..a11b2cef64 --- /dev/null +++ b/src/Effect/Functor/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor.Predicate where + +open import Category.Functor.Predicate public diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda new file mode 100644 index 0000000000..c4df178be8 --- /dev/null +++ b/src/Effect/Monad.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad where + +open import Category.Monad public diff --git a/src/Effect/Monad/Continuation.agda b/src/Effect/Monad/Continuation.agda new file mode 100644 index 0000000000..357102eef6 --- /dev/null +++ b/src/Effect/Monad/Continuation.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Continuation` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Continuation where + +open import Category.Monad.Continuation public diff --git a/src/Effect/Monad/Indexed.agda b/src/Effect/Monad/Indexed.agda new file mode 100644 index 0000000000..8bed8e27eb --- /dev/null +++ b/src/Effect/Monad/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Indexed where + +open import Category.Monad.Indexed public diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda new file mode 100644 index 0000000000..80783e6148 --- /dev/null +++ b/src/Effect/Monad/Partiality.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality where + +open import Category.Monad.Partiality public diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda new file mode 100644 index 0000000000..f91e83b6d5 --- /dev/null +++ b/src/Effect/Monad/Partiality/All.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality.All` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality.All where + +open import Category.Monad.Partiality.All public diff --git a/src/Effect/Monad/Partiality/Instances.agda b/src/Effect/Monad/Partiality/Instances.agda new file mode 100644 index 0000000000..aa322c83ab --- /dev/null +++ b/src/Effect/Monad/Partiality/Instances.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality.Instances` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality.Instances where + +open import Category.Monad.Partiality.Instances public diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda new file mode 100644 index 0000000000..56d6dbe0a4 --- /dev/null +++ b/src/Effect/Monad/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Predicate where + +open import Category.Monad.Predicate public diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda new file mode 100644 index 0000000000..78d05ae0de --- /dev/null +++ b/src/Effect/Monad/Reader.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Reader` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Reader where + +open import Category.Monad.Reader public diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda new file mode 100644 index 0000000000..14ffbf6b5c --- /dev/null +++ b/src/Effect/Monad/State.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.State` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.State where + +open import Category.Monad.State public diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index 45ae1b5fc5..a0e15a3c5d 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -27,3 +27,6 @@ postulate {-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-} {-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-} {-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-} + +-- Forward compatibility with v2.0. +pure = return diff --git a/src/Reflection/Annotated.agda b/src/Reflection/Annotated.agda index ba63faf0fb..171dfe75c4 100644 --- a/src/Reflection/Annotated.agda +++ b/src/Reflection/Annotated.agda @@ -35,8 +35,8 @@ Annotation : ∀ ℓ → Set (suc ℓ) Annotation ℓ = ∀ {u} → ⟦ u ⟧ → Set ℓ -- An annotated type is a family over an Annotation and a reflected term. -Typeₐ : ∀ ℓ → Univ → Set (suc ℓ) -Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set ℓ +Typeₐ : ∀ ℓ → Univ → Set (suc (suc ℓ)) +Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set (suc ℓ) private variable @@ -168,7 +168,7 @@ mutual -- An annotation function computes the top-level annotation given a -- term annotated at all sub-terms. -AnnotationFun : Annotation ℓ → Set ℓ +AnnotationFun : Annotation ℓ → Set (suc ℓ) AnnotationFun Ann = ∀ u {t : ⟦ u ⟧} → Annotated′ Ann t → Ann t diff --git a/standard-library.agda-lib b/standard-library.agda-lib index 29885b7c5c..4f40cf4b61 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,4 +1,4 @@ -name: standard-library-1.7.2 +name: standard-library-1.7.3 include: src flags: --warning=noUnsupportedIndexedMatch