diff options
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/README.Debian | 28 | ||||
| -rw-r--r-- | debian/changelog | 158 | ||||
| -rw-r--r-- | debian/compat | 1 | ||||
| -rw-r--r-- | debian/control | 65 | ||||
| -rw-r--r-- | debian/copyright | 19 | ||||
| -rw-r--r-- | debian/coq-libs.install | 4 | ||||
| -rw-r--r-- | debian/coq.desktop | 7 | ||||
| -rw-r--r-- | debian/coq.dirs | 4 | ||||
| -rw-r--r-- | debian/coq.emacsen-install | 45 | ||||
| -rw-r--r-- | debian/coq.emacsen-remove | 15 | ||||
| -rw-r--r-- | debian/coq.emacsen-startup | 21 | ||||
| -rw-r--r-- | debian/coq.install | 14 | ||||
| -rw-r--r-- | debian/coq.menu | 4 | ||||
| -rw-r--r-- | debian/coq.xpm | 54 | ||||
| -rw-r--r-- | debian/coq7-libs.install | 3 | ||||
| -rw-r--r-- | debian/coqide.dirs | 2 | ||||
| -rw-r--r-- | debian/coqide.install | 2 | ||||
| -rw-r--r-- | debian/docs | 3 | ||||
| -rwxr-xr-x | debian/rules | 92 |
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 |