[bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab.

[Josselin Poiret]

From: Josselin Poiret <dev@jpoiret.xyz>

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

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index e75386c990..2116ceced3 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -298,3 +298,32 @@ (define-public agda-cubical
 agda-stdlib but using cubical methods.")
       (home-page "https://github.com/agda/cubical";)
       (license license:expat))))
+
+(define-public agda-1lab
+  ;; Upstream doesn't do releases (yet).  Use a commit that builds with 2.6.3,
+  ;; since they use Agda HEAD.
+  (let* ((revision "1")
+         (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6"))
+    (package
+      (name "agda-1lab")
+      (version (git-version "0.0" revision commit))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/plt-amy/1lab.git";)
+               (commit commit)))
+         (file-name (git-file-name name version))
+         (sha256
+          (base32
+           "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx"))))
+      (build-system agda-build-system)
+      (arguments
+       (list #:plan '(("src/index\\.lagda\\.md$"))))
+      (synopsis "Areference 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
+not a “linear” resource: Concepts are presented as a directed graph, with
+links indicating dependencies.")
+      (home-page "https://1lab.dev";)
+      (license license:agpl3))))
-- 
2.39.2