[bug#66775] [PATCH 0/6] Update Agda and libraries to 2.6.4

[bug#66775] [PATCH 0/6] Update Agda and libraries to 2.6.4

[Josselin Poiret via Guix-patches via]

Hello everyone,

Small patchset, just updating Agda to the latest release.  All libraries should
work with this.

Best,

Josselin Poiret (6):
  gnu: Add ghc-text-icu.
  gnu: agda: Update to 2.6.4.
  gnu: agda-stdlib: Update to 1.7.3.
  gnu: agda-categories: Adapt to agda-stdlib 1.7.3.
  gnu: agda-cubical: Update to 0.6.
  gnu: agda-1lab: Update to 549fdb1c948a975e90e70f871993a4a4239aa280.

 gnu/local.mk                                  |  2 +
 gnu/packages/agda.scm                         | 37 ++++++++------
 gnu/packages/haskell-xyz.scm                  | 41 +++++++++++++++
 .../agda-categories-use-stdlib-1.7.3.patch    | 28 ++++++++++
 gnu/packages/patches/agda-use-sphinx-5.patch  | 51 +++++++++++++++++++
 5 files changed, 143 insertions(+), 16 deletions(-)
 create mode 100644 gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch
 create mode 100644 gnu/packages/patches/agda-use-sphinx-5.patch


base-commit: 2de30042674197fe451c220745186e36465d06e2
-- 
2.41.0

[bug#66775] [PATCH 1/6] gnu: Add ghc-text-icu.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

* gnu/packages/haskell-xyz.scm (ghc-text-icu): New variable.

Change-Id: I553f1fef4e76aeea6d09901917fd5d6032c23d46
---
 gnu/packages/haskell-xyz.scm | 41 ++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index c02fd007f9..b1a038bb09 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -65,6 +65,7 @@ (define-module (gnu packages haskell-xyz)
   #:use-module (gnu packages haskell-check)
   #:use-module (gnu packages haskell-crypto)
   #:use-module (gnu packages haskell-web)
+  #:use-module (gnu packages icu4c)
   #:use-module (gnu packages libffi)
   #:use-module (gnu packages linux)
   #:use-module (gnu packages llvm)
@@ -8352,6 +8353,46 @@ (define-public ghc-text-conversions
     (description "Safe conversions between textual types")
     (license license:isc)))
 
+(define-public ghc-text-icu
+  (package
+    (name "ghc-text-icu")
+    (version "0.8.0.4")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (hackage-uri "text-icu" version))
+       (sha256
+        (base32 "1yj0jdjrsx12sy6lj1gizb2ys5likp9rcv8ryc6sjf2dw74097rd"))))
+    (build-system haskell-build-system)
+    (properties '((upstream-name . "text-icu")))
+    (inputs (list icu4c))
+    (native-inputs (list ghc-hunit
+                         ghc-quickcheck
+                         ghc-random
+                         ghc-test-framework
+                         ghc-test-framework-hunit
+                         ghc-test-framework-quickcheck2
+                         pkg-config))
+    (home-page "https://github.com/haskell/text-icu")
+    (synopsis "Bindings to the ICU library")
+    (description
+     "Haskell bindings to the International Components for Unicode (ICU) libraries.
+These libraries provide robust and full-featured Unicode services on a wide
+variety of platforms. .  Features include: . * Both pure and impure bindings, to
+allow for fine control over efficiency and ease of use. . * Breaking of strings
+on character, word, sentence, and line boundaries. . * Access to the Unicode
+Character Database (UCD) of character metadata. . * String collation functions,
+for locales where the conventions for lexicographic ordering differ from the
+simple numeric ordering of character codes. . * Character set conversion
+functions, allowing conversion between Unicode and over 220 character encodings.
+. * Unicode normalization. (When implementations keep strings in a normalized
+form, they can be assured that equivalent strings have a unique binary
+representation.) . * Regular expression search and replace. . * Security checks
+for visually confusable (spoofable) strings. . * Bidirectional Unicode algorithm
+. * Calendar objects holding dates and times. . * Number and calendar
+formatting.")
+    (license license:bsd-3)))
+
 (define-public ghc-text-short
   (package
     (name "ghc-text-short")
-- 
2.41.0

[bug#66775] [PATCH 2/6] gnu: agda: Update to 2.6.4.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

* gnu/packages/agda.scm (agda): Update to 2.6.4.  Also build with
optimizations and cluster counting support.
* gnu/packages/patches/agda-use-sphinx-5.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.

Change-Id: I98a66678ec401b9201d9fd3a0f606fff9767b4bc
---
 gnu/local.mk                                 |  1 +
 gnu/packages/agda.scm                        | 11 +++--
 gnu/packages/patches/agda-use-sphinx-5.patch | 51 ++++++++++++++++++++
 3 files changed, 60 insertions(+), 3 deletions(-)
 create mode 100644 gnu/packages/patches/agda-use-sphinx-5.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index a00884a7c6..47626a6926 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -900,6 +900,7 @@ dist_patch_DATA =						\
   %D%/packages/patches/agda-categories-remove-incompatible-flags.patch	\
   %D%/packages/patches/agda-categories-use-find.patch	\
   %D%/packages/patches/agda-libdirs-env-variable.patch	\
+  %D%/packages/patches/agda-use-sphinx-5.patch	\
   %D%/packages/patches/agda-stdlib-use-runhaskell.patch	\
   %D%/packages/patches/agg-am_c_prototype.patch			\
   %D%/packages/patches/agg-2.5-gcc8.patch			\
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 8258818722..8c82701596 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -44,7 +44,7 @@ (define-module (gnu packages agda)
 (define-public agda
   (package
     (name "agda")
-    (version "2.6.3")
+    (version "2.6.4")
     (source
      (origin
        (method git-fetch)
@@ -53,12 +53,14 @@ (define-public agda
              (commit (string-append "v" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))
-       (patches (search-patches "agda-libdirs-env-variable.patch"))))
+        (base32 "0n4avd58j45rdcmnwgrmz5s0ril0z4n2z711mwwbahl50f7359ky"))
+       (patches (search-patches "agda-libdirs-env-variable.patch"
+                                "agda-use-sphinx-5.patch"))))
     (build-system haskell-build-system)
     (inputs
      (list ghc-aeson
            ghc-alex
+           ghc-ansi-terminal
            ghc-async
            ghc-blaze-html
            ghc-boxes
@@ -73,9 +75,11 @@ (define-public agda
            ghc-monad-control
            ghc-murmur-hash
            ghc-parallel
+           ghc-peano
            ghc-regex-tdfa
            ghc-split
            ghc-strict
+           ghc-text-icu
            ghc-unordered-containers
            ghc-uri-encode
            ghc-vector-hashtables
@@ -91,6 +95,7 @@ (define-public agda
                        (guix build utils)
                        (srfi srfi-26)
                        (ice-9 match))
+           #:configure-flags #~(list "-foptimise-heavily" "-fenable-cluster-counting")
            #:phases
            #~(modify-phases %standard-phases
                ;; This allows us to call the 'agda' binary before installing.
diff --git a/gnu/packages/patches/agda-use-sphinx-5.patch b/gnu/packages/patches/agda-use-sphinx-5.patch
new file mode 100644
index 0000000000..19fcf252f9
--- /dev/null
+++ b/gnu/packages/patches/agda-use-sphinx-5.patch
@@ -0,0 +1,51 @@
+From 99ed1b59ef73fd35053810f6a09e034e1513caee Mon Sep 17 00:00:00 2001
+Message-ID: <99ed1b59ef73fd35053810f6a09e034e1513caee.1698243851.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Wed, 25 Oct 2023 16:23:32 +0200
+Subject: [PATCH] Revert "Docs: bump Sphinx to 6.0.0"
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+This reverts commit 40dd42eaa7c04e134fa38cb4f958414a76df27a7.
+---
+ doc/user-manual/conf.py          | 5 ++---
+ doc/user-manual/requirements.txt | 4 ++--
+ 2 files changed, 4 insertions(+), 5 deletions(-)
+
+diff --git a/doc/user-manual/conf.py b/doc/user-manual/conf.py
+index 127f6582dc..d737ede19b 100644
+--- a/doc/user-manual/conf.py
++++ b/doc/user-manual/conf.py
+@@ -35,7 +35,7 @@ release = version
+ #
+ # If your change the version here also change it in the
+ # `requirements.txt` file [Issue #1936].
+-needs_sphinx = '6.0.0'
++needs_sphinx = '5.0.0'
+ 
+ # Add any Sphinx extension module names here, as strings. They can be
+ # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+@@ -43,8 +43,7 @@ needs_sphinx = '6.0.0'
+ extensions = [
+     'sphinx.ext.imgmath',
+     'sphinx.ext.ifconfig',
+-    'sphinx.ext.imgconverter',
+-    'sphinxcontrib.jquery'
++    'sphinx.ext.imgconverter'
+ ]
+ 
+ # Add any paths that contain templates here, relative to this directory.
+diff --git a/doc/user-manual/requirements.txt b/doc/user-manual/requirements.txt
+index 384b1466b4..656e6c9ac0 100644
+--- a/doc/user-manual/requirements.txt
++++ b/doc/user-manual/requirements.txt
+@@ -1,2 +1,2 @@
+-Sphinx           >= 7.2.5
+-sphinx_rtd_theme >= 1.3.0
++Sphinx           >= 5.0.0, != 5.2.0.post0
++sphinx_rtd_theme >= 1.0
+
+base-commit: 08b79a684d712ba3dc4b26e5052ec49f49f5ff6c
+-- 
+2.41.0
+
-- 
2.41.0

[bug#66775] [PATCH 3/6] gnu: agda-stdlib: Update to 1.7.3.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

* gnu/packages/agda.scm (agda-stdlib): Update to 1.7.3.

Change-Id: Ic941073814a6a2150d470fc05218dc8d19954445
---
 gnu/packages/agda.scm | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 8c82701596..538df99bf4 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -199,7 +199,7 @@ (define-public agda-ial
 (define-public agda-stdlib
   (package
     (name "agda-stdlib")
-    (version "1.7.2")
+    (version "1.7.3")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -208,7 +208,7 @@ (define-public agda-stdlib
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy"))))
+                "0y6rns64rrkh8hw7mamcf6797329pi4ravpak5zijpnkzdagmlmy"))))
     (build-system agda-build-system)
     (arguments
      (list
-- 
2.41.0

[bug#66775] [PATCH 4/6] gnu: agda-categories: Adapt to agda-stdlib 1.7.3.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

Change-Id: I25f16d55f14465a1dae882fd8ec47a95f8598e5c
---
 gnu/local.mk                                  |  1 +
 gnu/packages/agda.scm                         |  3 +-
 .../agda-categories-use-stdlib-1.7.3.patch    | 28 +++++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index 47626a6926..995771f73c 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -899,6 +899,7 @@ dist_patch_DATA =						\
   %D%/packages/patches/aegisub-make43.patch			\
   %D%/packages/patches/agda-categories-remove-incompatible-flags.patch	\
   %D%/packages/patches/agda-categories-use-find.patch	\
+  %D%/packages/patches/agda-categories-use-stdlib-1.7.3.patch	\
   %D%/packages/patches/agda-libdirs-env-variable.patch	\
   %D%/packages/patches/agda-use-sphinx-5.patch	\
   %D%/packages/patches/agda-stdlib-use-runhaskell.patch	\
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 538df99bf4..f206542845 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -246,7 +246,8 @@ (define-public agda-categories
                (base32
                 "0xwgm2mfl2pxipsv31bin8p14y1yhd9n27lv3clvsxd4z9yc034m"))
               (patches (search-patches "agda-categories-remove-incompatible-flags.patch"
-                                       "agda-categories-use-find.patch"))))
+                                       "agda-categories-use-find.patch"
+                                       "agda-categories-use-stdlib-1.7.3.patch"))))
     (build-system agda-build-system)
     (arguments
      (list
diff --git a/gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch b/gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch
new file mode 100644
index 0000000000..32680b99d7
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch
@@ -0,0 +1,28 @@
+From 76d3863a5e6e7b9ee948f10a3faec3420a2020f1 Mon Sep 17 00:00:00 2001
+Message-ID: <76d3863a5e6e7b9ee948f10a3faec3420a2020f1.1698265016.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Wed, 25 Oct 2023 22:15:43 +0200
+Subject: [PATCH] Bump stdlib to 1.7.3
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+---
+ agda-categories.agda-lib | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
+index 5b19c405..4d63d415 100644
+--- a/agda-categories.agda-lib
++++ b/agda-categories.agda-lib
+@@ -1,3 +1,3 @@
+ name: agda-categories
+-depend: standard-library-1.7.2
++depend: standard-library-1.7.3
+ include: src/
+
+base-commit: 9d61106740147a67fa2cae0a89ac066897b24a51
+prerequisite-patch-id: 508dabd923ba9ac1ee4d8dab6697432b4bd8ba18
+prerequisite-patch-id: b5f39b4fc9e4c9993ab31300de041ed2c7eb696b
+-- 
+2.41.0
+
-- 
2.41.0

[bug#66775] [PATCH 5/6] gnu: agda-cubical: Update to 0.6.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

* gnu/packages/agda.scm (agda-cubical): Update to 0.6.

Change-Id: I1d6edc44755260e505985fb974c632ec6fff2b49
---
 gnu/packages/agda.scm | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index f206542845..be3b625da7 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -265,12 +265,9 @@ (define-public agda-categories
     (license license:expat)))
 
 (define-public agda-cubical
-  ;; Upstream's HEAD follows the latest Agda release, but they don't release
-  ;; until a newer Agda release comes up, so their releases are always one
-  ;; version late.
   (package
     (name "agda-cubical")
-    (version "0.5")
+    (version "0.6")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -279,7 +276,7 @@ (define-public agda-cubical
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0yfg7gr55n08ly1qgzpcp16s15k1abycppbcdi9lzg1hjryqxcg3"))))
+                "0zq0z328zcjmm43mrv2ks27i1dnbylcf8mhzja2hd4gvz1kq1ays"))))
     (build-system agda-build-system)
     (arguments
      (list
-- 
2.41.0

[bug#66775] [PATCH 6/6] gnu: agda-1lab: Update to 549fdb1c948a975e90e70f871993a4a4239aa280.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@jpoiret.xyz>

* gnu/packages/agda.scm (agda-1lab): Update to
549fdb1c948a975e90e70f871993a4a4239aa280.

Change-Id: Iad77350fea5a6378e836cbd18c1f4a51bd5a5f0e
---
 gnu/packages/agda.scm | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index be3b625da7..c2ebf09e4a 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -293,10 +293,10 @@ (define-public agda-cubical
     (license license:expat)))
 
 (define-public agda-1lab
-  ;; Upstream doesn't do releases (yet).  Use a commit that builds with 2.6.3,
+  ;; Upstream doesn't do releases (yet).  Use a commit that builds with 2.6.4,
   ;; since they use Agda HEAD.
-  (let* ((revision "1")
-         (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6"))
+  (let* ((revision "2")
+         (commit "549fdb1c948a975e90e70f871993a4a4239aa280"))
     (package
       (name "agda-1lab")
       (version (git-version "0.0" revision commit))
@@ -309,10 +309,12 @@ (define-public agda-1lab
          (file-name (git-file-name name version))
          (sha256
           (base32
-           "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx"))))
+           "1k4zj8dibyplakpxaw4a8hpsaqhakynjb83dqxrva4h4ssj6gkqj"))))
       (build-system agda-build-system)
       (arguments
-       (list #:plan '(("src/index\\.lagda\\.md$"))))
+       ;; Check files individually first, to avoid running out of heap :(
+       (list #:plan '(("src/.+/.+\\.lagda\\.md$")
+                      ("src/index\\.lagda\\.md$"))))
       (synopsis "Reference resource for mathematics done in Homotopy Type Theory")
       (description "A formalised, cross-linked reference resource for
 mathematics done in Homotopy Type Theory.  Unlike the HoTT book, the 1lab is
-- 
2.41.0

bug#66775: [PATCH 0/6] Update Agda and libraries to 2.6.4

[Josselin Poiret via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 252 bytes --]

Hi,

Josselin Poiret <dev@jpoiret.xyz> writes:

> Small patchset, just updating Agda to the latest release.  All libraries should
> work with this.

Merged with bd0f2173210416e86281c1de8789e7cdab66dd57.  Closing.

Best,
-- 
Josselin Poiret

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 682 bytes --]