summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
Diffstat (limited to 'debian')
-rw-r--r--debian/README.Debian28
-rw-r--r--debian/changelog158
-rw-r--r--debian/compat1
-rw-r--r--debian/control65
-rw-r--r--debian/copyright19
-rw-r--r--debian/coq-libs.install4
-rw-r--r--debian/coq.desktop7
-rw-r--r--debian/coq.dirs4
-rw-r--r--debian/coq.emacsen-install45
-rw-r--r--debian/coq.emacsen-remove15
-rw-r--r--debian/coq.emacsen-startup21
-rw-r--r--debian/coq.install14
-rw-r--r--debian/coq.menu4
-rw-r--r--debian/coq.xpm54
-rw-r--r--debian/coq7-libs.install3
-rw-r--r--debian/coqide.dirs2
-rw-r--r--debian/coqide.install2
-rw-r--r--debian/docs3
-rwxr-xr-xdebian/rules92
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