GNU bug report logs - #66775
[PATCH 0/6] Update Agda and libraries to 2.6.4

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 66775 in the body.
You can then email your comments to 66775 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: guix-patches <at> gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 0/6] Update Agda and libraries to 2.6.4
Date: Fri, 27 Oct 2023 20:11:52 +0200

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

Message #8 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 1/6] gnu: Add ghc-text-icu.
Date: Fri, 27 Oct 2023 20:14:01 +0200

From: Josselin Poiret <dev <at> 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

Message #11 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 2/6] gnu: agda: Update to 2.6.4.
Date: Fri, 27 Oct 2023 20:14:02 +0200

From: Josselin Poiret <dev <at> 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 <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> 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 <at> 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

Message #14 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 3/6] gnu: agda-stdlib: Update to 1.7.3.
Date: Fri, 27 Oct 2023 20:14:03 +0200

From: Josselin Poiret <dev <at> 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

Message #17 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 4/6] gnu: agda-categories: Adapt to agda-stdlib 1.7.3.
Date: Fri, 27 Oct 2023 20:16:27 +0200

From: Josselin Poiret <dev <at> 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 <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Wed, 25 Oct 2023 22:15:43 +0200
+Subject: [PATCH] Bump stdlib to 1.7.3
+
+From: Josselin Poiret <dev <at> 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

Message #20 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 5/6] gnu: agda-cubical: Update to 0.6.
Date: Fri, 27 Oct 2023 20:16:28 +0200

From: Josselin Poiret <dev <at> 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

Message #23 received at 66775 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 6/6] gnu: agda-1lab: Update to
 549fdb1c948a975e90e70f871993a4a4239aa280.
Date: Fri, 27 Oct 2023 20:16:29 +0200

From: Josselin Poiret <dev <at> 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

Message #28 received at 66775-done <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775-done <at> debbugs.gnu.org
Subject: Re: [PATCH 0/6] Update Agda and libraries to 2.6.4
Date: Tue, 14 Nov 2023 14:13:34 +0100

[Message part 1 (text/plain, inline)]

Hi,

Josselin Poiret <dev <at> 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

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.