From cc09ca4e4b97bfe268acf3cba3b731143a358d24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Jul 2026 14:53:12 +0200 Subject: [PATCH] rocqPackages.relation-algebra: merge with coqPackages.relation-algebra --- .../coq-modules/relation-algebra/default.nix | 61 ------------------- .../rocq-modules/relation-algebra/default.nix | 46 +++++++++++--- pkgs/top-level/coq-packages.nix | 2 +- 3 files changed, 37 insertions(+), 72 deletions(-) delete mode 100644 pkgs/development/coq-modules/relation-algebra/default.nix diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix deleted file mode 100644 index 3b3635d3ad36..000000000000 --- a/pkgs/development/coq-modules/relation-algebra/default.nix +++ /dev/null @@ -1,61 +0,0 @@ -{ - lib, - mkCoqDerivation, - coq, - aac-tactics, - mathcomp-boot, - version ? null, -}: - -mkCoqDerivation { - pname = "relation-algebra"; - owner = "damien-pous"; - - releaseRev = v: if lib.versions.range "1.7.6" "1.7.9" v then "v.${v}" else "v${v}"; - - release."1.7.11".hash = "sha256-ZOV0lUdduSabW9Qsz70clkO7QK/NK2STaHqBWcXb7nI="; - release."1.7.10".hash = "sha256-h738L+dybhmWZwTSLJrhv+sB+cIbj0+62Zcy9BH5sVo="; - release."1.7.9".hash = "sha256-1WzAZyj6q7s0u/9r7lahzxTl8612EA540l9wpm7TYEg="; - release."1.7.8".hash = "sha256-RITFd3G5TjY+rFzW073Ao1AGU+u6OGQyQeGHVodAXnA="; - release."1.7.7".hash = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2"; - release."1.7.6".hash = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w"; - release."1.7.5".hash = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU="; - release."1.7.4".hash = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM="; - release."1.7.3".hash = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos="; - release."1.7.2".hash = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o="; - release."1.7.1".hash = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA="; - - inherit version; - defaultVersion = - let - case = case: out: { inherit case out; }; - in - with lib.versions; - lib.switch coq.coq-version [ - (case (isEq "8.20") "1.7.11") - (case (range "8.18" "8.19") "1.7.10") - (case (isEq "8.17") "1.7.9") - (case (isEq "8.16") "1.7.8") - (case (isEq "8.15") "1.7.7") - (case (isEq "8.14") "1.7.6") - (case (isEq "8.13") "1.7.5") - (case (isEq "8.12") "1.7.4") - (case (isEq "8.11") "1.7.3") - (case (isEq "8.10") "1.7.2") - (case (isEq "8.9") "1.7.1") - ] null; - - mlPlugin = true; - - propagatedBuildInputs = [ - aac-tactics - mathcomp-boot - ]; - - meta = { - description = "Relation algebra library for Coq"; - maintainers = with lib.maintainers; [ siraben ]; - license = lib.licenses.gpl3Plus; - platforms = lib.platforms.unix; - }; -} diff --git a/pkgs/development/rocq-modules/relation-algebra/default.nix b/pkgs/development/rocq-modules/relation-algebra/default.nix index 73a712681bcf..189adb0b0116 100644 --- a/pkgs/development/rocq-modules/relation-algebra/default.nix +++ b/pkgs/development/rocq-modules/relation-algebra/default.nix @@ -3,6 +3,8 @@ mkRocqDerivation, rocq-core, stdlib, + aac-tactics, + mathcomp-boot, version ? null, }: @@ -12,21 +14,43 @@ mkRocqDerivation { inherit version; defaultVersion = - lib.switch - [ rocq-core.rocq-version ] - [ - { - cases = [ (lib.versions.range "9.0" "9.1") ]; - out = "1.8.0"; - } - ] - null; + let + case = case: out: { inherit case out; }; + in + with lib.versions; + lib.switch rocq-core.rocq-version [ + (case (range "9.0" "9.1") "1.8.0") + (case (isEq "8.20") "1.7.11") + (case (range "8.18" "8.19") "1.7.10") + (case (isEq "8.17") "1.7.9") + (case (isEq "8.16") "1.7.8") + (case (isEq "8.15") "1.7.7") + (case (isEq "8.14") "1.7.6") + (case (isEq "8.13") "1.7.5") + (case (isEq "8.12") "1.7.4") + (case (isEq "8.11") "1.7.3") + (case (isEq "8.10") "1.7.2") + (case (isEq "8.9") "1.7.1") + ] null; - releaseRev = v: "v${v}"; + releaseRev = v: if lib.versions.range "1.7.6" "1.7.9" v then "v.${v}" else "v${v}"; release."1.8.0".sha256 = "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0="; + release."1.7.11".hash = "sha256-ZOV0lUdduSabW9Qsz70clkO7QK/NK2STaHqBWcXb7nI="; + release."1.7.10".hash = "sha256-h738L+dybhmWZwTSLJrhv+sB+cIbj0+62Zcy9BH5sVo="; + release."1.7.9".hash = "sha256-1WzAZyj6q7s0u/9r7lahzxTl8612EA540l9wpm7TYEg="; + release."1.7.8".hash = "sha256-RITFd3G5TjY+rFzW073Ao1AGU+u6OGQyQeGHVodAXnA="; + release."1.7.7".hash = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2"; + release."1.7.6".hash = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w"; + release."1.7.5".hash = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU="; + release."1.7.4".hash = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM="; + release."1.7.3".hash = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos="; + release."1.7.2".hash = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o="; + release."1.7.1".hash = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA="; propagatedBuildInputs = [ + aac-tactics + mathcomp-boot stdlib ]; @@ -34,6 +58,8 @@ mkRocqDerivation { mlPlugin = true; + useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.7.11" v; + meta = { description = "Relation algebra library for Rocq"; maintainers = with lib.maintainers; [ siraben ]; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index c87842d8c4ff..c2b915f0e33c 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -219,7 +219,7 @@ let pocklington = callPackage ../development/coq-modules/pocklington { }; QuickChick = callPackage ../development/coq-modules/QuickChick { }; reglang = callPackage ../development/coq-modules/reglang { }; - relation-algebra = callPackage ../development/coq-modules/relation-algebra { }; + relation-algebra = callPackage ../development/rocq-modules/relation-algebra { }; rewriter = callPackage ../development/coq-modules/rewriter { }; RustExtraction = callPackage ../development/coq-modules/RustExtraction { }; semantics = callPackage ../development/coq-modules/semantics { };