*** empty log message ***

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

3 files changed, 83 insertions, 6 deletions

diff --git a/distrib/debian/changelog b/distrib/debian/changelog
index 42dc8fa86..501b6e349 100644
--- a/distrib/debian/changelog
+++ b/distrib/debian/changelog
@@ -1,3 +1,47 @@
+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).
diff --git a/distrib/debian/control b/distrib/debian/control
index ca6570294..497804116 100644
--- a/distrib/debian/control
+++ b/distrib/debian/control
@@ -3,12 +3,12 @@ Section: devel
 Priority: optional
 Maintainer: Judicaël Courant <Judicael.Courant@lri.fr>
 Standards-Version: 3.5.3
-Build-Depends: debhelper (>= 3), ocaml (>= 3.01), ocaml (>=3.04) | camlp4
+Build-Depends: debhelper (>= 3), timeout, ocaml (>= 3.04)
 
 Package: coq
 Architecture: any
 Depends: ${shlibs:Depends}
-Suggests: coq-doc, ocaml (>= 3.01-1), camlp4, cle
+Suggests: coq-doc, ocaml (>= 3.04), cle
 Recommends: coq-doc
 Description: a proof assistant for higher-order logic.
  Coq is a proof assistant for higher-order logic, which allows the
diff --git a/distrib/debian/rules b/distrib/debian/rules
index 3c1a89263..72835d099 100755
--- a/distrib/debian/rules
+++ b/distrib/debian/rules
@@ -2,16 +2,49 @@
 
 export DH_COMPAT=3
 
+COQPREF=$(CURDIR)/debian/coq
+ADDPREF=COQINSTALLPREFIX=${COQPREF}
+
+# in version 3.04, ocamlopt has several bugs: on some arches, it produces
+# executables that sometimes fail mysteriously or loop.
+# We use a workaround to detect this kind of situations:
+# - we try to make Coq with timeouts (TMAKE)
+# - once this is done, we check make succeeded (timeout does not
+# return the exit status of MAKE)
+#
+TMAKE=timeout 5300 ${MAKE}
+MAKEQ=${MAKE} -q
+
+CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq
+
 configure: configure-stamp
 configure-stamp:
 	dh_testdir
-	./configure --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq
+	./configure -opt ${CONFIGUREOPTS} || ./configure ${CONFIGUREOPTS}
+	# on powerpc, we refuse to use the ".opt" compilers
+	if [ `arch` = ppc ] ; then ./configure ${CONFIGUREOPTS} ; fi
 	touch configure-stamp
 
 build: configure-stamp build-stamp
 build-stamp:
 	dh_testdir
-	$(MAKE) world || (echo WARNING: NATIVE CODE COMPILATION FAILED && echo Trying to build coq in bytecode && echo "OPT=byte" >> config/Makefile && $(MAKE) world)
+	if grep -q BEST=opt config/Makefile; \
+	then (${TMAKE} bin/coqmktop bin/coqc bin/coqtop.byte \
+	      && ${MAKEQ} bin/coqmktop bin/coqc bin/coqtop.byte \
+	      && ${TMAKE} bin/coqtop.opt bin/coqtop \
+	      && ${MAKEQ} bin/coqtop.opt bin/coqtop \
+	      && ${TMAKE} states \
+	      && ${MAKEQ} states \
+	      && ${TMAKE} world \
+	      && ${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
 	touch build-stamp
 
 clean:
@@ -30,8 +63,8 @@ install: build
 	dh_clean -k
 	dh_installdirs
 
-	$(MAKE) install COQINSTALLPREFIX=$(CURDIR)/debian/coq
-	-strip -R .note -R .comment $(CURDIR)/debian/coq/usr/bin/coqtop.opt
+	$(MAKE) ${ADDPREF} install || $(MAKE) BEST=byte ${ADDPREF} install
+	-strip -R .note -R .comment ${COQPREF}/usr/bin/coqtop.opt
 
 # Build architecture-independent files here.
 binary-indep: build install