*** empty log message ***

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

5 files changed, 101 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index 354936e9ee..b77b87dee7 100644
--- a/Makefile
+++ b/Makefile
@@ -59,7 +59,7 @@ CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
 COQINCLUDES=          # coqtop includes itself the needed paths
 GLOB=   # is "-dump-glob file" when making the doc
 
-BOOTCOQTOP=$(COQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB)
+BOOTCOQTOP=$(BESTCOQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB)
 
 ###########################################################################
 # Objects files 
@@ -247,11 +247,12 @@ BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
 COQTOP=bin/coqtop$(EXE)
 COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE)
 
+COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
+             $(COQINTERFACE) 
 
-world:: binaries states theories contrib tools
+coqbinaries:: ${COQBINARIES}
 
-binaries:: $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
-             $(COQINTERFACE) 
+world: coqbinaries states theories contrib tools
 
 $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX)
 	$(COQMKTOP) -opt $(MLINCLUDES) -o $@
@@ -527,10 +528,10 @@ INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc
 FOURIERVO = contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
 
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
-	$(COQTOP) -boot -byte $(COQINCLUDES) -compile $*
+	$(BESTCOQTOP) -boot -byte  $(COQINCLUDES) -compile $*
 
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
-	$(COQTOP) -boot -byte $(COQINCLUDES) -compile $*
+	$(BESTCOQTOP) -boot -byte  $(COQINCLUDES) -compile $*
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(CORRECTNESSVO)\
@@ -897,10 +898,12 @@ depend: beforedepend
 	$(MAKE) -f Makefile.dep $(ML4FILESML)
 # 3. We compute the dependencies inside the .ml files using ocamldep
 	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend
-# 4. We express dependencies of .cmo files w.r.t their grammars
+# 4. We express dependencies of .cmo and .cmx files w.r.t their grammars
 	for f in $(ML4FILES); do \
 	  printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \
 	  echo `$(CAMLP4DEPS) $$f` >> .depend; \
+	  printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \
+	  echo `$(CAMLP4DEPS) $$f` >> .depend; \
 	done
 # 5. Finally, we erase the generated .ml files
 	rm -f $(ML4FILESML)
diff --git a/distrib/Makefile b/distrib/Makefile
index 30bbc830e1..e7f16f0c19 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -23,7 +23,7 @@ RPM=${RAWRPM} ${RPMBUILDROOTOPT} --rcfile rpmrc
 FTPDIR=/net/pauillac/infosystems/ftp/coq/coq
 WWWDIR=/net/pauillac/infosystems/www/coq
 
-COQDEBPACKAGE=coq_${VERSION}-${RELEASENUM}_i386.deb
+COQDEBPACKAGE=coq_${VERSION}-${DEBRELEASENUM}_i386.deb
 
 COQPACKAGE=coq-${VERSION}
 COQRPMPACKAGE=coq-${VERSION}-${RELEASENUM}
@@ -311,12 +311,18 @@ ${COQDEBORIG}.tar.gz: ${COQPACKAGE}.tar.gz
 	tar czf ${COQDEBORIG}.tar.gz ${COQDEBORIG}	
 	rm -rf ${COQDEBORIG}
 
-deb: ${COQDEBORIG}.tar.gz ${COQPACKAGE}.tar.gz
+prep-deb: ${COQDEBORIG}.tar.gz ${COQPACKAGE}.tar.gz
 	rm -rf deb_build
 	mkdir -p deb_build
 	cd deb_build ; cp ../${COQDEBORIG}.tar.gz .
 	cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz
 	cp -a debian deb_build/${COQPACKAGE}
 	rm -rf deb_build/${COQPACKAGE}/debian/CVS
+
+deb: prep-deb
 	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee ../../deb.log
 	lintian deb_build/${COQDEBCHANGES} || true
+
+deb-sign: prep-deb
+	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot 2>&1 | tee ../../deb.log
+	lintian deb_build/${COQDEBCHANGES} || true
diff --git a/distrib/debian/changelog b/distrib/debian/changelog
index 42dc8fa86e..501b6e349f 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 ca65702947..4978041164 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 3c1a892639..72835d099e 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