From 8c9c19b5a9a46c6a042e6a48f34bdcf65c07cd51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Na=C3=AFm=20Favier?= <n@monade.li>
Date: Sun, 6 Aug 2023 12:27:44 +0200
Subject: [PATCH] agdaPackages._1lab: init at unstable-2023-03-07

https://github.com/plt-amy/1lab
---
 .../libraries/agda/1lab/default.nix           | 32 +++++++++++++++++++
 pkgs/top-level/agda-packages.nix              |  2 ++
 2 files changed, 34 insertions(+)
 create mode 100644 pkgs/development/libraries/agda/1lab/default.nix

diff --git a/pkgs/development/libraries/agda/1lab/default.nix b/pkgs/development/libraries/agda/1lab/default.nix
new file mode 100644
index 000000000000..81afbe4886cd
--- /dev/null
+++ b/pkgs/development/libraries/agda/1lab/default.nix
@@ -0,0 +1,32 @@
+{ lib, mkDerivation, fetchFromGitHub }:
+
+mkDerivation rec {
+  pname = "1lab";
+  version = "unstable-2023-03-07";
+
+  src = fetchFromGitHub {
+    owner = "plt-amy";
+    repo = pname;
+    # Last commit that compiles with Agda 2.6.3
+    rev = "c6ee57a2da327def241324b4775ec2c67cdab2af";
+    hash = "sha256-zDqFaDZxAdFxYM6l2zc7ZTi4XwMThw1AQwHfvhOxzdg=";
+  };
+
+  # We don't need anything in support; avoid installing LICENSE.agda
+  postPatch = ''
+    rm -rf support
+  '';
+
+  libraryName = "cubical-1lab";
+  libraryFile = "1lab.agda-lib";
+  everythingFile = "src/index.lagda.md";
+
+  meta = with lib; {
+    description =
+      "A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
+    homepage = src.meta.homepage;
+    license = licenses.agpl3;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ ncfavier ];
+  };
+}
diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix
index 948040deecbd..1e0e6e0a2d58 100644
--- a/pkgs/top-level/agda-packages.nix
+++ b/pkgs/top-level/agda-packages.nix
@@ -33,5 +33,7 @@ let
     generic = callPackage ../development/libraries/agda/generic { };
 
     agdarsec = callPackage ../development/libraries/agda/agdarsec { };
+
+    _1lab = callPackage ../development/libraries/agda/1lab { };
   };
 in mkAgdaPackages Agda