tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 stdlib,
6 coq-elpi,
7 version ? null,
8}:
9
10let
11 hb = mkCoqDerivation {
12 pname = "hierarchy-builder";
13 owner = "math-comp";
14 inherit version;
15 defaultVersion =
16 let
17 case = case: out: { inherit case out; };
18 in
19 with lib.versions;
20 lib.switch coq.coq-version [
21 (case (range "8.20" "8.20") "1.9.1")
22 (case (range "8.19" "8.20") "1.8.0")
23 (case (range "8.18" "8.20") "1.7.1")
24 (case (range "8.16" "8.18") "1.6.0")
25 (case (range "8.15" "8.18") "1.5.0")
26 (case (range "8.15" "8.17") "1.4.0")
27 (case (range "8.13" "8.14") "1.2.0")
28 (case (range "8.12" "8.13") "1.1.0")
29 (case (isEq "8.11") "0.10.0")
30 ] null;
31 release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
32 release."1.8.1".sha256 = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
33 release."1.8.0".sha256 = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
34 release."1.7.1".sha256 = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
35 release."1.7.0".sha256 = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
36 release."1.6.0".sha256 = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
37 release."1.5.0".sha256 = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
38 release."1.4.0".sha256 = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
39 release."1.3.0".sha256 = "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
40 release."1.2.1".sha256 = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
41 release."1.2.0".sha256 = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
42 release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
43 release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
44 release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
45 releaseRev = v: "v${v}";
46
47 propagatedBuildInputs = [ coq-elpi ];
48
49 mlPlugin = true;
50
51 meta = with lib; {
52 description = "High level commands to declare a hierarchy based on packed classes";
53 maintainers = with maintainers; [
54 cohencyril
55 siraben
56 ];
57 license = licenses.mit;
58 };
59 };
60 hb2 = hb.overrideAttrs (
61 o:
62 lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
63 buildPhase = "make build";
64 }
65 // (
66 if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then
67 { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
68 else
69 { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
70 )
71 // lib.optionalAttrs (o.version != null && o.version == "1.8.1") {
72 propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
73 }
74 );
75in
76# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0
77if coq.rocqPackages ? hierarchy-builder then
78 coq.rocqPackages.hierarchy-builder.override {
79 inherit version;
80 inherit (coq.rocqPackages) rocq-core;
81 rocq-elpi = coq-elpi;
82 }
83else
84 hb2