Bump versions to agda 2.8.0 and stdlib 2.3

.github/workflows/agda-ci.yml

@@ -25,27 +25,25 @@ jobs:
         # - os: windows-latest
         #   agda: 2.6.2.2
         - os: ubuntu-latest
-          agda: 2.6.3
+          agda: 2.8.0
 
     steps:
 
       # Checkout to $HOME empties $HOME so we have to do it before we put stuff there.
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Setup Agda
-        uses: wenkokke/setup-agda@latest
+        uses: agda/agda-setup-action@v1
         id:   setup
         with:
           agda-version: ${{ matrix.agda }}
-          # agda-stdlib-version: recommended
-          agda-stdlib-version: '1.7.1'
-          # agda-stdlib-default: true
+          agda-stdlib-version: '2.3'
 
       - name: Cache build
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         id:   cache
         with:
-          key: ${{ runner.os }}-agda-${{ steps.setup.outputs.agda-version }}
+          key: ${{ runner.os }}-agda-${{ matrix.agda }}
           # Don't have version of standard library. :-(
           # -std-lib-${{ matrix.std-lib }}
           path: |
@@ -57,7 +55,7 @@ jobs:
         working-directory: src
         run: agda Everything.agda --html
 
-      - uses: actions/upload-pages-artifact@v1
+      - uses: actions/upload-pages-artifact@v3
         with:
           path: src/html
 

.gitignore

@@ -32,3 +32,4 @@
 *.tdo
 *.agdai
 *~
+flake.lock

flake.nix

@@ -0,0 +1,16 @@
+{
+    description = "Continuous normalization";
+
+    inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+
+    outputs = { self, nixpkgs }:
+      let
+        system = "x86_64-linux";
+        pkgs = nixpkgs.legacyPackages.${system};
+        agda = pkgs.agda.withPackages (p: [ p.standard-library ]);
+      in {
+        devShells.${system}.default = pkgs.mkShell {
+          buildInputs = [ agda ];
+        };
+      };
+}

src/Delay.agda

@@ -1,10 +1,11 @@
 module Delay where
 
 open import Library
-open import Category.Applicative.Indexed
+open import Effect.Applicative.Indexed
+import Effect.Monad
 -- Coinductive delay monad.
 
-infix 10 _⇓_
+-- infix 10 _⇓_
 
 mutual
 
@@ -45,14 +46,11 @@ module Bind where
     force (x ∞>>= f) = force x >>= f
 
 delayMonad : ∀ {i} → RawMonad {f = lzero} (Delay i)
-delayMonad {i} = record
-  { return = now
-  ; _>>=_  = _>>=_ {i}
-  } where open Bind
+delayMonad {i} = Effect.Monad.mkRawMonad (Delay i) now (_>>=_ {i}) where open Bind
 
 module _ {i : Size} where
   open module DelayMonad = RawMonad (delayMonad {i = i})
-                           public renaming (_⊛_ to _<*>_)
+                           public
 open Bind public using (_∞>>=_)
 
 -- Map for ∞Delay
@@ -70,7 +68,6 @@ _=<<2_,_ : ∀ {i A B C} → (A → B → Delay i C) → Delay i A → Delay i B
 f =<<2 x , y = x >>= λ a → y >>= λ b → f a b
 
 -- Lifting a predicate to Delay (without convergence).
-
 mutual
   data Delay₁ i {A : Set} (P : A → Set) : Delay ∞ A → Set where
     now₁   : ∀{a}  → (p : P a) → Delay₁ i P (now a)
@@ -184,7 +181,7 @@ module ≈-Reasoning {i : Size} {A : Set} where
 
 module ∞≈-Reasoning {i : Size} {A : Set} where
   private module M = SetoidReasoning (∞≈setoid i A)
-  open M public using (begin_; _∎; _≡⟨⟩_; step-≡)
+  open M public using (begin_; _∎; step-≡-∣; step-≡)
   step-∞≈ = M.step-≈
   infixr 2 step-∞≈
   syntax step-∞≈ x y≈z x≈y = x ∞≈⟨ x≈y ⟩ y≈z

src/Library.agda

@@ -3,14 +3,14 @@
 module Library where
 
 open import Function public
-  hiding (_∋_)
+  hiding (_∋_; force)
 
 open import Level public
   using (Level) renaming (zero to lzero; suc to lsuc)
 
 open import Size public
 
-open import Category.Monad public
+open import Effect.Monad public
   using (RawMonad; module RawMonad)
 
 open import Data.Empty public

src/Main.agda-lib

@@ -1,3 +1,3 @@
 include: .
-depend: standard-library-1.7.1
+depend: standard-library-2.3
 flags: --sized-types