tjh.dev
1{
2 lib,
3 mkRocqDerivation,
4 which,
5 rocq-core,
6 version ? null,
7 elpi-version ? null,
8}:
9
10let
11 default-elpi-version =
12 if elpi-version != null then
13 elpi-version
14 else
15 let
16 case = case: out: { inherit case out; };
17 in
18 with lib.versions;
19 lib.switch rocq-core.rocq-version [
20 (case (range "9.0" "9.1") "2.0.7")
21 ] { };
22 elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
23 propagatedBuildInputs_wo_elpi = [
24 rocq-core.ocamlPackages.findlib
25 rocq-core.ocamlPackages.ppx_optcomp
26 ];
27 derivation = mkRocqDerivation {
28 pname = "elpi";
29 repo = "coq-elpi";
30 owner = "LPCIC";
31 inherit version;
32 defaultVersion =
33 let
34 case = case: out: { inherit case out; };
35 in
36 with lib.versions;
37 lib.switch rocq-core.rocq-version [
38 (case (range "9.0" "9.1") "2.6.0")
39 (case ("9.0") "2.5.2")
40 ] null;
41 release."2.6.0".sha256 = "sha256-23BHq1NFUkI3ayXnGUwiGFySLyY3EuH4RyMgAhQqI4g=";
42 release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
43 releaseRev = v: "v${v}";
44
45 mlPlugin = true;
46 useDune = true;
47
48 propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ];
49
50 configurePhase = ''
51 patchShebangs etc/with-rocq-wrap.sh
52 make dune-files || true
53 '';
54
55 buildPhase = ''
56 etc/with-rocq-wrap.sh dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
57 '';
58
59 installPhase = ''
60 etc/with-rocq-wrap.sh dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
61 mkdir $out/lib/coq/
62 mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}
63 '';
64
65 meta = {
66 description = "Rocq plugin embedding ELPI";
67 maintainers = [ lib.maintainers.cohencyril ];
68 license = lib.licenses.lgpl21Plus;
69 };
70 };
71 patched-derivation1 = derivation.overrideAttrs (
72 o:
73 lib.optionalAttrs (o ? elpi-version) {
74 propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [
75 (rocq-core.ocamlPackages.elpi.override { version = o.elpi-version; })
76 ];
77 }
78 );
79in
80patched-derivation1