tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 callPackage,
5 coq,
6 flocq,
7 parseque,
8 mathcomp-boot,
9 compcert,
10 ExtLib,
11 version ? null,
12}:
13
14mkCoqDerivation {
15 pname = "wasm";
16 repo = "WasmCert-Coq";
17 owner = "WasmCert";
18
19 inherit version;
20 defaultVersion =
21 let
22 case = coq: mc: out: {
23 cases = [
24 coq
25 mc
26 ];
27 inherit out;
28 };
29 in
30 lib.switch
31 [ coq.coq-version mathcomp-boot.version ]
32 [
33 (case (lib.versions.range "8.20" "9.0") (lib.versions.isGe "2.4") "2.2.0")
34 ]
35 null;
36
37 release."2.1.0".sha256 = "sha256-k094mxDLLeelYP+ABm+dm6Y5YrachrbhNeZhfwLHNRo=";
38 release."2.2.0".sha256 = "sha256-GsfNpXgCG6XGqDE+bekzwZsWIHyjDTzWRuNnjCtS/88=";
39
40 mlPlugin = true;
41 useDune = true;
42
43 propagatedBuildInputs = [
44 ExtLib
45 mathcomp-boot
46 parseque
47 flocq
48 compcert
49 ];
50
51 buildInputs = [
52 coq.ocamlPackages.mdx
53 coq.ocamlPackages.linenoise
54 coq.ocamlPackages.wasm
55 ];
56
57 releaseRev = v: "v${v}";
58
59 passthru.tests.HelloWorld = callPackage ./test.nix { };
60
61 meta = {
62 description = "Wasm mechanisation in Coq/Rocq";
63 maintainers = with lib.maintainers; [ womeier ];
64 license = lib.licenses.mit;
65 };
66}