pyrox.dev
1{stdenv, fetchurl, coq}:
2
3stdenv.mkDerivation rec {
4
5 name = "coq-fiat-${coq.coq-version}-${version}";
6 version = "20141031";
7
8 src = fetchurl {
9 url = "http://plv.csail.mit.edu/fiat/releases/fiat-${version}.tar.gz";
10 sha256 = "0c5jrcgbpdj0gfzg2q4naqw7frf0xxs1f451fnic6airvpaj0d55";
11 };
12
13 buildInputs = [ coq.ocaml coq.camlp5 ];
14 propagatedBuildInputs = [ coq ];
15
16 enableParallelBuilding = false;
17 doCheck = !stdenv.isi686;
18
19 unpackPhase = ''
20 mkdir fiat
21 cd fiat
22 tar xvzf ${src}
23 '';
24
25 buildPhase = "make -j$NIX_BUILD_CORES sources";
26 checkPhase = "make -j$NIX_BUILD_CORES examples";
27
28 installPhase = ''
29 COQLIB=$out/lib/coq/${coq.coq-version}/
30 mkdir -p $COQLIB/user-contrib/Fiat
31 cp -pR src/* $COQLIB/user-contrib/Fiat
32 '';
33
34 meta = with stdenv.lib; {
35 homepage = http://plv.csail.mit.edu/fiat/;
36 description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
37 maintainers = with maintainers; [ jwiegley ];
38 platforms = coq.meta.platforms;
39 };
40
41}