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.hierarchy-builder: merge with coqPackages.hierarchy-builder

Browse Source
This commit is contained in:
Pierre Roux
2026-07-23 13:59:50 +02:00
committed by Vincent Laporte
parent 853cde0e77
commit 0f6109b799
3 changed files with 40 additions and 90 deletions
Download Patch File Download Diff File Expand all files Collapse all files

84
pkgs/development/coq-modules/hierarchy-builder/default.nix
View File

@@ -1,84 +0,0 @@
{
lib,
mkCoqDerivation,
coq,
stdlib,
coq-elpi,
version ? null,
}:
let
hb = mkCoqDerivation {
pname = "hierarchy-builder";
owner = "math-comp";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version [
(case (range "8.20" "8.20") "1.9.1")
(case (range "8.19" "8.20") "1.8.0")
(case (range "8.18" "8.20") "1.7.1")
(case (range "8.16" "8.18") "1.6.0")
(case (range "8.15" "8.18") "1.5.0")
(case (range "8.15" "8.17") "1.4.0")
(case (range "8.13" "8.14") "1.2.0")
(case (range "8.12" "8.13") "1.1.0")
(case (isEq "8.11") "0.10.0")
] null;
release."1.9.1".hash = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
release."1.8.1".hash = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
releaseRev = v: "v${v}";
propagatedBuildInputs = [ coq-elpi ];
mlPlugin = true;
meta = {
description = "High level commands to declare a hierarchy based on packed classes";
maintainers = with lib.maintainers; [
cohencyril
siraben
];
license = lib.licenses.mit;
};
};
hb2 = hb.overrideAttrs (
o:
lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
buildPhase = "make build";
}
// (
if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
else
{ installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
)
// lib.optionalAttrs (o.version != null && o.version == "1.8.1") {
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
}
);
in
# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0
if coq.rocqPackages ? hierarchy-builder then
coq.rocqPackages.hierarchy-builder.override {
inherit version;
inherit (coq.rocqPackages) rocq-core;
rocq-elpi = coq-elpi;
}
else
hb2

43
pkgs/development/rocq-modules/hierarchy-builder/default.nix
View File

@@ -20,16 +20,38 @@ let
(case (range "9.0" "9.3") "1.10.3")
(case (range "9.0" "9.1") "1.10.2")
(case (range "9.0" "9.1") "1.10.0")
(case (range "9.0" "9.1") "1.9.1")
(case (range "8.20" "9.1") "1.9.1")
(case (range "8.19" "8.20") "1.8.0")
(case (range "8.18" "8.20") "1.7.1")
(case (range "8.16" "8.18") "1.6.0")
(case (range "8.15" "8.18") "1.5.0")
(case (range "8.15" "8.17") "1.4.0")
(case (range "8.13" "8.14") "1.2.0")
(case (range "8.12" "8.13") "1.1.0")
(case (isEq "8.11") "0.10.0")
] null;
release."1.10.3".hash = "sha256-y13KxzLulIu39Ci3aMc1cZG4tw3LL2ab7U9snI6jrXc=";
release."1.10.2".sha256 = "sha256-Uzni9qrYQP45Tr+JkHs0BuRARwmWSMwA/iHhIzkolxc=";
release."1.10.0".sha256 = "sha256-c52nS8I0tia7Q8lZTFJyHVPVabW9xv55m7w6B7y3+e8=";
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
releaseRev = v: "v${v}";
propagatedBuildInputs = [ rocq-elpi ];
useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.9.1" v;
meta = {
description = "High level commands to declare a hierarchy based on packed classes";
maintainers = with lib.maintainers; [
@@ -39,8 +61,19 @@ let
license = lib.licenses.mit;
};
};
hb2 = hb.overrideAttrs (
o:
lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
buildPhase = "make build";
}
// (
if lib.versions.range "1.1.0" "1.9.1" o.version then
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
else if lib.versions.range "0.10.0" "1.1.0" o.version then
{ installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
else
{ }
)
);
in
hb.overrideAttrs (
o:
lib.optionalAttrs (o.version == "1.9.1") { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
)
hb2

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

@@ -99,6 +99,7 @@ let
ConCert = callPackage ../development/coq-modules/ConCert { };
coq-bits = callPackage ../development/coq-modules/coq-bits { };
coq-elpi = callPackage ../development/coq-modules/coq-elpi { };
rocq-elpi = callPackage ../development/coq-modules/coq-elpi { };
coq-hammer = callPackage ../development/coq-modules/coq-hammer { };
coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { };
CoqMatrix = callPackage ../development/coq-modules/coq-matrix { };
@@ -134,7 +135,7 @@ let
goedel = callPackage ../development/coq-modules/goedel { };
graph-theory = callPackage ../development/coq-modules/graph-theory { };
heq = callPackage ../development/coq-modules/heq { };
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder { };
hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
high-school-geometry = callPackage ../development/coq-modules/high-school-geometry { };
HoTT = callPackage ../development/coq-modules/HoTT { };
http = callPackage ../development/coq-modules/http { };