GNU bug report logs - #73421
[PATCH 0/5] Update Agda to 2.7.0.1 along with libraries.

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 73421 in the body.
You can then email your comments to 73421 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/5] Update Agda to 2.7.0.1 along with libraries.
Date: Sun, 22 Sep 2024 13:06:14 +0200

This patch series updates Agda and libraries to the latest upstream versions.

Josselin Poiret (5):
  gnu: agda: Update to 2.7.0.1.
  gnu: agda-stdlib: Update to 2.1.13
  gnu: agda-categories: Update to 0.2.0.
  gnu: agda-cubical: Update to 0.7.
  gnu: agda-1lab: Update to afcf848d367f906d6d07d1612fbd41d7dd8c978e.

 gnu/local.mk                                  |  2 +-
 gnu/packages/agda.scm                         | 30 ++++++++++---------
 .../agda-categories-use-newer-stdlib.patch    | 21 +++++++++++++
 .../agda-categories-use-stdlib-1.7.3.patch    | 28 -----------------
 4 files changed, 38 insertions(+), 43 deletions(-)
 create mode 100644 gnu/packages/patches/agda-categories-use-newer-stdlib.patch
 delete mode 100644 gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch


base-commit: b7c94d528875415ea7ec6225d88a6b3d55fa2e14
-- 
2.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 1/5] gnu: agda: Update to 2.7.0.1.
Date: Sun, 22 Sep 2024 13:17:16 +0200

From: Josselin Poiret <dev <at> jpoiret.xyz>

* gnu/packages/agda.scm (agda): Update to 2.7.0.1.

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

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 4afe583b2e..0e38d4e2d8 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.4")
+    (version "2.7.0.1")
     (source
      (origin
        (method git-fetch)
@@ -53,7 +53,7 @@ (define-public agda
              (commit (string-append "v" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "0n4avd58j45rdcmnwgrmz5s0ril0z4n2z711mwwbahl50f7359ky"))
+        (base32 "1dh9fi8lwjv9rk6zik2bwjgqln0f0d36m3hm9m3zmmk4fby4rsi2"))
        (patches (search-patches "agda-libdirs-env-variable.patch"
                                 "agda-use-sphinx-5.patch"))))
     (build-system haskell-build-system)
@@ -76,6 +76,7 @@ (define-public agda
            ghc-murmur-hash
            ghc-parallel
            ghc-peano
+           ghc-pqueue
            ghc-regex-tdfa
            ghc-split
            ghc-strict
-- 
2.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 2/5] gnu: agda-stdlib: Update to 2.1.13
Date: Sun, 22 Sep 2024 13:17:17 +0200

From: Josselin Poiret <dev <at> jpoiret.xyz>

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

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

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 0e38d4e2d8..8df3354243 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -200,7 +200,7 @@ (define-public agda-ial
 (define-public agda-stdlib
   (package
     (name "agda-stdlib")
-    (version "1.7.3")
+    (version "2.1.1")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -209,11 +209,11 @@ (define-public agda-stdlib
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0y6rns64rrkh8hw7mamcf6797329pi4ravpak5zijpnkzdagmlmy"))))
+                "1n742qvlxaj4dprnknvzrr876af6yjfwa4ps1dr4v1h814sg0xz0"))))
     (build-system agda-build-system)
     (arguments
      (list
-      #:plan '(("^\\./README.agda$" "-i."))
+      #:plan '(("^\\./doc/README.agda$" "-idoc/"))
       #:gnu-and-haskell? #t
       #:phases
       #~(modify-phases %standard-phases
@@ -221,7 +221,8 @@ (define-public agda-stdlib
             (lambda* (#:key inputs native-inputs #:allow-other-keys)
               (invoke
                (search-input-file (or native-inputs inputs) "/bin/runhaskell")
-               "GenerateEverything.hs"))))))
+               "GenerateEverything.hs"
+               "--out-dir" "doc/"))))))
     (native-inputs (list ghc-filemanip))
     (synopsis "The Agda Standard Library")
     (description
-- 
2.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 3/5] gnu: agda-categories: Update to 0.2.0.
Date: Sun, 22 Sep 2024 13:17:18 +0200

From: Josselin Poiret <dev <at> jpoiret.xyz>

* gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch ->
gnu/packages/patches/agda-categories-use-newer-stdlib.patch: Adapt patch.
* gnu/local.mk (dist_patch_DATA): Change registered name to new name.
* gnu/packages/agda.scm (agda-categories): Update to 0.2.0.  Use new patch
name.

