From 28ced4eb9c9566c71d8f6a5e149e38801ca31e60 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Fri, 30 Jan 2026 15:34:29 +0100
Subject: [PATCH] rocqPackages.relation-algebra: init at 1.8.0

---
 .../rocq-modules/relation-algebra/default.nix | 43 +++++++++++++++++++
 pkgs/top-level/rocq-packages.nix              |  1 +
 2 files changed, 44 insertions(+)
 create mode 100644 pkgs/development/rocq-modules/relation-algebra/default.nix

diff --git a/pkgs/development/rocq-modules/relation-algebra/default.nix b/pkgs/development/rocq-modules/relation-algebra/default.nix
new file mode 100644
index 000000000000..0bb2e1d289ad
--- /dev/null
+++ b/pkgs/development/rocq-modules/relation-algebra/default.nix
@@ -0,0 +1,43 @@
+{
+  lib,
+  mkRocqDerivation,
+  rocq-core,
+  stdlib,
+  version ? null,
+}:
+
+mkRocqDerivation {
+  pname = "relation-algebra";
+  owner = "damien-pous";
+
+  inherit version;
+  defaultVersion =
+    lib.switch
+      [ rocq-core.rocq-version ]
+      [
+        {
+          cases = [ (lib.versions.isEq "9.0") ];
+          out = "1.8.0";
+        }
+      ]
+      null;
+
+  releaseRev = v: "v${v}";
+
+  release."1.8.0".sha256 = "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0=";
+
+  propagatedBuildInputs = [
+    stdlib
+  ];
+
+  dontConfigure = true;
+
+  mlPlugin = true;
+
+  meta = {
+    description = "Relation algebra library for Rocq";
+    maintainers = with lib.maintainers; [ siraben ];
+    license = lib.licenses.gpl3Plus;
+    platforms = lib.platforms.unix;
+  };
+}
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 84f6f26bb8c4..ed0327ee96ec 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -46,6 +46,7 @@ let
       mathcomp-field = self.mathcomp.field;
       mathcomp-character = self.mathcomp.character;
       parseque = callPackage ../development/rocq-modules/parseque { };
+      relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
       stdlib = callPackage ../development/rocq-modules/stdlib { };
       vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };