Changes for release of v1.7.3 (#2141)

Author: andreasabel

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.

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.

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"

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.

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

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:

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)
 

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))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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