From 0430167083c1cdca354b295f87290d7b10a930e7 Mon Sep 17 00:00:00 2001
From: Marco Maggesi <maggesi@math.unifi.it>
Date: Thu, 4 Nov 2010 11:24:27 +0000
Subject: [PATCH] Update Coq
svn path=/nixpkgs/trunk/; revision=24597
---
.../applications/science/logic/coq/8.3rc1.nix | 53 ------------------
....3-rc1_configure.patch => configure.patch} | 10 ++--
.../science/logic/coq/configure.patch.gz | Bin 438 -> 0 bytes
.../science/logic/coq/default.nix | 18 ++----
pkgs/top-level/all-packages.nix | 4 --
5 files changed, 10 insertions(+), 75 deletions(-)
delete mode 100644 pkgs/applications/science/logic/coq/8.3rc1.nix
rename pkgs/applications/science/logic/coq/{coq-8.3-rc1_configure.patch => configure.patch} (72%)
delete mode 100644 pkgs/applications/science/logic/coq/configure.patch.gz
diff --git a/pkgs/applications/science/logic/coq/8.3rc1.nix b/pkgs/applications/science/logic/coq/8.3rc1.nix
deleted file mode 100644
index 66eb4de833e8..000000000000
--- a/pkgs/applications/science/logic/coq/8.3rc1.nix
+++ /dev/null
@@ -1,53 +0,0 @@
-# TODO:
-# - coqide compilation should be optional or (better) separate;
-# - coqide libraries are not installed;
-
-{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
-
-stdenv.mkDerivation {
- name = "coq-devel-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 (development version)";
- 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-rc1_configure.patch b/pkgs/applications/science/logic/coq/configure.patch
similarity index 72%
rename from pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch
rename to pkgs/applications/science/logic/coq/configure.patch
index 9ae5d2d688a0..3989ea5c6015 100644
--- a/pkgs/applications/science/logic/coq/coq-8.3-rc1_configure.patch
+++ b/pkgs/applications/science/logic/coq/configure.patch
@@ -1,7 +1,7 @@
-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 @@
+diff -Nuar coq-8.3/configure coq-8.3.nixos/configure
+--- coq-8.3/configure 2010-10-14 16:02:46.000000000 +0200
++++ coq-8.3.nixos/configure 2010-11-04 09:57:16.000000000 +0100
+@@ -394,7 +394,6 @@
ocamlyaccexec=$CAMLBIN/ocamlyacc
ocamlmktopexec=$CAMLBIN/ocamlmktop
ocamlmklibexec=$CAMLBIN/ocamlmklib
@@ -9,7 +9,7 @@ diff -Nuar coq-8.3-rc1/configure coq-8.3-rc1.nixos/configure
esac
if test ! -f "$CAMLC" ; then
-@@ -647,7 +646,7 @@
+@@ -637,7 +636,7 @@
no) LABLGTKLIB=+lablgtk2 # Pour le message
LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
yes) LABLGTKLIB="$lablgtkdir" # Pour le message
diff --git a/pkgs/applications/science/logic/coq/configure.patch.gz b/pkgs/applications/science/logic/coq/configure.patch.gz
deleted file mode 100644
index 85ecfda6dae166ef6bb80f561242684b473c3e67..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 438
zcmV;n0ZINJiwFoXow!N@17mM)W@%@2a%C=XVRU0?0F9K(PQx$|Mc4IL42WHDaS9Y#
zgjDDX3HS%snNX{V9UK?YzsCtF4>1*!O_Y1)o=CRrrLSx6pxv$t8_+}_EVgqn{#9O&
zCry=~t*is>iXV}5_PvY6^53#qquF4f1OwtoyesVs>F9|lY*~Wb{_Si7(v<{+l#*<W
zCQ8kux{@k~JfB})&y^ah{R5dwTx3~x&^!ocax&=z7t^`Q{|FWfkms}M=@n$%YYK~n
zfDw43>uRTs!FM#bC(FC1$NPupv#<DTrrt!~5JP?bW2&+%aw_FQj-dN!F8uG2AryeE
zPJa|&ONiJ;I09M1aX+^_h8u`$bi56W!LAPMV22oz0^cY>iaBL($g($#vMrD*r<hZA
z5ko`vd%{qpQ{u3q6rY5lsOZ(NSSz2Vf)2X_f(|hxwI;8T6f??=4y|?M6)+%<Bw*Y%
zhctW05_w;?w51~qMQeg>BIy_qM-p{9m87F53`Nu?T0=Sp#F3<{LAF~P$z$?OIjS}G
gAt@RdN8^1(J37D;G!?$lhi=cr2mRT}?mPzo0K|UE9{>OV
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 8716d39a1769..d72a2104370c 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -4,7 +4,7 @@
{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
let
- version = "8.2pl2";
+ version = "8.3";
in
stdenv.mkDerivation {
@@ -12,7 +12,7 @@ stdenv.mkDerivation {
src = fetchurl {
url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
- sha256 = "0dh2vv3bvz8694dd12kjdkdaq19l1vslvygzif11igshc5bw4rhf";
+ sha256 = "02iy4rxz1n1kc85fb3vs4xpxqfxjw87y2gvmi39fxrj8742qx0dx";
};
buildInputs = [ ocaml camlp5 ncurses lablgtk ];
@@ -27,21 +27,13 @@ stdenv.mkDerivation {
buildFlags = "world"; # Debug with "world VERBOSE=1";
- patches = [ ./configure.patch.gz ];
+ patches = [ ./configure.patch ];
postPatch = ''
- BASH=$(type -tp bash)
UNAME=$(type -tp uname)
- MV=$(type -tp 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 configure --replace "/bin/uname" "$UNAME"
+ substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
substituteInPlace scripts/coqmktop.ml --replace \
"\"-I\"; \"+lablgtk2\"" \
"\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 571f931e52d6..de151eab5ad8 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6836,10 +6836,6 @@ let
camlp5 = camlp5_transitional;
};
- coq_devel = callPackage ../applications/science/logic/coq/8.3rc1.nix {
- camlp5 = camlp5_transitional;
- };
-
eprover = callPackage ../applications/science/logic/eProver {
texLive = texLiveAggregationFun {
paths = [