tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 stdlib,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "paco";
11 owner = "snu-sf";
12 inherit version;
13 defaultVersion =
14 let
15 case = case: out: { inherit case out; };
16 in
17 with lib.versions;
18 lib.switch coq.coq-version [
19 (case (range "8.14" "9.1") "4.2.3")
20 (case (isEq "8.13") "4.2.2")
21 (case (range "8.12" "8.17") "4.1.2")
22 (case (range "8.9" "8.13") "4.1.1")
23 (case (range "8.6" "8.13") "4.0.2")
24 (case (isEq "8.5") "1.2.8")
25 ] null;
26 release."4.2.3".sha256 = "sha256-ldUjNd5daUu2B3v4tk20/iXFgyUuW4XHlbubTInpwcs=";
27 release."4.2.2".sha256 = "sha256-qr6o45Q90FK+kkBUJ+W7QhiA0YQRb1RUwwXUpTTFt8A=";
28 release."4.2.0".sha256 = "sha256-YHYtiz9hium96n3owL/C99AjJAFTlTCmmb2+ttevgMY=";
29 release."4.1.2".sha256 = "sha256:1l8mwakqp4wnppsldl8wp2j24h1jvadnvrsgf35xnvdyygypjp2v";
30 release."4.1.1".sha256 = "1qap8cyv649lr1s11r7h5jzdjd4hsna8kph15qy5fw24h5nx6byy";
31 release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
32 release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
33 releaseRev = v: "v${v}";
34
35 propagatedBuildInputs = [ stdlib ];
36
37 preBuild = "cd src";
38
39 installPhase = ''
40 COQLIB=$out/lib/coq/${coq.coq-version}/
41 mkdir -p $COQLIB/user-contrib/Paco
42 cp -pR *.vo $COQLIB/user-contrib/Paco
43 '';
44
45 meta = {
46 homepage = "https://plv.mpi-sws.org/paco/";
47 description = "Coq library implementing parameterized coinduction";
48 maintainers = with lib.maintainers; [
49 jwiegley
50 ptival
51 ];
52 };
53}