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 85ecfda6dae1..000000000000
Binary files a/pkgs/applications/science/logic/coq/configure.patch.gz and /dev/null differ
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 = [