Proof General: Build and install via the makefile.

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

pkgs/applications/editors/emacs-modes/proofgeneral/default.nix

@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, emacs, perl }:
+{ stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake }:
 
 let
   pname = "ProofGeneral";
@@ -15,28 +15,32 @@ stdenv.mkDerivation {
     sha256 = "ae430590d6763618df50a662a37f0627d3c3c8f31372f6f0bb2116b738fc92d8";
   };
 
-  buildInputs = [ emacs perl ];
-
   sourceRoot = name;
 
-  postPatch = "EMACS=emacs make clean";
+  buildInputs = [ emacs texinfo texLive perl which ];
 
-  # Skip building ...
-  buildPhase = "true";
+  patchPhase =
+    '' sed -i "Makefile" \
+           -e "s|^\(\(DEST_\)\?PREFIX\)=.*$|\1=$out|g ; \
+               s|/sbin/install-info|install-info|g"
 
-  installPhase = ''
-    DEST=$out/share/emacs/site-lisp/ProofGeneral
-    ensureDir $DEST
-    cp -a * $DEST
-  '';
+       sed -i "bin/proofgeneral" -e's/which/type -p/g'
+    '';
+
+  installPhase =
+    # Copy `texinfo.tex' in the right place so that `texi2pdf' works.
+    '' cp -v "${automake}/share/"automake-*/texinfo.tex doc
+       make install install-doc
+    '';
 
   meta = {
-    description = "A generic front-end for proof assistants";
+    description = "Proof General, an Emacs front-end for proof assistants";
     longDescription = ''
       Proof General is a generic front-end for proof assistants (also known as
       interactive theorem provers), based on the customizable text editor Emacs.
     '';
     homepage = website;
-    license = "GPL";
+    license = "GPLv2+";
+    platforms = stdenv.lib.platforms.gnu;  # arbitrary choice
   };
 }

pkgs/top-level/all-packages.nix

@@ -7665,7 +7665,7 @@ let
     };
 
     proofgeneral = import ../applications/editors/emacs-modes/proofgeneral {
-       inherit stdenv fetchurl emacs perl;
+      inherit stdenv fetchurl emacs texinfo texLive perl which automake;
     };
 
     quack = import ../applications/editors/emacs-modes/quack {