*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2288 85f007b7-540e-0410-9357-904b9bb8a0f7

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