rocqPackages.hierarchy-builder: init at 1.9.1

pkgs/development/coq-modules/hierarchy-builder/default.nix

@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
+  rocqPackages,
   stdlib,
   coq-elpi,
   version ? null,
@@ -96,4 +97,20 @@ hb.overrideAttrs (
   // lib.optionalAttrs (o.version != null && o.version == "1.8.1") {
     propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
   }
+  # this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0
+  //
+    lib.optionalAttrs
+      (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))
+      {
+        configurePhase = ''
+          echo no configuration
+        '';
+        buildPhase = ''
+          echo building nothing
+        '';
+        installPhase = ''
+          echo installing nothing
+        '';
+        propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocqPackages.hierarchy-builder ];
+      }
 )

pkgs/development/rocq-modules/hierarchy-builder/default.nix

@@ -0,0 +1,40 @@
+{
+  lib,
+  mkRocqDerivation,
+  rocq-core,
+  rocq-elpi,
+  version ? null,
+}:
+
+let
+  hb = mkRocqDerivation {
+    pname = "hierarchy-builder";
+    owner = "math-comp";
+    inherit version;
+    defaultVersion =
+      with lib.versions;
+      lib.switch rocq-core.rocq-version [
+        {
+          case = range "9.0" "9.0";
+          out = "1.9.1";
+        }
+      ] null;
+    release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
+    releaseRev = v: "v${v}";
+
+    propagatedBuildInputs = [ rocq-elpi ];
+
+    meta = with lib; {
+      description = "High level commands to declare a hierarchy based on packed classes";
+      maintainers = with maintainers; [
+        cohencyril
+        siraben
+      ];
+      license = licenses.mit;
+    };
+  };
+in
+hb.overrideAttrs (
+  o:
+  lib.optionalAttrs (o.version == "1.9.1") { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
+)

pkgs/top-level/rocq-packages.nix

@@ -37,6 +37,7 @@ let
       mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
 
       bignums = callPackage ../development/rocq-modules/bignums { };
+      hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
       stdlib = callPackage ../development/rocq-modules/stdlib { };