mirror of
https://github.com/NixOS/nixpkgs.git
synced 2026-09-01 05:04:40 +00:00
103 lines
2.1 KiB
Nix
103 lines
2.1 KiB
Nix
{
|
|
lib,
|
|
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}";
|
|
|
|
propagatedBuildInputs = [
|
|
wasmcert
|
|
compcert
|
|
ExtLib
|
|
metarocq-erasure-plugin
|
|
metarocq-safechecker-plugin
|
|
];
|
|
|
|
postPatch = ''
|
|
patchShebangs ./configure.sh
|
|
patchShebangs ./clean_extraction.sh
|
|
patchShebangs ./make_plugin.sh
|
|
|
|
# drop after https://github.com/CertiRocq/certirocq/pull/162
|
|
substituteInPlace runtime/Makefile \
|
|
--replace-fail "gcc -I /opt/homebrew/include" '$(CC)'
|
|
substituteInPlace clean_extraction.sh \
|
|
--replace-fail "mv aST.ml AST.ml" "mv aST.ml AST.ml.tmp && mv AST.ml.tmp AST.ml" \
|
|
--replace-fail "mv aST.mli AST.mli" "mv aST.mli AST.mli.tmp && mv AST.mli.tmp AST.mli"
|
|
'';
|
|
|
|
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;
|
|
};
|
|
}
|