Author: maggesi
Date: Tue Sep 14 21:15:58 2010
New Revision: 23803
URL: https://svn.nixos.org/websvn/nix/?rev=23803&sc=1
Log:
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.
Added:
nixpkgs/trunk/pkgs/applications/science/logic/coq/8.3rc1.nix
nixpkgs/trunk/pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch
Modified:
nixpkgs/trunk/pkgs/top-level/all-packages.nix
Added: nixpkgs/trunk/pkgs/applications/science/logic/coq/8.3rc1.nix
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/coq/8.3rc1.nix Tue Sep
14 21:15:58 2010 (r23803)
@@ -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";
+ };
+}
Added:
nixpkgs/trunk/pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++
nixpkgs/trunk/pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch
Tue Sep 14 21:15:58 2010 (r23803)
@@ -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
Modified: nixpkgs/trunk/pkgs/top-level/all-packages.nix
==============================================================================
--- nixpkgs/trunk/pkgs/top-level/all-packages.nix Tue Sep 14 16:39:42
2010 (r23802)
+++ nixpkgs/trunk/pkgs/top-level/all-packages.nix Tue Sep 14 21:15:58
2010 (r23803)
@@ -6671,6 +6671,10 @@
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;
};
_______________________________________________
nix-commits mailing list
[email protected]
http://mail.cs.uu.nl/mailman/listinfo/nix-commits
