rocqPackages.rocqnavi: init at 0.5.0

This commit is contained in:
Cyril Cohen 2025-07-30 19:05:43 +02:00 committed by Pierre Roux
commit cbe7fae921
2 changed files with 48 additions and 0 deletions

View file

@ -0,0 +1,47 @@
{
lib,
mkRocqDerivation,
rocq-core,
version ? null,
}:
with lib;
mkRocqDerivation {
pname = "rocqnavi";
owner = "affeldt-aist";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with versions;
switch rocq-core.rocq-version [
(case (range "9.0" "9.2") "0.5.0")
] null;
release = {
"0.5.0".hash = "sha256-pmK4gD5ccerjr2UVgwGIVbjH/RiXdYQq79/XFetiHZg=";
};
releaseRev = v: "rocqnavi." + v;
nativeBuildInputs =
let
ocamlpkgs = rocq-core.ocamlPackages;
in
[
ocamlpkgs.yojson
ocamlpkgs.dune-glob
];
## Does the package contain OCaml code?
mlPlugin = true;
buildPhase = "make";
preInstallPhase = "mkdir $(out)/bin";
installFlags = [ "BINDIR=$(out)/bin" ];
meta = {
description = "Rocqnavi: an HTML documentation generator for Rocq prover";
maintainers = with maintainers; [ cohencyril ];
license = licenses.gpl2;
};
}

View file

@ -62,6 +62,7 @@ let
parseque = callPackage ../development/rocq-modules/parseque { };
relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
rocqnavi = callPackage ../development/rocq-modules/rocqnavi { };
stdlib = callPackage ../development/rocq-modules/stdlib { };
stdpp = callPackage ../development/rocq-modules/stdpp { };
vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };