From 602677cb48ff444cbd799cf6dd9b687fe3670620 Mon Sep 17 00:00:00 2001
From: thelissimus <thelissimus@tuta.io>
Date: Sun, 15 Dec 2024 15:32:30 +0500
Subject: [PATCH] cubical-mini: init at nightly-20241214

---
 .../libraries/agda/cubical-mini/default.nix   | 43 +++++++++++++++++++
 pkgs/top-level/agda-packages.nix              |  2 +
 2 files changed, 45 insertions(+)
 create mode 100644 pkgs/development/libraries/agda/cubical-mini/default.nix

diff --git a/pkgs/development/libraries/agda/cubical-mini/default.nix b/pkgs/development/libraries/agda/cubical-mini/default.nix
new file mode 100644
index 000000000000..385d99b96ada
--- /dev/null
+++ b/pkgs/development/libraries/agda/cubical-mini/default.nix
@@ -0,0 +1,43 @@
+{
+  lib,
+  mkDerivation,
+  fetchFromGitHub,
+  ghc,
+  cabal-install,
+}:
+
+mkDerivation rec {
+  pname = "cubical-mini";
+  version = "nightly-20241214";
+
+  src = fetchFromGitHub {
+    repo = pname;
+    owner = "cmcmA20";
+    rev = "ab18320018ddc0055db60d4bb5560d31909c5b78";
+    hash = "sha256-32qXY9KbProdPwqHxSkwO74Oqx65rTzoXtH2SpRB3OM=";
+  };
+
+  nativeBuildInputs = [
+    ghc
+    cabal-install
+  ];
+
+  # Makefile uses `cabal run` which tries to write its default config to $HOME and download package
+  # lists. We need to create an empty config file to make cabal work offline.
+  buildPhase = ''
+    runHook preBuild
+    export HOME=$TMP
+    mkdir $HOME/.cabal
+    touch $HOME/.cabal/config
+    make
+    runHook postBuild
+  '';
+
+  meta = {
+    homepage = "https://github.com/cmcmA20/cubical-mini";
+    description = "A nonstandard library for Cubical Agda";
+    license = lib.licenses.agpl3Only;
+    platforms = lib.platforms.unix;
+    maintainers = with lib.maintainers; [ thelissimus ];
+  };
+}
diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix
index c3b055dd3785..a943c2c52cfd 100644
--- a/pkgs/top-level/agda-packages.nix
+++ b/pkgs/top-level/agda-packages.nix
@@ -40,6 +40,8 @@ let
 
       cubical = callPackage ../development/libraries/agda/cubical { };
 
+      cubical-mini = callPackage ../development/libraries/agda/cubical-mini { };
+
       functional-linear-algebra = callPackage ../development/libraries/agda/functional-linear-algebra { };
 
       generic = callPackage ../development/libraries/agda/generic { };