tjh.dev
1{
2 callPackage,
3 fetchurl,
4 lib,
5 stdenv,
6 ocamlPackages,
7 coqPackages,
8 rubber,
9 hevea,
10 emacs,
11 version ? "1.8.1",
12 ideSupport ? true,
13 wrapGAppsHook3,
14}:
15
16stdenv.mkDerivation rec {
17 pname = "why3";
18 inherit version;
19
20 src = fetchurl {
21 url = "https://why3.gitlabpages.inria.fr/releases/${pname}-${version}.tar.gz";
22 hash =
23 {
24 "1.8.1" = "sha256-RSj89bP8ZBdTQM7x5cpJTsk55SIXlc2SXMQj6Q1GFW8=";
25 "1.7.2" = "sha256-VaSG/FiO2MDdSSFXGJJrIylQx0LPwtT8AF7TpPVZhCQ=";
26 "1.6.0" = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
27 }
28 ."${version}";
29 };
30
31 strictDeps = true;
32
33 nativeBuildInputs =
34 lib.optional ideSupport wrapGAppsHook3
35 ++ (with ocamlPackages; [
36 ocaml
37 findlib
38 menhir
39 ])
40 ++ [
41 # Coq Support
42 coqPackages.coq
43 ];
44
45 buildInputs =
46 with ocamlPackages;
47 [
48 ocamlgraph
49 zarith
50 # Emacs compilation of why3.el
51 emacs
52 # Documentation
53 rubber
54 hevea
55 ]
56 ++
57 lib.optional ideSupport
58 # GUI
59 lablgtk3-sourceview3
60 ++ [
61 # WebIDE
62 js_of_ocaml
63 js_of_ocaml-ppx
64 # S-expression output for why3pp
65 ppx_deriving
66 ppx_sexp_conv
67 ]
68 ++
69 # Coq Support
70 (with coqPackages; [
71 coq
72 flocq
73 ]);
74
75 propagatedBuildInputs = with ocamlPackages; [
76 camlzip
77 menhirLib
78 (if lib.versionAtLeast version "1.8.0" then zarith else num)
79 re
80 sexplib
81 ];
82
83 enableParallelBuilding = true;
84
85 configureFlags = [
86 "--enable-verbose-make"
87 (lib.enableFeature ideSupport "ide")
88 ];
89
90 outputs = [
91 "out"
92 "dev"
93 ];
94
95 installTargets = [
96 "install"
97 "install-lib"
98 ];
99
100 postInstall = ''
101 mkdir -p $dev/lib
102 mv $out/lib/ocaml $dev/lib/
103 '';
104
105 passthru.withProvers = callPackage ./with-provers.nix { };
106
107 meta = with lib; {
108 description = "Platform for deductive program verification";
109 homepage = "https://why3.lri.fr/";
110 license = licenses.lgpl21;
111 platforms = platforms.unix;
112 maintainers = with maintainers; [
113 thoughtpolice
114 vbgl
115 ];
116 };
117}