pkgs/development/coq-modules/fiat/HEAD.nix

   1 {
   2   lib,
   3   mkCoqDerivation,
   4   coq,
   5   python27,
   6   version ? null,
   7 }:
   8
   9 mkCoqDerivation rec {
  10   pname = "fiat";
  11   owner = "mit-plv";
  12   repo = "fiat";
  13   displayVersion = {
  14     fiat = v: "unstable-${v}";
  15   };
  16   inherit version;
  17   defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null;
  18   release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
  19   release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi";
  20
  21   mlPlugin = true;
  22   buildInputs = [ python27 ];
  23
  24   prePatch = "patchShebangs etc/coq-scripts";
  25
  26   doCheck = false;
  27
  28   enableParallelBuilding = false;
  29   buildPhase = "make -j$NIX_BUILD_CORES";
  30
  31   installPhase = ''
  32     COQLIB=$out/lib/coq/${coq.coq-version}/
  33     mkdir -p $COQLIB/user-contrib/Fiat
  34     cp -pR src/* $COQLIB/user-contrib/Fiat
  35   '';
  36
  37   meta = {
  38     homepage = "http://plv.csail.mit.edu/fiat/";
  39     description = "Library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
  40     maintainers = with lib.maintainers; [ jwiegley ];
  41   };
  42 }