[ new ] golden testing framework

.github/workflows/ci-ubuntu.yml

@@ -68,12 +68,12 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/master' \
              || '${{ github.base_ref }}' == 'master' ]]; then
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.6.1.3.20210524" >> $GITHUB_ENV;
+            echo "AGDA_COMMIT=tags/v2.6.2" >> $GITHUB_ENV;
             echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
           elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
                || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=tags/v2.6.1.3.20210524" >> $GITHUB_ENV;
+            echo "AGDA_COMMIT=tags/v2.6.2" >> $GITHUB_ENV;
             echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
           fi
 
@@ -130,7 +130,7 @@ jobs:
           cd ..
 
 ########################################################################
-## TESTING AND DEPLOYMENT
+## TESTING
 ########################################################################
 
       # By default github actions do not pull the repo
@@ -139,13 +139,22 @@ jobs:
 
       - name: Test stdlib
         run: |
-          ${{ env.CABAL_INSTALL }} agda-stdlib-utils.cabal
           cabal run GenerateEverything
           cp travis/* .
           ./index.sh
           ${{ env.AGDA }} --safe EverythingSafe.agda
           ${{ env.AGDA }} index.agda
 
+      - name: Golden testing
+        run: |
+          ${{ env.CABAL_INSTALL }} --lib clock
+          make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
+
+
+########################################################################
+## DOC DEPLOYMENT
+########################################################################
+
       # We start by retrieving the currently deployed docs
       # We remove the content that is in the directory we are going to populate
       # so that stale files corresponding to deleted modules do not accumulate.
@@ -157,25 +166,11 @@ jobs:
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
           ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
 
-      # This is a massive hack at the moment
-      # - name: Compile stdlib
-      #   run: |
-      #     ${{ env.AGDA }} -c --no-main --ghc-dont-call-ghc --compile-dir=tmp Everything.agda
-      #     cd tmp
-      #     yes | cabal init --interactive
-      #     head -n -17 tmp.cabal > tmp
-      #     mv tmp tmp.cabal
-      #     cat ../travis/ghc-options >> tmp.cabal
-      #     cabal build
-
-##          ${{ env.AGDA }} -c README/Foreign/Haskell.agda && ./Haskell
-
-
       - name: Deploy HTML
         uses: JamesIves/[email protected]
         if: ${{ success() && env.AGDA_DEPLOY }}
 
         with:
           branch: gh-pages
           folder: html
-          git-config-name: Github Actions
+          git-config-name: Github Actions

.gitignore

@@ -19,7 +19,11 @@ Everything.agda
 EverythingSafe.agda
 EverythingSafeGuardedness.agda
 EverythingSafeSizedTypes.agda
+failures
 GenerateEverything
 Haskell
 html
+log
 MAlonzo
+output
+runtests

CHANGELOG.md

@@ -6,12 +6,53 @@ The library has been tested using Agda 2.6.2.
 Highlights
 ----------
 
+* A golden testing library in `Test.Golden`. This allows you to run a set
+  of tests and make sure their output matches an expected `golden' value.
+  The test runner has many options: filtering tests by name, dumping the
+  list of failures to a file, timing the runs, coloured output, etc.
+  Cf. the comments in `Test.Golden` and the standard library's own tests
+  in `tests/` for documentation on how to use the library.
+
 Bug-fixes
 ---------
 
+* In `System.Exit`, the `ExitFailure` constructor is now carrying an integer
+  rather than a natural. The previous binding was incorrectly assuming that
+  all exit codes where non-negative.
+
 Non-backwards compatible changes
 --------------------------------
 
+* In `Text.Pretty`, `Doc` is now a record rather than a type alias. This
+  helps Agda reconstruct the `width` parameter when the module is opened
+  without it being applied. In particular this allows users to write
+  width-generic pretty printers and only pick a width when calling the
+  renderer by using this import style:
+  ```
+  open import Text.Pretty using (Doc; render)
+  --                      ^-- no width parameter for Doc & render
+  open module Pretty {w} = Text.Pretty w hiding (Doc; render)
+  --                 ^-- implicit width parameter for the combinators
+
+  pretty : Doc w
+  pretty = ? -- you can use the combinators here and there won't be any
+             -- issues related to the fact that `w` cannot be reconstructed
+             -- anymore
+
+  main = do
+    -- you can now use the same pretty with different widths:
+    putStrLn $ render 40 pretty
+    putStrLn $ render 80 pretty
+  ```
+
+* In `Text.Regex.Search` the `searchND` function finding infix matches has
+  been tweaked to make sure the returned solution is a local maximum in terms
+  of length. It used to be that we would make the match start as late as
+  possible and finish as early as possible. It's now the reverse.
+
+  So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
+  will return "Main.agdai" when it used to be happy to just return "n.agda".
+
 Deprecated modules
 ------------------
 
@@ -27,6 +68,29 @@ New modules
   Algebra.Morphism.Construct.Identity
   ```
 
+* Show module for unnormalised rationals:
+  ```
+  Data.Rational.Unnormalised.Show
+  ```
+
+* Various system types and primitives:
+  ```
+  System.Clock.Primitive
+  System.Clock
+  System.Console.ANSI
+  System.Directory.Primitive
+  System.Directory
+  System.FilePath.Posix.Primitive
+  System.FilePath.Posix
+  System.Process.Primitive
+  System.Process
+  ```
+
+* A golden testing library with test pools, an options parser, a runner:
+  ```
+  Test.Golden
+  ```
+
 Other minor additions
 ---------------------
 
@@ -53,3 +117,39 @@ Other minor additions
   ∧-isCommutativeSemigroup : IsCommutativeSemigroup ∧
   ```
   and their corresponding algebraic substructures.
+
+* In `Data.String.Properties`:
+  ```
+  ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
+  ≤-decTotalOrder-≈   :  DecTotalOrder _ _ _
+  ```
+
+* In `IO`:
+  ```
+  Colist.forM  : Colist A → (A → IO B) → IO (Colist B)
+  Colist.forM′ : Colist A → (A → IO B) → IO ⊤
+
+  List.forM  : List A → (A → IO B) → IO (List B)
+  List.forM′ : List A → (A → IO B) → IO ⊤
+  ```
+
+* In `IO.Base`:
+  ```
+  lift! : IO A → IO (Lift b A)
+  _<$_  : B → IO A → IO B
+  _=<<_ : (A → IO B) → IO A → IO B
+  _<<_  : IO B → IO A → IO B
+  lift′ : Prim.IO ⊤ → IO {a} ⊤
+
+  when   : Bool → IO {a} ⊤ → IO ⊤
+  unless : Bool → IO {a} ⊤ → IO ⊤
+
+  whenJust  : Maybe A → (A → IO {a} ⊤) → IO ⊤
+  untilJust : IO (Maybe A) → IO A
+  ```
+
+* In `System.Exit`:
+  ```
+  isSuccess : ExitCode → Bool
+  isFailure : ExitCode → Bool
+  ```

GNUmakefile

@@ -10,6 +10,9 @@ AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
 test: Everything.agda check-whitespace
 	$(AGDA) -i. -isrc README.agda
 
+testsuite:
+	$(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only)
+
 check-whitespace:
 	cabal exec -- fix-whitespace --check
 

GenerateEverything.hs

@@ -56,10 +56,19 @@ unsafeModules = map modToFile
   , "IO.Primitive.Infinite"
   , "IO.Primitive.Finite"
   , "Relation.Binary.PropositionalEquality.TrustMe"
+  , "System.Clock"
+  , "System.Clock.Primitive"
+  , "System.Directory"
+  , "System.Directory.Primitive"
   , "System.Environment"
   , "System.Environment.Primitive"
   , "System.Exit"
   , "System.Exit.Primitive"
+  , "System.FilePath.Posix"
+  , "System.FilePath.Posix.Primitive"
+  , "System.Process"
+  , "System.Process.Primitive"
+  , "Test.Golden"
   , "Text.Pretty.Core"
   , "Text.Pretty"
   ] ++ sizedTypesModules

src/Data/Rational/Unnormalised/Show.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing unnormalised rational numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Rational.Unnormalised.Show where
+
+import Data.Integer.Show as ℤ
+open import Data.Rational.Unnormalised.Base
+open import Data.String.Base using (String; _++_)
+
+show : ℚᵘ → String
+show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)

src/Data/String/Properties.agda

@@ -129,6 +129,18 @@ x <? y = StrictLex.<-decidable Charₚ._≟_ Charₚ._<?_ (toList x) (toList y)
     toList
     (StrictLex.≤-isDecPartialOrder Charₚ.<-isStrictTotalOrder)
 
+≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
+≤-isDecTotalOrder-≈ =
+  On.isDecTotalOrder
+    toList
+    (StrictLex.≤-isDecTotalOrder Charₚ.<-isStrictTotalOrder)
+
+≤-decTotalOrder-≈ :  DecTotalOrder _ _ _
+≤-decTotalOrder-≈ =
+  On.decTotalOrder
+    (StrictLex.≤-decTotalOrder Charₚ.<-strictTotalOrder)
+    toList
+
 ≤-decPoset-≈ : DecPoset _ _ _
 ≤-decPoset-≈ =
   On.decPoset

src/IO.agda

@@ -13,7 +13,7 @@ open import Codata.Musical.Costring
 open import Data.Unit.Polymorphic.Base
 open import Data.String.Base
 import Data.Unit.Base as Unit0
-open import Function.Base using (_∘_)
+open import Function.Base using (_∘_; flip)
 import IO.Primitive as Prim
 open import Level
 
@@ -54,6 +54,12 @@ module Colist where
   mapM′ : (A → IO B) → Colist A → IO ⊤
   mapM′ f = sequence′ ∘ map f
 
+  forM : Colist A → (A → IO B) → IO (Colist B)
+  forM = flip mapM
+
+  forM′ : Colist A → (A → IO B) → IO ⊤
+  forM′ = flip mapM′
+
 module List where
 
   open import Data.List.Base
@@ -75,6 +81,12 @@ module List where
   mapM′ : (A → IO B) → List A → IO ⊤
   mapM′ f = sequence′ ∘ map f
 
+  forM : List A → (A → IO B) → IO (List B)
+  forM = flip mapM
+
+  forM′ : List A → (A → IO B) → IO ⊤
+  forM′ = flip mapM′
+
 ------------------------------------------------------------------------
 -- Simple lazy IO