From 067e75e17a7f2c278eb6273824e33454d8e00566 Mon Sep 17 00:00:00 2001
From: Josselin Poiret <dev@jpoiret.xyz>
Date: Sun, 30 Apr 2023 12:12:33 +0200
Subject: [PATCH] gnu: Add agda-1lab.

* 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 240a51de1a..bd7fe29f1e 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -295,3 +295,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 "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
+not a “linear” resource: Concepts are presented as a directed graph, with
+links indicating dependencies.")
+      (home-page "https://1lab.dev")
+      (license license:agpl3))))