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

Previous Next

Package: guix-patches;

Reported by: Josselin Poiret <dev <at> jpoiret.xyz>

Date: Fri, 27 Oct 2023 18:13:01 UTC

Severity: normal

Tags: patch

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

Bug is archived. No further changes may be made.

Full log


View this message in rfc822 format

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: 66775 <at> debbugs.gnu.org
Cc: Josselin Poiret <dev <at> jpoiret.xyz>
Subject: [bug#66775] [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





This bug report was last modified 1 year and 189 days ago.

Previous Next


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