Change-Id: Id5d1e335fe22c2d5809116083ed72e7b9208d69e
---
 gnu/local.mk                                  |  2 +-
 gnu/packages/agda.scm                         |  6 ++--
 .../agda-categories-use-newer-stdlib.patch    | 21 ++++++++++++++
 .../agda-categories-use-stdlib-1.7.3.patch    | 28 -------------------
 4 files changed, 25 insertions(+), 32 deletions(-)
 create mode 100644 gnu/packages/patches/agda-categories-use-newer-stdlib.patch
 delete mode 100644 gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index 8e7abc8a47..7d36746b88 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -939,7 +939,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-categories-use-newer-stdlib.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 8df3354243..d6a24c8be3 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -237,7 +237,7 @@ (define-public agda-stdlib
 (define-public agda-categories
   (package
     (name "agda-categories")
-    (version "0.1.7.2")
+    (version "0.2.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -246,10 +246,10 @@ (define-public agda-categories
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0xwgm2mfl2pxipsv31bin8p14y1yhd9n27lv3clvsxd4z9yc034m"))
+                "0a9mz9zyifkm03ss00iixa7b844m3gyvsx92al410hqj6v3r02qr"))
               (patches (search-patches "agda-categories-remove-incompatible-flags.patch"
                                        "agda-categories-use-find.patch"
-                                       "agda-categories-use-stdlib-1.7.3.patch"))))
+                                       "agda-categories-use-newer-stdlib.patch"))))
     (build-system agda-build-system)
     (arguments
      (list
diff --git a/gnu/packages/patches/agda-categories-use-newer-stdlib.patch b/gnu/packages/patches/agda-categories-use-newer-stdlib.patch
new file mode 100644
index 0000000000..00917853ba
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-use-newer-stdlib.patch
@@ -0,0 +1,21 @@
+Use newer stdlib.
+
+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,4 +1,4 @@
+ name: agda-categories
+-depend: standard-library-2.0
++depend: standard-library
+ include: src/
+
+-- 
+2.41.0
+
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
deleted file mode 100644
index 32680b99d7..0000000000
--- a/gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch
+++ /dev/null
@@ -1,28 +0,0 @@
-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.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 4/5] gnu: agda-cubical: Update to 0.7.
Date: Sun, 22 Sep 2024 13:17:19 +0200

From: Josselin Poiret <dev <at> jpoiret.xyz>

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

Change-Id: I7a0b3e711974c4d93eea6a753054803acc7e5c30
---
 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 d6a24c8be3..f388b4d669 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -269,7 +269,7 @@ (define-public agda-categories
 (define-public agda-cubical
   (package
     (name "agda-cubical")
-    (version "0.6")
+    (version "0.7")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -278,7 +278,7 @@ (define-public agda-cubical
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0zq0z328zcjmm43mrv2ks27i1dnbylcf8mhzja2hd4gvz1kq1ays"))))
+                "1c6axx3xx9ga7pl5294xqwklgbw96irxj0n74a1bxafhcx2lmfm0"))))
     (build-system agda-build-system)
     (arguments
      (list
-- 
2.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [PATCH 5/5] gnu: agda-1lab: Update to
 afcf848d367f906d6d07d1612fbd41d7dd8c978e.
Date: Sun, 22 Sep 2024 13:17:20 +0200

From: Josselin Poiret <dev <at> jpoiret.xyz>

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

Change-Id: I0c0b5273c13152e079f9e62daffc5c051d62ca63
---
 gnu/packages/agda.scm | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index f388b4d669..c20549888d 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -297,8 +297,8 @@ (define-public agda-cubical
 (define-public agda-1lab
   ;; Upstream doesn't do releases (yet).  Use a commit that builds with 2.6.4,
   ;; since they use Agda HEAD.
-  (let* ((revision "2")
-         (commit "549fdb1c948a975e90e70f871993a4a4239aa280"))
+  (let* ((revision "3")
+         (commit "afcf848d367f906d6d07d1612fbd41d7dd8c978e"))
     (package
       (name "agda-1lab")
       (version (git-version "0.0" revision commit))
@@ -311,7 +311,7 @@ (define-public agda-1lab
          (file-name (git-file-name name version))
          (sha256
           (base32
-           "1k4zj8dibyplakpxaw4a8hpsaqhakynjb83dqxrva4h4ssj6gkqj"))))
+           "12ax3n9111dkzm7nm3kwnvgslzsybyh740vml7l089in89f979wn"))))
       (build-system agda-build-system)
       (arguments
        ;; Check files individually first, to avoid running out of heap :(
-- 
2.46.0

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

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 73421-done <at> debbugs.gnu.org
Subject: Re: [PATCH 0/5] Update Agda to 2.7.0.1 along with libraries.
Date: Sat, 12 Oct 2024 11:56:30 +0200

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

Merged as bea5e1e2392a2557c8f01f6fdfffb936af891557.

Josselin Poiret <dev <at> jpoiret.xyz> writes:

> This patch series updates Agda and libraries to the latest upstream versions.
>
> Josselin Poiret (5):
>   gnu: agda: Update to 2.7.0.1.
>   gnu: agda-stdlib: Update to 2.1.13
>   gnu: agda-categories: Update to 0.2.0.
>   gnu: agda-cubical: Update to 0.7.
>   gnu: agda-1lab: Update to afcf848d367f906d6d07d1612fbd41d7dd8c978e.
>
>  gnu/local.mk                                  |  2 +-
>  gnu/packages/agda.scm                         | 30 ++++++++++---------
>  .../agda-categories-use-newer-stdlib.patch    | 21 +++++++++++++
>  .../agda-categories-use-stdlib-1.7.3.patch    | 28 -----------------
>  4 files changed, 38 insertions(+), 43 deletions(-)
>  create mode 100644 gnu/packages/patches/agda-categories-use-newer-stdlib.patch
>  delete mode 100644 gnu/packages/patches/agda-categories-use-stdlib-1.7.3.patch
>
>
> base-commit: b7c94d528875415ea7ec6225d88a6b3d55fa2e14
> -- 
> 2.46.0
>

-- 
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.