Add coq-8.3rc1

Note: In this version we introduce a new schema for the name of the coq
derivations where the coq version is included in the name (i.e.,
"coq8.3-8.3pre1" instead of "coq-8.3pre1").  The reason for this is that often
coq releases introduce several incompatibilities.  Thus I argue that, in
general, users do not want nix-env to upgrade automatically form one release to
another.  Also version string "8.3pre1" is used instead of "8.3-rc1" to trigger
the nix mechanism for versions comparison.


svn path=/nixpkgs/trunk/; revision=23803

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

@@ -0,0 +1,53 @@
+# TODO:
+# - coqide compilation should be optional or (better) separate;
+# - coqide libraries are not installed;
+
+{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
+
+stdenv.mkDerivation {
+  name = "coq8.3-8.3pre1";
+
+  src = fetchurl {
+    url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
+    sha256 = "0r43dqr7nzjfkxlz4963sj18gvjni6x3lhrlgh4l8k0cjspi62sj";
+  };
+
+  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
+
+  patches = [ ./coq-8.3-rc1_configure.patch ];
+
+  postPatch = ''
+    substituteInPlace scripts/coqmktop.ml --replace \
+      "\"-I\"; \"+lablgtk2\"" \
+      "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
+  '';
+
+  prefixKey = "-prefix ";
+
+  preConfigure = ''
+    ARCH=`uname -s`
+    CAMLDIR=`type -p ocamlc`
+  '';
+
+  configureFlags =
+    "-arch $ARCH " +
+    "-camldir $CAMLDIR " +
+    "-camldir ${ocaml}/bin " +
+    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
+    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
+    "-opt -coqide opt";
+
+  buildFlags = "world"; # Debug with "world VERBOSE=1";
+
+  meta = {
+    description = "Coq proof assistant";
+    longDescription = ''
+      Coq is a formal proof management system.  It provides a formal language
+      to write mathematical definitions, executable algorithms and theorems
+      together with an environment for semi-interactive development of
+      machine-checked proofs.
+    '';
+    homepage = "http://coq.inria.fr";
+    license = "LGPL";
+  };
+}

pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch

@@ -0,0 +1,20 @@
+diff -Nuar coq-8.3-rc1/configure coq-8.3-rc1.nixos/configure
+--- coq-8.3-rc1/configure	2010-08-06 10:36:16.000000000 +0200
++++ coq-8.3-rc1.nixos/configure	2010-09-14 20:30:02.000000000 +0200
+@@ -399,7 +399,6 @@
+ 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
+ 	 ocamlmktopexec=$CAMLBIN/ocamlmktop
+ 	 ocamlmklibexec=$CAMLBIN/ocamlmklib
+-	 camlp4oexec=$CAMLBIN/camlp4o
+ esac
+ 
+ if test ! -f "$CAMLC" ; then
+@@ -647,7 +646,7 @@
+             no)  LABLGTKLIB=+lablgtk2                   # Pour le message
+                  LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
+             yes) LABLGTKLIB="$lablgtkdir"               # Pour le message
+-                 LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
++                 LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
+         esac;;
+     no) LABLGTKINCLUDES="";;
+ esac

pkgs/top-level/all-packages.nix

@@ -6671,6 +6671,10 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  coq8_3 = callPackage ../applications/science/logic/coq/8.3rc1.nix {
+    camlp5 = camlp5_transitional;
+  };
+
   coq_beta = callPackage ../applications/science/logic/coq/beta.nix {
     camlp5 = camlp5_transitional;
   };