tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 stdlib,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "waterproof";
11 owner = "impermeable";
12 repo = "coq-waterproof";
13 inherit version;
14 defaultVersion =
15 let
16 inherit (lib.versions) range;
17 in
18 lib.switch coq.coq-version [
19 {
20 case = range "8.18" "8.18";
21 out = "2.1.1+8.18";
22 }
23 ] null;
24 release = {
25 "2.1.1+8.18".sha256 = "sha256-jYuQ9SPFRefNCUfn6+jEaJ4399EnU0gXPPkEDCpJYOI=";
26 };
27
28 propagatedBuildInputs = [ stdlib ];
29
30 mlPlugin = true;
31
32 useDune = true;
33
34 meta = {
35 description = "Coq proofs in a style that resembles non-mechanized mathematical proofs";
36 license = lib.licenses.lgpl3Plus;
37 };
38}