@@ -6,12 +6,53 @@ The library has been tested using Agda 2.6.2.
66Highlights
77----------
88
9+ * A golden testing library in ` Test.Golden ` . This allows you to run a set
10+ of tests and make sure their output matches an expected `golden' value.
11+ The test runner has many options: filtering tests by name, dumping the
12+ list of failures to a file, timing the runs, coloured output, etc.
13+ Cf. the comments in ` Test.Golden ` and the standard library's own tests
14+ in ` tests/ ` for documentation on how to use the library.
15+
916Bug-fixes
1017---------
1118
19+ * In ` System.Exit ` , the ` ExitFailure ` constructor is now carrying an integer
20+ rather than a natural. The previous binding was incorrectly assuming that
21+ all exit codes where non-negative.
22+
1223Non-backwards compatible changes
1324--------------------------------
1425
26+ * In ` Text.Pretty ` , ` Doc ` is now a record rather than a type alias. This
27+ helps Agda reconstruct the ` width ` parameter when the module is opened
28+ without it being applied. In particular this allows users to write
29+ width-generic pretty printers and only pick a width when calling the
30+ renderer by using this import style:
31+ ```
32+ open import Text.Pretty using (Doc; render)
33+ -- ^-- no width parameter for Doc & render
34+ open module Pretty {w} = Text.Pretty w hiding (Doc; render)
35+ -- ^-- implicit width parameter for the combinators
36+
37+ pretty : Doc w
38+ pretty = ? -- you can use the combinators here and there won't be any
39+ -- issues related to the fact that `w` cannot be reconstructed
40+ -- anymore
41+
42+ main = do
43+ -- you can now use the same pretty with different widths:
44+ putStrLn $ render 40 pretty
45+ putStrLn $ render 80 pretty
46+ ```
47+
48+ * In ` Text.Regex.Search ` the ` searchND ` function finding infix matches has
49+ been tweaked to make sure the returned solution is a local maximum in terms
50+ of length. It used to be that we would make the match start as late as
51+ possible and finish as early as possible. It's now the reverse.
52+
53+ So ` [a-zA-Z]+.agdai? ` run on "the path _ build/Main.agdai corresponds to"
54+ will return "Main.agdai" when it used to be happy to just return "n.agda".
55+
1556Deprecated modules
1657------------------
1758
@@ -27,6 +68,29 @@ New modules
2768 Algebra.Morphism.Construct.Identity
2869```
2970
71+ * Show module for unnormalised rationals:
72+ ```
73+ Data.Rational.Unnormalised.Show
74+ ```
75+
76+ * Various system types and primitives:
77+ ```
78+ System.Clock.Primitive
79+ System.Clock
80+ System.Console.ANSI
81+ System.Directory.Primitive
82+ System.Directory
83+ System.FilePath.Posix.Primitive
84+ System.FilePath.Posix
85+ System.Process.Primitive
86+ System.Process
87+ ```
88+
89+ * A golden testing library with test pools, an options parser, a runner:
90+ ```
91+ Test.Golden
92+ ```
93+
3094Other minor additions
3195---------------------
3296
@@ -53,3 +117,39 @@ Other minor additions
53117 ∧-isCommutativeSemigroup : IsCommutativeSemigroup ∧
54118```
55119 and their corresponding algebraic substructures.
120+
121+ * In ` Data.String.Properties ` :
122+ ```
123+ ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
124+ ≤-decTotalOrder-≈ : DecTotalOrder _ _ _
125+ ```
126+
127+ * In ` IO ` :
128+ ```
129+ Colist.forM : Colist A → (A → IO B) → IO (Colist B)
130+ Colist.forM′ : Colist A → (A → IO B) → IO ⊤
131+
132+ List.forM : List A → (A → IO B) → IO (List B)
133+ List.forM′ : List A → (A → IO B) → IO ⊤
134+ ```
135+
136+ * In ` IO.Base ` :
137+ ```
138+ lift! : IO A → IO (Lift b A)
139+ _<$_ : B → IO A → IO B
140+ _=<<_ : (A → IO B) → IO A → IO B
141+ _<<_ : IO B → IO A → IO B
142+ lift′ : Prim.IO ⊤ → IO {a} ⊤
143+
144+ when : Bool → IO {a} ⊤ → IO ⊤
145+ unless : Bool → IO {a} ⊤ → IO ⊤
146+
147+ whenJust : Maybe A → (A → IO {a} ⊤) → IO ⊤
148+ untilJust : IO (Maybe A) → IO A
149+ ```
150+
151+ * In ` System.Exit ` :
152+ ```
153+ isSuccess : ExitCode → Bool
154+ isFailure : ExitCode → Bool
155+ ```
0 commit comments