GNU bug report logs - #61915
[PATCH 0/4] Update Agda to 2.6.3

Previous Next

Package: guix-patches;

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

Date: Thu, 2 Mar 2023 14:11:02 UTC

Severity: normal

Tags: patch

Merged with 61848

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: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org
Subject: [bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical.
Date: Sun, 30 Apr 2023 12:53:22 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>

* gnu/packages/agda.scm: New variable agda-cubical.
---
 gnu/packages/agda.scm | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 1068d8734f..e75386c990 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -265,3 +265,36 @@ (define-public agda-categories
       (description "A new Categories library for Agda")
       (home-page "https://github.com/agda/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.
+  (let* ((revision "1")
+         (commit "3dc3cd12579544c8c1c1d2c5f64fd8d577fd3d66"))
+    (package
+      (name "agda-cubical")
+      (version (git-version "0.4" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/agda/cubical.git")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "1b40adjgwrrdarzk0yiy2jmjgmf455ax6z70hfzdgc6j06vdb6mg"))))
+      (build-system agda-build-system)
+      (arguments
+       (list
+        #:gnu-and-haskell? #t
+        #:phases
+        #~(modify-phases %standard-phases
+            (replace 'build
+              (lambda _
+                (invoke "make"))))))
+      (synopsis "A standard library for Cubical Agda")
+      (description "A standard library for Cubical Agda, comparable to
+agda-stdlib but using cubical methods.")
+      (home-page "https://github.com/agda/cubical")
+      (license license:expat))))
-- 
2.39.2





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

Previous Next


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