tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
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") "3.4.2")
21 (case (range "9.0" "9.1") "2.0.7")
22 ] { };
23 elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
24 propagatedBuildInputs_wo_elpi = [
25 rocq-core.ocamlPackages.findlib
26 rocq-core.ocamlPackages.ppx_optcomp
27 ];
28 derivation = mkRocqDerivation {
29 pname = "elpi";
30 repo = "coq-elpi";
31 owner = "LPCIC";
32 inherit version;
33 defaultVersion =
34 let
35 case = case: out: { inherit case out; };
36 in
37 with lib.versions;
38 lib.switch rocq-core.rocq-version [
39 (case (range "9.0" "9.1") "3.2.0")
40 (case (range "9.0" "9.1") "2.6.0")
41 (case "9.0" "2.5.2")
42 ] null;
43 release."3.2.0".sha256 = "sha256-FyYG/8lEyt1L/paMez8jYAnnUE+sxIp4Da5MztmwJ/c=";
44 release."3.1.0".sha256 = "sha256-ytGPGwJv+jmRT6uN0sg6q+xh8ND0PMIZ9ULB0Uwca1w=";
45 release."3.0.0".sha256 = "sha256-YMe2is7duGcvAHjM4joUE90EloibjSxqfZThsJhstdU=";
46 release."2.6.0".sha256 = "sha256-23BHq1NFUkI3ayXnGUwiGFySLyY3EuH4RyMgAhQqI4g=";
47 release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
48 releaseRev = v: "v${v}";
49
50 mlPlugin = true;
51 useDune = true;
52
53 propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ];
54
55 configurePhase = ''
56 patchShebangs etc/with-rocq-wrap.sh
57 make dune-files || true
58 '';
59
60 buildPhase = ''
61 etc/with-rocq-wrap.sh dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
62 '';
63
64 installPhase = ''
65 etc/with-rocq-wrap.sh dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
66 mkdir $out/lib/coq/
67 mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}
68 '';
69
70 meta = {
71 description = "Rocq plugin embedding ELPI";
72 maintainers = [ lib.maintainers.cohencyril ];
73 license = lib.licenses.lgpl21Plus;
74 };
75 };
76 patched-derivation1 = derivation.overrideAttrs (
77 o:
78 lib.optionalAttrs (o ? elpi-version) {
79 propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [
80 (rocq-core.ocamlPackages.elpi.override { version = o.elpi-version; })
81 ];
82 }
83 );
84in
85patched-derivation1