Getting prepared for the licensing-problems-free 8.0 release of COQ.

19 files changed, 541 insertions, 0 deletions

diff --git a/debian/README.Debian b/debian/README.Debian
new file mode 100644
index 00000000..5657bfca
--- /dev/null
+++ b/debian/README.Debian
@@ -0,0 +1,28 @@
+Coq package for Debian
+----------------------
+
+Note that all bytecode files in this package need to be left
+'unstripped' after compiling. The reason is the following:
+
+  It is possible to strip the .out corresponding to ocaml code compiled in
+  native code (and it is done in Coq (coqopt.out) When compiling in
+  byte-code, the Coq system uses the -custom option in order to get an
+  autonomous executable (running independently of an ocaml implementation on
+  your computer). The way it works is that the .out file is composed of the
+  executable of the byte-code interpreter plus the byte-code for your own
+  program which is stored in the symbol table zone...  stripping such an
+  executable, just remove your byte-code and consequentely cannot run
+  properly.
+
+Moreover the bytecode version is installed even on platforms having a
+native version as the dynamic loading of tactics works only with the
+bytecode version.
+
+For interactive use of coqtop, we suggest
+- either the Debian cle package
+- or the Proof-General (x)emacs mode, which unfortunately can not be
+distributed by Debian for copyright reasons. However, a Debian package
+might become available at proof general home page in the future
+(http://zermelo.dcs.ed.ac.uk/~proofgen)
+
+However we recommand you to use the CoqIde gtk interface provided in coqide.
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 00000000..b610546e
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,158 @@
+coq (8.0-1) unstable; urgency=low
+
+  * New upstream release.
+  * Libraries are now in separate packages (coq-libs and coq7-libs).
+  * An additionnal package provides coqide.
+
+ -- Samuel Mimram <samuel.mimram@ens-lyon.org>  Thu, 15 Jul 2004 17:35:00 +0200
+
+coq (7.3.1-3) unstable; urgency=low
+
+  * Added build-dependency on ocaml-best-compilers, check for opt compilers
+    in the configure-stamp target of debian/rules. Thanks to Mike Furr for
+    the patch (closes: #242761).
+  * Converted changelog to UTF-8.
+
+ -- Ralf Treinen <treinen@debian.org>  Fri,  9 Apr 2004 18:03:41 +0200
+
+coq (7.3.1-2) unstable; urgency=low
+
+  * Standards-Version 3.6.1.
+  * File debian/compat instead of variable DH_COMPAT.
+  * Build with ocaml-3.07.
+  * Maintainers: debian-ocaml-maint, Uploaders: The Ocaml Gang.
+  * Switch to dpatch system:
+    - 01_ocaml307: patch by Hugo Herbelin (thanks!) for compilation with
+      ocaml 3.07.
+  * Removed timeout crutch which used to be necessary for ocaml 3.04.
+  * Removed forcing of byte compilation on ppc.
+  * debian/rules: some cosmetic changes.
+  * Short description: capitalize first letter, drop terminal dot.
+
+ -- Ralf Treinen <treinen@debian.org>  Tue,  7 Oct 2003 22:11:31 +0200
+
+coq (7.3.1-1) unstable; urgency=low
+
+  * New bugfix upstream version.
+  * Proof General is now Recommended since he has been freed (closes:
+    Bug#162894).
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Mon,  7 Oct 2002 12:34:03 +0200
+
+coq (7.3-1) unstable; urgency=low
+
+  * New upstream version.
+ 
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 22 May 2002 14:48:21 +0200
+
+coq (7.2-9) unstable; urgency=low
+  * ocamlc.opt completely broken on powerpc. Added a special case in
+    "rules" for using only bytecode.
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Fri, 15 Feb 2002 09:17:20 +0100
+
+coq (7.2-8) unstable; urgency=low
+
+  * "timeout" time is now 5300s (< 90 min).
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Thu, 14 Feb 2002 17:38:06 +0100
+
+coq (7.2-7) unstable; urgency=low
+
+  * Build now uses ocamlc.opt and ocamlopt.opt if available.
+  * Dependency forced on ocaml >= 3.04 (dependency ocaml >=3.04 | camlp4
+    does not make buildd happy. See http://buildd.debian.org/fetch.php?
+    &pkg=coq&ver=7.2-5&arch=arm&stamp=1013388706&file=log&as=raw).
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Tue, 12 Feb 2002 09:10:01 +0100
+
+coq (7.2-6) unstable; urgency=low
+
+  * Typo in rules, which made the build process always build in
+    bytecode. Fixed.
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Mon, 11 Feb 2002 11:22:21 +0100
+
+coq (7.2-5) unstable; urgency=low
+
+  * Pb with timeout, used in 7.2-4 (bug 132927) making the build process
+    fail when compilation in native mode fails. Workaround in rules: after
+    a "timeout ... make ..." we try a "make -q" to check that everything
+    has been done correctly.
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  8 Feb 2002 10:08:10 +0100
+
+coq (7.2-4) unstable; urgency=low
+  * Native code compilation failed on sparc; coqtop built by ocamlopt
+    entered an infinite loop on powerpc. Fixed (using timeout for powerpc:
+    if coqtop loops, it is rebuild using the bytecode compiler)
+
+ -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  1 Feb 2002 11:04:25 +0100
+
+coq (7.2-3) unstable; urgency=low
+  * Workaround for problems with buildd/apt trying to install camlp4
+    (closes: Bug#130046).
+  
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Mon, 21 Jan 2002 09:46:16 +0100
+
+coq (7.2-2) unstable; urgency=low
+
+  * Build-Depends now requires camlp4 instead of camlp4 (>=3.01) since
+    camlp4 is a virtual package provided by ocaml >=3.04.
+
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Fri, 11 Jan 2002 11:08:03 +0100
+
+coq (7.2-1) unstable; urgency=low
+  * New upstream version.
+
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Wed,  9 Jan 2002 14:02:42 +0100
+
+coq (7.1-2) unstable; urgency=low
+
+  * Fixed policy problem (conf files).
+  * Trying to compile in bytecode if native code compilation fails
+    (closes: Bug#119714)
+  * Errors raised by the Simpl tactic is an upstream bug and should
+    have been fixed in 7.0 (closes: Bug#74518).
+
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue, 11 Dec 2001 13:33:15 +0100
+
+coq (7.1-1) unstable; urgency=low
+  * New upstream version.
+
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  25 Sep 2001 16:27:04 +0200
+
+coq (7.0-1) unstable; urgency=low
+  * New maintainer Judicaël Courant <Judicael.Courant@lri.fr>.
+  * New upstream version.
+  * Added Build-Depends (closes: Bug#70273).
+  * Cleaned up dependencies.
+  * Emacs mode installation now follows Emacs policy.
+  * Made compilation non-interactive (closes: Bug#92461).
+  * Added Suggests cle.
+  
+
+ -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  17 Apr 2001 19:24:34 +0200
+
+coq (6.3.1-3) unstable; urgency=low
+
+  * Patched to allow use of ocaml3.
+
+ -- Fernando Sanchez <fer@debian.org>  Fri,  7 Jul 2000 08:05:47 +0200
+
+coq (6.3.1-2) unstable; urgency=low
+
+  * Some changes to allow successful porting of this package:
+  * Added checking for ocamlopt.opt before running ./configure with -opt,
+    and configure without it if it is not present for this architecture.
+  * Added checking for ocamlopt before making world-opt.
+
+ -- Fernando Sanchez <fer@debian.org>  Sat, 18 Dec 1999 16:45:01 +0100
+
+coq (6.3.1-1) unstable; urgency=low
+
+  * Initial Release.
+
+ -- Fernando Sanchez <fer@debian.org>  Fri,  3 Dec 1999 22:06:04 +0100
+
+
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 00000000..bf0d87ab
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+4
\ No newline at end of file
diff --git a/debian/control b/debian/control
new file mode 100644
index 00000000..bddc2fdb
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,65 @@
+Source: coq
+Section: devel
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
+Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Jerome Marant <jerome@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>
+Standards-Version: 3.6.1
+Build-Depends: debhelper (>= 4.0.0), ocaml-3.07, ocaml-best-compilers, liblablgtk2-ocaml-dev
+
+Package: coq
+Architecture: any
+Depends: ${shlibs:Depends}, coq-libs
+Suggests: coq-doc, ocaml-3.07, proofgeneral-coq, ledit, cle
+Recommends: coq-doc, coqide | proofgeneral-coq
+Description: Proof assistant for higher-order logic
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This packages provides coqtop, a command line interface to Coq.
+ .
+ A graphical interface for Coq is provided in the coqide package.
+ Coq can also be used with ProofGeneral, which allows proofs to be
+ edited using emacs and xemacs.  This requires the proofgeneral-coq
+ package to be installed.
+
+Package: coqide
+Architecture: any
+Depends: coq (>= 8.0), ${shlibs:Depends}
+Description: Proof assistant for higher-order logic
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This package provides CoqIde, a graphical user interface for
+ developing proofs.
+
+Package: coq-libs
+Architecture: any
+Recommends: coq (>= 8.0)
+Conflicts: coq (<< 8.0)
+Description: Proof assistant for higher-order logic
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This package provides existing theories that new proofs can be
+ based upon, including theories of arithmetic and Boolean values.
+
+Package: coq7-libs
+Architecture: any
+Recommends: coq (>= 8.0)
+Description: Proof assistant for higher-order logic
+ Coq is a proof assistant for higher-order logic, which allows the
+ development of computer programs consistent with their formal
+ specification. It is developed using Objective Caml and Camlp4.
+ For more information, see <http://coq.inria.fr/>.
+ .
+ This package provides existing theories from Coq 7 in Coq 8, and
+ allows proofs that were developed in Coq 7 to be used in Coq 8.
+ It is also required to translate theories in Coq 7 syntax into 
+ the new syntax introduced in Coq 8.  However, this package does
+ not need to be installed to use Coq 7.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 00000000..59529f30
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,19 @@
+This package was debianized by Fernando Sanchez <fer@debian.org>
+
+The "Coq proof assistant" was developed conjointly by
+        INRIA (since 1985),
+        Laboratoire de l'Informatique du Parallelisme LIP
+        associated to CNRS and ENS Lyon (sept.89-sept.97),
+        Laboratoire de Recherche en Informatique
+        associated to CNRS and Paris 11 (since sept. 97).
+
+The complete list of developpers and contributors can be found in
+/usr/share/doc/doc/CREDITS.gz
+
+Copyright: the Coq Proof Assistant is distributed under the terms of the GNU
+Lesser General Public Licence, version 2.1, see
+/usr/share/common-licenses/LGPL-2.1.
+
+However there are two exceptions: files in the directories contrib/jprover and
+ide/utils are distributed under the terms of the GNU General Public Licence,
+see /usr/share/common-licenses/GPL.
diff --git a/debian/coq-libs.install b/debian/coq-libs.install
new file mode 100644
index 00000000..22e69d53
--- /dev/null
+++ b/debian/coq-libs.install
@@ -0,0 +1,4 @@
+usr/lib/coq/contrib
+usr/lib/coq/states
+usr/lib/coq/theories
+
diff --git a/debian/coq.desktop b/debian/coq.desktop
new file mode 100644
index 00000000..af2698ec
--- /dev/null
+++ b/debian/coq.desktop
@@ -0,0 +1,7 @@
+[Desktop Entry]
+Name=Coq
+Comment=Proof Assistant
+Exec=/usr/bin/coqide
+Type=Application
+Terminal=0
+Icon=/usr/share/pixmaps/coq.xpm
diff --git a/debian/coq.dirs b/debian/coq.dirs
new file mode 100644
index 00000000..90431880
--- /dev/null
+++ b/debian/coq.dirs
@@ -0,0 +1,4 @@
+usr/bin
+usr/lib
+usr/lib/coq
+usr/share/pixmaps
diff --git a/debian/coq.emacsen-install b/debian/coq.emacsen-install
new file mode 100644
index 00000000..1ed8fe43
--- /dev/null
+++ b/debian/coq.emacsen-install
@@ -0,0 +1,45 @@
+#! /bin/sh -e
+# /usr/lib/emacsen-common/packages/install/coq
+
+# Written by Jim Van Zandt <jrv@vanzandt.mv.com>, borrowing heavily
+# from the install scripts for gettext by Santiago Vila
+# <sanvila@ctv.es> and octave by Dirk Eddelbuettel <edd@debian.org>.
+
+FLAVOR=$1
+PACKAGE=coq
+
+if [ ${FLAVOR} = emacs ]; then exit 0; fi
+
+echo install/${PACKAGE}: Handling install for emacsen flavor ${FLAVOR}
+
+#FLAVORTEST=`echo $FLAVOR | cut -c-6`
+#if [ ${FLAVORTEST} = xemacs ] ; then
+#    SITEFLAG="-no-site-file"
+#else
+#    SITEFLAG="--no-site-file"
+#fi
+FLAGS="${SITEFLAG} -q -batch -l path.el -f batch-byte-compile"
+
+ELDIR=/usr/share/emacs/site-lisp/${PACKAGE}
+ELCDIR=/usr/share/${FLAVOR}/site-lisp/${PACKAGE}
+
+# Install-info-altdir does not actually exist. 
+# Maybe somebody will write it.
+if test -x /usr/sbin/install-info-altdir; then
+    echo install/${PACKAGE}: install Info links for ${FLAVOR}
+    install-info-altdir --quiet --section "" "" --dirname=${FLAVOR} /usr/info/${PACKAGE}.info.gz
+fi
+
+install -m 755 -d ${ELCDIR}
+cd ${ELDIR}
+FILES=`echo *.el`
+cp ${FILES} ${ELCDIR}
+cd ${ELCDIR}
+
+cat << EOF > path.el
+(setq load-path (cons "." load-path) byte-compile-warnings nil)
+EOF
+${FLAVOR} ${FLAGS} ${FILES}
+rm -f *.el path.el
+
+exit 0
diff --git a/debian/coq.emacsen-remove b/debian/coq.emacsen-remove
new file mode 100644
index 00000000..02b6392c
--- /dev/null
+++ b/debian/coq.emacsen-remove
@@ -0,0 +1,15 @@
+#!/bin/sh -e
+# /usr/lib/emacsen-common/packages/remove/coq
+
+FLAVOR=$1
+PACKAGE=coq
+
+if [ ${FLAVOR} != emacs ]; then
+    if test -x /usr/sbin/install-info-altdir; then
+        echo remove/${PACKAGE}: removing Info links for ${FLAVOR}
+        install-info-altdir --quiet --remove --dirname=${FLAVOR} /usr/info/coq.info.gz
+    fi
+
+    echo remove/${PACKAGE}: purging byte-compiled files for ${FLAVOR}
+    rm -rf /usr/share/${FLAVOR}/site-lisp/${PACKAGE}
+fi
diff --git a/debian/coq.emacsen-startup b/debian/coq.emacsen-startup
new file mode 100644
index 00000000..91b56915
--- /dev/null
+++ b/debian/coq.emacsen-startup
@@ -0,0 +1,21 @@
+;; -*-emacs-lisp-*-
+;;
+;; Emacs startup file for the Debian GNU/Linux coq package
+;;
+;; Originally contributed by Nils Naumann <naumann@unileoben.ac.at>
+;; Modified by Dirk Eddelbuettel <edd@debian.org>
+;; Adapted for dh-make by Jim Van Zandt <jrv@vanzandt.mv.com>
+
+;; The coq package follows the Debian/GNU Linux 'emacsen' policy and
+;; byte-compiles its elisp files for each 'emacs flavor' (emacs19,
+;; xemacs19, emacs20, xemacs20...).  The compiled code is then
+;; installed in a subdirectory of the respective site-lisp directory.
+;; We have to add this to the load-path:
+
+(setq load-path (cons (concat "/usr/share/"
+                              (symbol-name flavor)
+			      "/site-lisp/coq") load-path))
+
+(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
+(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+
diff --git a/debian/coq.install b/debian/coq.install
new file mode 100644
index 00000000..155e13af
--- /dev/null
+++ b/debian/coq.install
@@ -0,0 +1,14 @@
+usr/bin/coqc
+usr/bin/coqdep
+usr/bin/coqdoc
+usr/bin/coq-interface*
+usr/bin/coq_makefile
+usr/bin/coqmktop
+usr/bin/coq-tex
+usr/bin/coqtop*
+usr/bin/coqwc
+usr/bin/gallina
+usr/share/emacs/site-lisp/coq
+usr/share/man/man1/c*
+usr/share/man/man1/gallina.1
+usr/share/texmf/tex/latex/misc/*
diff --git a/debian/coq.menu b/debian/coq.menu
new file mode 100644
index 00000000..0a1e30f7
--- /dev/null
+++ b/debian/coq.menu
@@ -0,0 +1,4 @@
+?package(coq):command="/usr/bin/coqtop" \
+  icon="/usr/share/pixmaps/coq.xpm" \
+  needs="text" \
+  section="Apps/Math" title="Coq"
diff --git a/debian/coq.xpm b/debian/coq.xpm
new file mode 100644
index 00000000..e58ebad7
--- /dev/null
+++ b/debian/coq.xpm
@@ -0,0 +1,54 @@
+/* XPM */
+static char *coq[] = {
+/* columns rows colors chars-per-pixel */
+"32 32 16 1",
+"  c #220C08",
+". c #342A2C",
+"X c #5A261F",
+"o c #6A4D4B",
+"O c #923827",
+"+ c #BF381C",
+"@ c #996252",
+"# c #837671",
+"$ c #D35E3A",
+"% c #CA7852",
+"& c #E19667",
+"* c #A59082",
+"= c #B9ADA8",
+"- c #EAB48F",
+"; c #F2D3B6",
+": c #FCFDF9",
+/* pixels */
+"::::::::::::::::::::::::::::::::",
+"::::::::::::::::::::::::::::::::",
+":::::X.:::::::::::::::::::::::::",
+"::::++-==:::::::::::::::::::::::",
+":::+;;+$:*::::::::::::::::::::::",
+":::;-++%:: :::::::::::::::::::::",
+":::*+++#:::;::::::::::::::::::::",
+"::::= +O::::::::::::::::::::::::",
+":::::: :::::o:::::::::::::::::::",
+"::::::=;:::::=::::::::::::::*:::",
+"::::::;::::::::: :::::::::::=:::",
+":::::=:::::::::::::::::: :::.:::",
+":::::*:::::::::::::.::.::::;X:::",
+":::::;::::::::::::::o:::;:-*.:::",
+"::::*;;;::::::;;:;-::--:;&&&X:::",
+"::::#;;;;-;;::;;;;;-;;--%%-%::::",
+":::::--;;@;;;;;-;-;--%oO%&% ::::",
+":::::.--;-@%&--&&%$$OOXO%%@:::::",
+"::::::o&--& O+XO&& XXX Oo ::::::",
+"::::::;@%%&%$  XX$X X Oo@ ::::::",
+"::::::::=O$OO+XX O X OO@ :::::::",
+"::::::::::;+X O%OOOOOOOo::::::::",
+"::::::::::::oOOXXX X  ::::::::::",
+":::::::::::::XX  X X::::::::::::",
+"::::::::::::::    .:::::::::::::",
+":::::::::::::: o:.::::::::::::::",
+":::::::::::::: #:.::::::::::::::",
+":::::::::::-oX%oo&*:::::::::::::",
+"::::::::::::o.#:::=@::::::::::::",
+"::::::::::::::::::::::::::::::::",
+"::::::::::::::::::::::::::::::::",
+"::::::::::::::::::::::::::::::::"
+};
diff --git a/debian/coq7-libs.install b/debian/coq7-libs.install
new file mode 100644
index 00000000..e888a17f
--- /dev/null
+++ b/debian/coq7-libs.install
@@ -0,0 +1,3 @@
+usr/lib/coq/contrib7
+usr/lib/coq/states7
+usr/lib/coq/theories7
diff --git a/debian/coqide.dirs b/debian/coqide.dirs
new file mode 100644
index 00000000..f783eb3a
--- /dev/null
+++ b/debian/coqide.dirs
@@ -0,0 +1,2 @@
+usr/share/doc/coqide
+usr/share/applnk/Development
diff --git a/debian/coqide.install b/debian/coqide.install
new file mode 100644
index 00000000..7bc6f33c
--- /dev/null
+++ b/debian/coqide.install
@@ -0,0 +1,2 @@
+usr/bin/coqide*
+usr/lib/coq/ide
diff --git a/debian/docs b/debian/docs
new file mode 100644
index 00000000..62998f27
--- /dev/null
+++ b/debian/docs
@@ -0,0 +1,3 @@
+README
+CREDITS
+CHANGES
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 00000000..b9552a69
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,92 @@
+#!/usr/bin/make -f
+# debian/rules for coq
+
+COQPREF=$(CURDIR)/debian/tmp
+ADDPREF=COQINSTALLPREFIX=$(COQPREF)
+
+MAKEQ=$(MAKE) -q
+
+CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man \
+	--emacslib /usr/share/emacs/site-lisp/coq --reals all
+
+configure: configure-stamp
+configure-stamp: patch
+	dh_testdir
+	if [ -e /usr/bin/ocamlc.opt ]; \
+	then \
+		./configure -opt $(CONFIGUREOPTS); \
+	else \
+		./configure $(CONFIGUREOPTS); \
+	fi
+	if [ `arch` = ppc ] ; then ./configure $(CONFIGUREOPTS) ; fi
+	touch configure-stamp
+
+build: configure-stamp build-stamp
+build-stamp:
+	dh_testdir
+	if grep -q BEST=opt config/Makefile; \
+	then ($(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
+	      && $(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
+	      && $(MAKEQ) bin/coqtop.opt bin/coqtop \
+	      && $(MAKEQ) states \
+	      && $(MAKEQ) world ) \
+         ||  (echo WARNING: NATIVE CODE COMPILATION FAILED \
+	    && echo Trying to build coq in bytecode \
+	    && $(MAKE) archclean clean \
+	    && $(MAKE) BEST=byte world \
+	    && echo NATIVE CODE COMPILATION FAILED \
+	    && echo Coq was built in bytecode instead); \
+	else $(MAKE) world; \
+	fi
+	$(MAKE) world
+	touch test-suite/success/debian.v8
+	$(MAKE) check
+	touch build-stamp
+
+clean:
+	dh_testdir
+	dh_testroot
+	rm -f build-stamp configure-stamp
+
+	-$(MAKE) clean
+	-$(MAKE) archclean
+	rm -f bin/parser.opt
+	rm -f tools/coqdoc/*.cm[oi]
+	rm -f config/coq_config.ml config/Makefile test-suite/check.log
+
+	dh_clean
+
+install: build
+	dh_testdir
+	dh_testroot
+	dh_clean -k
+	dh_installdirs
+
+	$(MAKE) $(ADDPREF) install || $(MAKE) BEST=byte $(ADDPREF) install
+	-strip -R .note -R .comment $(COQPREF)/usr/bin/coqtop.opt
+	-strip -R .note -R .comment $(COQPREF)/usr/bin/coqide.opt
+	-strip -R .note -R .comment $(COQPREF)/usr/bin/coq-interface.opt
+#	-strip -R .note -R .comment $(COQPREF)/usr/bin/parser.opt
+	install debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
+	install debian/coq.desktop debian/coqide/usr/share/applnk/Development
+	dh_install --sourcedir=$(COQPREF)
+
+binary-indep: build install
+
+binary-arch: build install
+	dh_testdir
+	dh_testroot
+	dh_installdocs
+	dh_installemacsen
+	dh_installchangelogs CHANGES
+	dh_link
+	dh_compress
+	dh_fixperms
+	dh_installdeb
+	dh_shlibdeps
+	dh_gencontrol
+	dh_md5sums
+	dh_builddeb
+
+binary: binary-indep binary-arch
+.PHONY: build clean binary-indep binary-arch binary install configure patch unpatch