coqPackages.CertiRocq: init at 0.9.1 (#501154)

2026-03-19 07:02:44 +00:00
parent 1a25a9d4cd c20f11c48a
commit 65c3df51c2
2 changed files with 102 additions and 0 deletions
@@ -0,0 +1,101 @@
+{
+  lib,
+  pkgs,
+  pkg-config,
+  mkCoqDerivation,
+  coq,
+  wasmcert,
+  compcert,
+  metarocq-erasure-plugin,
+  metarocq-safechecker-plugin,
+  ExtLib,
+  version ? null,
+}:
+
+with lib;
+mkCoqDerivation {
+  pname = "CertiRocq";
+  owner = "CertiRocq";
+  repo = "certirocq";
+  opam-name = "rocq-certirocq";
+  mlPlugin = true;
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mr: out: {
+        cases = [
+          coq
+          mr
+        ];
+        inherit out;
+      };
+    in
+    lib.switch
+      [
+        coq.coq-version
+        metarocq-erasure-plugin.version
+      ]
+      [
+        (case "9.1" "1.5.1-9.1" "0.9.1+9.1")
+      ]
+      null;
+  release = {
+    "0.9.1+9.1".sha256 = "sha256-YsweBaoq8+QG63e7Llp/4bHldAFnSQSyMumJkb+Bsp0=";
+  };
+  releaseRev = v: "v${v}";
+
+  buildInputs = [
+    pkgs.clang
+  ];
+
+  propagatedBuildInputs = [
+    wasmcert
+    compcert
+    ExtLib
+    metarocq-erasure-plugin
+    metarocq-safechecker-plugin
+  ];
+
+  patchPhase = ''
+    patchShebangs ./configure.sh
+    patchShebangs ./clean_extraction.sh
+    patchShebangs ./make_plugin.sh
+  '';
+
+  configurePhase = ''
+    ./configure.sh local
+  '';
+
+  buildPhase = ''
+    runHook preBuild
+
+    make all
+    make plugins
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+
+    OUTDIR=$out/lib/coq/${coq.coq-version}/user-contrib
+
+    DST=$OUTDIR/CertiRocq/Plugin/runtime make -C runtime install
+    COQLIBINSTALL=$OUTDIR make -C theories install
+    COQLIBINSTALL=$OUTDIR make -C libraries install
+    COQLIBINSTALL=$OUTDIR COQPLUGININSTALL=$OCAMLFIND_DESTDIR make -C plugin install
+    COQLIBINSTALL=$OUTDIR COQPLUGININSTALL=$OCAMLFIND_DESTDIR make -C cplugin install
+
+    runHook postInstall
+  '';
+
+  meta = {
+    description = "CertiRocq";
+    maintainers = with maintainers; [
+      womeier
+      _4ever2
+    ];
+    license = licenses.mit;
+  };
+}
@@ -71,6 +71,7 @@ let
      category-theory = callPackage ../development/coq-modules/category-theory { };
      ceres = callPackage ../development/coq-modules/ceres { };
      ceres-bs = callPackage ../development/coq-modules/ceres-bs { };
+      CertiRocq = callPackage ../development/coq-modules/CertiRocq { };
      Cheerios = callPackage ../development/coq-modules/Cheerios { };
      coinduction = callPackage ../development/coq-modules/coinduction { };
      CoLoR = callPackage ../development/coq-modules/CoLoR (