diff options
| author | Marco Maggesi <maggesi@math.unifi.it> | 2010-05-11 20:14:46 +0000 |
|---|---|---|
| committer | Marco Maggesi <maggesi@math.unifi.it> | 2010-05-11 20:14:46 +0000 |
| commit | afbb01c90d4a10191bc68b68e2d484283eea329c (patch) | |
| tree | 8cfcb2384819c7f8dea7573c56e33f9bf09a8853 /pkgs/applications/science/logic | |
| parent | 76167b5bd37f61138b0276cb62417df9faf26e5d (diff) | |
| download | nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar.gz nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar.bz2 nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar.lz nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar.xz nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.tar.zst nixlib-afbb01c90d4a10191bc68b68e2d484283eea329c.zip | |
Add expression for Coq 8.3 beta
svn path=/nixpkgs/trunk/; revision=21734
Diffstat (limited to 'pkgs/applications/science/logic')
| -rw-r--r-- | pkgs/applications/science/logic/coq/beta.nix | 53 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch | 20 |
2 files changed, 73 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/coq/beta.nix b/pkgs/applications/science/logic/coq/beta.nix new file mode 100644 index 000000000000..c5c4221ac1ee --- /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 000000000000..a5259eb43c08 --- /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 |