nathan/nixpkgs
1
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2026-08-25 17:55:21 +00:00
Code Issues Packages Projects Releases Wiki Activity

rocqPackages.relation-algebra: merge with coqPackages.relation-algebra

Browse Source
This commit is contained in:
Pierre Roux
2026-07-23 14:53:12 +02:00
committed by Vincent Laporte
parent 11b5a8d235
commit cc09ca4e4b
3 changed files with 37 additions and 72 deletions
Download Patch File Download Diff File Expand all files Collapse all files

61
pkgs/development/coq-modules/relation-algebra/default.nix
View File

@@ -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;
};
}

46
pkgs/development/rocq-modules/relation-algebra/default.nix
View File

@@ -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 ];

2
pkgs/top-level/coq-packages.nix
View File

@@ -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 { };