102 lines
1.8 KiB
Nix
102 lines
1.8 KiB
Nix
{
|
|
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".hash = "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;
|
|
};
|
|
}
|