coqPackages.wasmcert: init at 2.1.0

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
This commit is contained in:
Wolfgang Meier 2025-07-18 17:49:29 +02:00 committed by Vincent Laporte
parent 5fadf32bee
commit 0bed63d0d9
3 changed files with 98 additions and 0 deletions

View File

@ -0,0 +1,67 @@
{
lib,
mkCoqDerivation,
callPackage,
coq,
flocq,
parseque,
mathcomp-boot,
compcert,
ExtLib,
version ? null,
}:
with lib;
mkCoqDerivation {
pname = "wasm";
repo = "WasmCert-Coq";
owner = "WasmCert";
inherit version;
defaultVersion =
let
case = coq: mc: out: {
cases = [
coq
mc
];
inherit out;
};
in
with lib.versions;
lib.switch
[ coq.coq-version mathcomp-boot.version ]
[
(case (isEq "8.20") (isEq "2.4") "2.1.0")
]
null;
release."2.1.0".sha256 = "sha256-k094mxDLLeelYP+ABm+dm6Y5YrachrbhNeZhfwLHNRo=";
mlPlugin = true;
useDune = true;
propagatedBuildInputs = [
ExtLib
mathcomp-boot
parseque
flocq
compcert
];
buildInputs = [
coq.ocamlPackages.mdx
coq.ocamlPackages.linenoise
coq.ocamlPackages.wasm
];
releaseRev = v: "v${v}";
passthru.tests.HelloWorld = callPackage ./test.nix { };
meta = {
description = "Wasm mechanisation in Coq/Rocq";
maintainers = with maintainers; [ womeier ];
license = licenses.mit;
};
}

View File

@ -0,0 +1,30 @@
{
stdenv,
coq,
wasmcert,
}:
stdenv.mkDerivation {
pname = "wasmcert-interpreter-test";
inherit (wasmcert) src version;
nativeCheckInputs = [
wasmcert
coq
];
dontConfigure = true;
dontBuild = true;
doCheck = true;
checkPhase = ''
coqc .ci/import_test.v
wasm_coq_interpreter tests/add.wasm -r main
if [ $? -ne 0 ]; then
echo "Wasm_coq_interpreter failed to run hello world program"
exit 1
fi
'';
installPhase = "touch $out";
}

View File

@ -245,6 +245,7 @@ let
};
})
);
wasmcert = callPackage ../development/coq-modules/wasmcert { };
waterproof = callPackage ../development/coq-modules/waterproof { };
zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;