diff options
| -rw-r--r-- | distrib/Makefile | 2 | ||||
| -rw-r--r-- | distrib/debian/README.Debian | 19 | ||||
| -rw-r--r-- | distrib/debian/changelog | 9 | ||||
| -rw-r--r-- | distrib/debian/control | 9 | ||||
| -rw-r--r-- | distrib/debian/copyright | 64 | ||||
| -rw-r--r-- | distrib/debian/docs | 2 | ||||
| -rwxr-xr-x | distrib/debian/rules | 4 |
7 files changed, 37 insertions, 72 deletions
diff --git a/distrib/Makefile b/distrib/Makefile index 2f6d7ee27..442d7f93d 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -25,6 +25,7 @@ WWWDIR=/net/pauillac/infosystems/www/coq COQPACKAGE=coq-${VERSION} COQRPMPACKAGE=coq-${VERSION}-${RELEASENUM} +COQDEBPACKAGE=coq_${VERSION}-${RELEASENUM}_i386.deb ###################### @@ -304,3 +305,4 @@ deb: ${COQPACKAGE}.tar.gz cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz cp -a debian deb_build/${COQPACKAGE} cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us + lintian deb_build/${COQDEBPACKAGE} diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian index 7dc4ee03d..1aec78c0b 100644 --- a/distrib/debian/README.Debian +++ b/distrib/debian/README.Debian @@ -1,9 +1,8 @@ Coq package for Debian ---------------------- -As an unusual thing, some files (*.out) in this package need to be left -'unstripped' after compiling. The reason, as explained by the authors, is -the following: +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 @@ -14,3 +13,17 @@ the following: 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) + + + diff --git a/distrib/debian/changelog b/distrib/debian/changelog index 65d7fa05f..ab6c3b804 100644 --- a/distrib/debian/changelog +++ b/distrib/debian/changelog @@ -1,10 +1,17 @@ +coq (7.0-2) unstable; urgency=low + * Trying to compile in bytecode if native code compilation fails (closes: Bug#119714) + * Errors raised by the Simpl tactic is an upstream bug and was probably fixed by switching to 7.0 (closes: Bug#74518). + + -- Judicaël Courant <Judicael.Courant@lri.fr> Tue, 11 Dec 2001 13:33:15 +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. + * 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 diff --git a/distrib/debian/control b/distrib/debian/control index c36ceaa98..67bed545d 100644 --- a/distrib/debian/control +++ b/distrib/debian/control @@ -2,13 +2,14 @@ Source: coq Section: devel Priority: optional Maintainer: Judicaël Courant <Judicael.Courant@lri.fr> -Standards-Version: 3.0.1 -Build-Depends: debhelper (>= 2), ocaml (>= 3.00-1), camlp4 (>= 3.00-1) +Standards-Version: 3.5.3 +Build-Depends: debhelper (>= 2), ocaml (>= 3.01), camlp4 (>= 3.01) Package: coq Architecture: any -Depends: ${shlibs:Depends} -Suggests: coq-doc, ocaml (>= 3.00-1), camlp4 (>= 3.00-1) +Depends: ocaml (>= 3.01), ${shlibs:Depends} +Suggests: ocaml (>= 3.01), camlp4 (>= 3.01), cle +Recommends: coq-doc Description: a 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 diff --git a/distrib/debian/copyright b/distrib/debian/copyright index 88eafcc0b..b5d9eadf4 100644 --- a/distrib/debian/copyright +++ b/distrib/debian/copyright @@ -1,7 +1,4 @@ -This package was debianized by Fernando Sanchez <fer@debian.org> on -Fri, 3 Dec 1999 22:06:04 +0100. - -It was downloaded from ftp://ftp.inria.fr/INRIA/coq +This package was debianized by Fernando Sanchez <fer@debian.org> The "Coq proof assistant" was developed conjointly by INRIA (since 1985), @@ -10,63 +7,8 @@ The "Coq proof assistant" was developed conjointly by Laboratoire de Recherche en Informatique associated to CNRS and Paris 11 (since sept. 97). -The following people have contributed to the core of the system -during the indicated time : - - Bruno Barras, (INRIA, 1995-1999) - Cristina Cornes, (INRIA, 1993-1996) - David Delahaye, (INRIA, 1997-1999) - Daniel de Rauglaudre, (INRIA, 1996-1998) - Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-1999) - Eduardo Giménez, (ENS Lyon, 1993-1996, INRIA, 1997-1998) - Hugo Herbelin, (INRIA, 1996-1999) - Gérard Huet, (INRIA, 1985-1997) - César Muñoz, (INRIA, 1994-1995) - Chetan Murthy, (INRIA, 1992-1994) - Catherine Parent-Vigouroux, (ENS Lyon 1992-1995) - Patrick Loiseleur, (Paris 11, 1997-1999) - Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) - (Paris 11, 1997-1999) - Amokrane Saïbi, (INRIA, 1993-1998) - -The following directories contain independent contributions: -tactics/contrib/eqdecide - developed by Eduardo Gimenez (INRIA, 1997-1998) -tactics/contrib/extraction - developed by Benjamin Werner (INRIA, 1989) - and Jean-Christophe Filliatre (ENS Lyon, 1994-1997) -tactics/contrib/linear - developed by Jean-Christophe Filliatre (ENS Lyon, 1994-1997) -tactics/contrib/natural - developed by Yann Coscoy (INRIA, 1996) -tactics/contrib/omega - developed by Pierre Cregut (CNET-France Telecom, 1996) -tactics/contrib/pcoq - developed by Yves Bertot (INRIA, 1996-1999) -tactics/contrib/polynom - developed by Samuel Boutin (INRIA, 1996) - and Patrick Loiseleur (LRI, 1997-1999) -tactics/programs - developed by Jean-Christophe Filliatre (LRI, 1997-1999) -theories/REALS - developed by Micaela Mayero (INRIA, 1997-1999) -*************************************************************************** -INRIA refers to : - Institute National de la Recherche en Informatique et Automatique -CNRS refers to : - Centre National de la Recherche Scientifique -Paris 11 refers to : - Universite Paris Sud -ENS Lyon refers to : - Ecole Normale Superieure de Lyon -**************************************************************************** - - -Copyright: +The complete list of developpers and contributors can be found in /usr/share/doc/doc/CREDITS.gz -All files of the "Coq proof assistant" in directories or sub-directories of - src, tactics, theories, tools -are distributed under the terms of the GNU Lesser General Public License -Version 2.1. +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 diff --git a/distrib/debian/docs b/distrib/debian/docs index 9737d93a4..297170db8 100644 --- a/distrib/debian/docs +++ b/distrib/debian/docs @@ -1,2 +1,2 @@ -INSTALL README +CREDITS diff --git a/distrib/debian/rules b/distrib/debian/rules index e8e3aaea6..0e5831069 100755 --- a/distrib/debian/rules +++ b/distrib/debian/rules @@ -21,7 +21,7 @@ build-stamp: dh_testdir # Add here commands to compile the package. - $(MAKE) world + $(MAKE) world || (echo ERROR: trying to build in bytecode && echo "OPT=byte" >> config/Makefile && $(MAKE) world) #/usr/bin/docbook-to-man debian/coq.sgml > coq.1 touch build-stamp @@ -69,7 +69,7 @@ binary-arch: build install # dh_undocumented dh_installchangelogs CHANGES dh_link - dh_strip +# dh_strip dh_compress dh_fixperms # dh_makeshlibs |