From afbb01c90d4a10191bc68b68e2d484283eea329c Mon Sep 17 00:00:00 2001 From: Marco Maggesi Date: Tue, 11 May 2010 20:14:46 +0000 Subject: [PATCH] Add expression for Coq 8.3 beta svn path=/nixpkgs/trunk/; revision=21734 --- pkgs/applications/science/logic/coq/beta.nix | 53 +++++++++++++++++++ .../science/logic/coq/coq-8.3-beta0-1.patch | 20 +++++++ pkgs/top-level/all-packages.nix | 5 ++ 3 files changed, 78 insertions(+) create mode 100644 pkgs/applications/science/logic/coq/beta.nix create mode 100644 pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch diff --git a/pkgs/applications/science/logic/coq/beta.nix b/pkgs/applications/science/logic/coq/beta.nix new file mode 100644 index 00000000000..c5c4221ac1e --- /dev/null +++ b/pkgs/applications/science/logic/coq/beta.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 = "coq-8.3-beta0-1"; + + src = fetchurl { + url = http://coq.inria.fr/distrib/V8.3-beta0/files/coq-8.3-beta0-1.tar.gz; + sha256 = "01m1x0gpzfsiybyqanm82ls8q63q0g2d9vvfs99zf4z1nny7vlf1"; + }; + + buildInputs = [ ocaml camlp5 ncurses lablgtk ]; + + 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"; + + patches = [ ./coq-8.3-beta0-1.patch ]; + + postPatch = '' + substituteInPlace scripts/coqmktop.ml --replace \ + "\"-I\"; \"+lablgtk2\"" \ + "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\"" + ''; + + 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"; + }; +} diff --git a/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch b/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch new file mode 100644 index 00000000000..a5259eb43c0 --- /dev/null +++ b/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch @@ -0,0 +1,20 @@ +diff -Nurp coq-8.3-beta0-1/configure coq-8.3-beta0-1-nix/configure +--- coq-8.3-beta0-1/configure 2010-02-16 12:37:58.000000000 +0100 ++++ coq-8.3-beta0-1-nix/configure 2010-05-11 17:47:44.000000000 +0200 +@@ -394,7 +394,6 @@ case $camldir_spec in + ocamlyaccexec=$CAMLBIN/ocamlyacc + ocamlmktopexec=$CAMLBIN/ocamlmktop + ocamlmklibexec=$CAMLBIN/ocamlmklib +- camlp4oexec=$CAMLBIN/camlp4o + esac + + if test ! -f "$CAMLC" ; then +@@ -626,7 +625,7 @@ case $COQIDE in + 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 diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 367e99223e7..a4a0a996b96 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -9209,6 +9209,11 @@ let camlp5 = camlp5_transitional; }; + coq_beta = import ../applications/science/logic/coq/beta.nix { + inherit stdenv fetchurl ocaml lablgtk ncurses; + camlp5 = camlp5_transitional; + }; + hol_light = import ../applications/science/logic/hol_light { inherit stdenv fetchurl ocaml_with_sources; };