1{stdenv, fetchurl, coq}:
2
3stdenv.mkDerivation rec {
4
5 name = "coq-bedrock-${coq.coq-version}-${version}";
6 version = "20140722";
7
8 src = fetchurl {
9 url = "http://plv.csail.mit.edu/bedrock/bedrock-${version}.tgz";
10 sha256 = "0aaa98q42rsy9hpsxji21bqznizfvf6fplsw6jq42h06j0049k80";
11 };
12
13 buildInputs = [ coq.ocaml coq.camlp5 ];
14 propagatedBuildInputs = [ coq ];
15
16 enableParallelBuilding = true;
17
18 buildPhase = ''
19 make -j$NIX_BUILD_CORES -C src/reification
20 make -j$NIX_BUILD_CORES -C src
21 make -j$NIX_BUILD_CORES -C src native
22 # make -j$NIX_BUILD_CORES -C platform
23 # make -j$NIX_BUILD_CORES -C platform -f Makefile.cito
24 '';
25
26 installPhase = ''
27 COQLIB=$out/lib/coq/${coq.coq-version}/
28 mkdir -p $COQLIB/user-contrib/Bedrock
29 cp -pR src/* $COQLIB/user-contrib/Bedrock
30 '';
31
32 meta = with stdenv.lib; {
33 homepage = http://plv.csail.mit.edu/bedrock/;
34 description = "A library that turns Coq into a tool much like classical verification systems";
35 maintainers = with maintainers; [ jwiegley ];
36 platforms = coq.meta.platforms;
37 };
38
39}