2 # - coqide compilation should be optional or (better) separate;
3 # - coqide libraries are not installed;
5 {stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
8 name = "coq8.3-8.3pre1";
11 url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
12 sha256 = "0r43dqr7nzjfkxlz4963sj18gvjni6x3lhrlgh4l8k0cjspi62sj";
15 buildInputs = [ ocaml camlp5 ncurses lablgtk ];
17 patches = [ ./coq-8.3-rc1_configure.patch ];
20 substituteInPlace scripts/coqmktop.ml --replace \
21 "\"-I\"; \"+lablgtk2\"" \
22 "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
25 prefixKey = "-prefix ";
29 CAMLDIR=`type -p ocamlc`
34 "-camldir $CAMLDIR " +
35 "-camldir ${ocaml}/bin " +
36 "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
37 "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
40 buildFlags = "world"; # Debug with "world VERBOSE=1";
43 description = "Coq proof assistant";
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.
50 homepage = "http://coq.inria.fr";