summary refs log tree commit diff
path: root/pkgs/applications/science
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science')
-rw-r--r--pkgs/applications/science/logic/coq/configure.patch.gzbin0 -> 438 bytes
-rw-r--r--pkgs/applications/science/logic/coq/default.nix65
-rw-r--r--pkgs/applications/science/math/wxmaxima/default.nix36
3 files changed, 58 insertions, 43 deletions
diff --git a/pkgs/applications/science/logic/coq/configure.patch.gz b/pkgs/applications/science/logic/coq/configure.patch.gz
new file mode 100644
index 0000000000000..85ecfda6dae16
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/configure.patch.gz
Binary files differdiff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 475c68f7b9cf0..19827022072d6 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -1,23 +1,66 @@
-{stdenv, fetchurl, ocaml, ncurses}:
+# TODO:
+# - coqide compilation should be optional or (better) separate;
+# - coqide libraries are not installed;
 
-stdenv.mkDerivation (rec {
+{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
+
+let
+
+  pname = "coq";
+  version = "8.2pl1";
+  name = "${pname}-${version}";
+
+in
+
+stdenv.mkDerivation {
+  inherit name;
 
-  name = "coq-8.1pl3";
   src = fetchurl {
-    url = "http://coq.inria.fr/V8.1pl3/files/coq-8.1pl3.tar.gz";
-    sha256 = "7f8f45594adff2625312c5ecb144cb00d39c99201dac309c9286b34d01a36bb6";
+    url = "http://coq.inria.fr/V${version}/files/${name}.tar.gz";
+    sha256 = "7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c";
   };
 
-  buildInputs = [ocaml ncurses];
+  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
 
   prefixKey = "-prefix ";
-  patchPhase = ''
+
+  configureFlags =
+    "-camldir ${ocaml}/bin " +
+    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
+    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
+    "-opt -coqide opt";
+
+  buildFlags = "world"; # Debug with "world VERBOSE=1";
+
+  patches = [ ./configure.patch.gz ];
+
+  postPatch = ''
+    BASH=$(type -tp bash)
     UNAME=$(type -tp uname)
     MV=$(type -tp mv)
-    RM=$(type -tp cp)
-    substituteInPlace ./configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace Makefile --replace "/bin/mv" "$MV" \
+    RM=$(type -tp rm)
+    substituteInPlace configure --replace "/bin/bash" "$BASH" \
+                                --replace "/bin/uname" "$UNAME"
+    substituteInPlace Makefile --replace "/bin/bash" "$BASH" \
+                               --replace "/bin/mv" "$MV" \
                                --replace "/bin/rm" "$RM"
+    substituteInPlace Makefile.stage1 --replace "/bin/bash" "$BASH"
+    substituteInPlace install.sh --replace "/bin/bash" "$BASH"
+    substituteInPlace dev/v8-syntax/check-grammar --replace "/bin/bash" "$BASH"
+    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/math/wxmaxima/default.nix b/pkgs/applications/science/math/wxmaxima/default.nix
index 04cab117c81c9..403105aaaa7fa 100644
--- a/pkgs/applications/science/math/wxmaxima/default.nix
+++ b/pkgs/applications/science/math/wxmaxima/default.nix
@@ -1,5 +1,9 @@
 { stdenv, fetchurl, maxima, wxGTK }:
 
+# TODO: Build the correct ${maxima}/bin/maxima store path into wxMaxima so that
+#       it can run that binary without relying on $PATH, /etc/wxMaxima.conf, or
+#       ~/.wxMaxima.
+
 let
     name    = "wxmaxima";
     version = "0.8.3";
@@ -19,35 +23,3 @@ stdenv.mkDerivation {
     homepage = http://wxmaxima.sourceforge.net;
   };
 }
-
-# # $Id: PKGBUILD,v 1.10 2008/05/13 19:03:39 ronald Exp $
-# # Maintainer: Ronald van Haren <ronald.archlinux.org>
-# # Contributor: Angelo Theodorou <encelo@users.sourceforge.net>
-# # Contributor: Vinay S Shastry <vinayshastry@gmail.com>
-
-# pkgname=wxmaxima
-# pkgver=0.8.3
-# pkgrel=1
-# pkgdesc="A
-# arch=('i686' 'x86_64')
-# url="http://wxmaxima.sourceforge.net/"
-# license=('GPL2')
-# depends=('maxima>=5.18.1' 'libxml2>=2.7.3' 'wxgtk>=2.8.10.1')
-# source=(http://downloads.sourceforge.net/$pkgname/wxMaxima-$pkgver.tar.gz)
-# md5sums=('341913b9d54f24b796a50a3167b4d9b2')
-
-# build() {
-#   cd "${srcdir}/wxMaxima-${pkgver}"
-#   ./configure --prefix=/usr || return 1
-#   make || return 1
-#   make DESTDIR="${pkgdir}" install || return 1
-
-#   # Fix category in .desktop file
-#   sed -i -e 's/Utility;X-Red-Hat-Base;X-Red-Hat-Base-Only;/Science;Math;/' wxmaxima.desktop
-
-#   # Install desktop file and icon
-#   install -m755 -d "${pkgdir}/usr/share/applications"
-#   install -m755 -d "${pkgdir}/usr/share/pixmaps"
-#   install -m644 wxmaxima.desktop "${pkgdir}/usr/share/applications/" || return 1
-#   install -m644 data/wxmaxima.png "${pkgdir}/usr/share/pixmaps/" || return 1
-# }