pkgs/applications/science/logic/coq/8.3rc1.nix

   1 # TODO:
   2 # - coqide compilation should be optional or (better) separate;
   3 # - coqide libraries are not installed;
   4
   5 {stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
   6
   7 stdenv.mkDerivation {
   8   name = "coq8.3-8.3pre1";
   9
  10   src = fetchurl {
  11     url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
  12     sha256 = "0r43dqr7nzjfkxlz4963sj18gvjni6x3lhrlgh4l8k0cjspi62sj";
  13   };
  14
  15   buildInputs = [ ocaml camlp5 ncurses lablgtk ];
  16
  17   patches = [ ./coq-8.3-rc1_configure.patch ];
  18
  19   postPatch = ''
  20     substituteInPlace scripts/coqmktop.ml --replace \
  21       "\"-I\"; \"+lablgtk2\"" \
  22       "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
  23   '';
  24
  25   prefixKey = "-prefix ";
  26
  27   preConfigure = ''
  28     ARCH=`uname -s`
  29     CAMLDIR=`type -p ocamlc`
  30   '';
  31
  32   configureFlags =
  33     "-arch $ARCH " +
  34     "-camldir $CAMLDIR " +
  35     "-camldir ${ocaml}/bin " +
  36     "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
  37     "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
  38     "-opt -coqide opt";
  39
  40   buildFlags = "world"; # Debug with "world VERBOSE=1";
  41
  42   meta = {
  43     description = "Coq proof assistant";
  44     longDescription = ''
  45       Coq is a formal proof management system.  It provides a formal language
  46       to write mathematical definitions, executable algorithms and theorems
  47       together with an environment for semi-interactive development of
  48       machine-checked proofs.
  49     '';
  50     homepage = "http://coq.inria.fr";
  51     license = "LGPL";
  52   };
  53 }