- fixed the Assert_failure error in kernel/modops

- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
  the CVS working dir)


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

1 files changed, 391 insertions, 323 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 869130f6df..79dcdae715 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -1,38 +1,25 @@
 # Building the different files of the coq distribution
 
+# Rk: parameterized targets are not accepted on DEC boxes...
+
+# config.distrib defines: VERSION, PREVIOUSVERSION, DISTRIBDIR,
+# CVSMODULE, CVSTAG, RELEASENUM and ARCH 
 sinclude config.distrib
 LOCALARCH=`uname -m`
 SYSTEM=`uname -s`
 
-ARCHBUILDROOT=$(DISTRIBDIR)/${ARCH}
-RPMTOPDIR=$(DISTRIBDIR)/redhat
-RPMTMPPATHDIR=$(DISTRIBDIR)/redhat/admin
-
-# Parce que le chemin d'installation est cablé en dur dans coqtop, on ne
-# peut pas construire les rpm ailleurs que dans / et donc on doit être root
-#RPMBUILDROOTOPT=
-RPMBUILDROOT=$(DISTRIBDIR)/rpmbuildroot
-RPMBUILDROOTOPT=--buildroot ${RPMBUILDROOT}
-
-# rpm versions 2 and 3: replace rpmbuild by rpm 
-RAWRPM=rpmbuild
-
-RPMVERSION=`${RAWRPM} --version | sed -e "s/RPM version \(.\).*/\1/"`
-RPM=${RAWRPM} ${RPMBUILDROOTOPT} --rcfile rpmrc
+BUILDTARGET=world
+INSTTARGET=install
+MAKECOQ=make
 
+# We assume we are not on pauillac, so we use ssh and scp
+SERVER=pauillac.inria.fr
+CP=scp -p
+SERVEREXEC=ssh $(SERVER) sh -c
 FTPDIR=/net/pauillac/infosystems/ftp/coq/coq
-WWWDIR=/net/pauillac/infosystems/www/coq
-
-COQDEBPACKAGE=coq_${VERSION}-${DEBRELEASENUM}_i386.deb
-
-COQPACKAGE=coq-${VERSION}
-COQRPMPACKAGE=coq-${VERSION}-${RELEASENUM}
-COQDEBPACKAGE=coq_${VERSION}-${RELEASENUM}_i386.deb
-COQDEBCHANGES=coq_${VERSION}-${RELEASENUM}_*.changes
-COQDEBORIG=coq_${VERSION}.orig
+#WWWDIR=/net/pauillac/infosystems/www/coq
 
-COQIDERPMPACKAGE=coqide-${VERSION}-${RELEASENUM}
-COQIDEDEBPACKAGE=coqide_${VERSION}-${RELEASENUM}_i386.deb
+FTPVDIR=$(SERVER):$(FTPDIR)/V$(VERSION)
 
 ######################
 
@@ -40,345 +27,337 @@ noarguments:
 	@echo Please use either
 	@echo "make tag          to tag the current archive with the release number"
 	@echo "make tar-gz       to build a tar.gz of sources"
+	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
 	@echo "make rpm          to prepare a src.rpm and a rpm for the current arch"
 	@echo "make arch-rpm     to prepare a rpm for the current arch from the src.rpm"
-	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
-	@echo "make contrib-tag    to tag the current contrib state with the release number"
-	@echo "make contrib-tar-gz to build a tar.gz of contrib sources"
-	@echo "make ftp-install  to prepare the ftp repository and copy the packages done"
+	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
+	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
+	@echo "make deb          to build a debian package"
+	@echo "make win          to build a windows package"
+	@echo "make macosx       to build a MacOS-X package on a disk image"
+	@echo "make contrib-tag     to tag the current contrib state with the release number"
+	@echo "make contrib-tar-gz  to build a tar.gz of contrib sources"
+	@echo "make ftp-install     to prepare the ftp repository and copy the packages done"
 	@echo "make tar-gz-ftp-install         |add the corresponding"
 	@echo "make src-rpm-ftp-install        |packages to the ftp"
 	@echo "make arch-rpm-ftp-install       |repository supposed"
 	@echo "make arch-tar-gz-ftp-install    |to be already"
 	@echo "make contrib-ftp-install	       |prepared"
-	@echo "make deb		 to build a debian package"
-	@echo "make win		 to build a windows package"
-	@echo "make macosx	 to build a MacOS-X package on a disk image"
-	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
-	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
+	@echo
+	@echo "make clean        to remove temporary files"
+	@echo "make cleanall     also removes built packages" 
 
 ################## Main targets
 
-distrib: tag export tar-gz
-rpm: src-rpm arch-rpm
-ide-rpm: ide-src-rpm ide-arch-rpm
+COQPACKAGE=coq-$(VERSION)
 
-#################
-tag:
-	echo -n "Tagging the archive with version number $(DASHEDVERSION)...";\
-	cvs rtag -F $(DASHEDVERSION) $(MAJORVERSION)
+distrib: tag tar-gz
+
+###################################################################
+# Tagging the archive
+#
 
-export:
+tag:
+	echo -n "Tagging the archive with version number $(CVSTAG)...";\
+	cvs rtag -F $(CVSTAG) $(CVSMODULE)
+
+
+## Use make LOCAL=1 to build packages from working directory...
+ifeq ($(LOCAL),1)
+# export sources of the current work directory
+WORKDIR=..
+$(COQPACKAGE):
+	@echo "Copying sources from work directory"
+	@- rm -rf $(COQPACKAGE)
+	mkdir $(COQPACKAGE)
+	cd $(WORKDIR) ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` $(DISTRIBDIR)/$(COQPACKAGE)/
+	cd $(COQPACKAGE)/ ; $(MAKECOQ) clean; \
+	  rm -fr CVS */CVS */*/CVS */*/*/CVS */*/*/*/CVS
+	find $(COQPACKAGE) -name CVS -type d -exec rm -fr {} \;
+else
+# export a fresh copy of the tagged CVS version
+$(COQPACKAGE):
 	@echo -n Exporting a fresh copy of the archive...
-	@- rm -rf ${COQPACKAGE}
-	@cvs export -d $(COQPACKAGE) -r $(DASHEDVERSION) $(MAJORVERSION)
+	@- rm -rf $(COQPACKAGE)
+	@cvs export -d $(COQPACKAGE) -r $(CVSTAG) $(CVSMODULE)
 	@echo done
-
-export-from-local:
-	@- rm -rf ${COQPACKAGE}
-	mkdir ${COQPACKAGE}
-	cd .. ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` distrib/${COQPACKAGE}/
-	cd ${COQPACKAGE}/ ; $(MAKE) clean
-
-tar-gz: 
-	@echo -n Removing the maintenance files and doc...
-#	@rm -rf ${COQPACKAGE}/doc     # doc is implementation doc
-	@rm -rf ${COQPACKAGE}/distrib
-	@rm -rf ${COQPACKAGE}/KNOWN-BUGS
-	@rm -rf ${COQPACKAGE}/{TODO,ANNONCE,PROBLEMES}
-	@rm -rf ${COQPACKAGE}/theories/Num
-	@rm -rf ${COQPACKAGE}/contrib/graphs
-	@rm -rf ${COQPACKAGE}/doc/newsyntax.tex 
-	@rm -f ${COQPACKAGE}/make.result
-	@rm -rf ${COQPACKAGE}/test-suite/parser   # tests pcoq
-	@find ${COQPACKAGE} -name ".cvsignore" -exec rm {} \;
+endif
+
+###################################################################
+# .tar.gz packages (sources, binaries)
+#
+
+TARGZ=$(COQPACKAGE).tar.gz
+ARCHTAR=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+ARCHTARGZ=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz
+
+tar-gz:
+	rm -f $(TARGZ)
+	$(MAKE) $(TARGZ)
+
+$(TARGZ): $(COQPACKAGE)
+	@rm -rf $(COQPACKAGE)/doc     # doc is implementation doc
+	@rm -rf $(COQPACKAGE)/distrib
+	@rm -rf $(COQPACKAGE)/KNOWN-BUGS
+	@rm -rf $(COQPACKAGE)/{TODO,ANNONCE,PROBLEMES}
+	@rm -rf $(COQPACKAGE)/theories/Num
+	@rm -rf $(COQPACKAGE)/contrib/graphs
+	@rm -rf $(COQPACKAGE)/doc/newsyntax.tex 
+	@rm -f $(COQPACKAGE)/make.result
+	@rm -rf $(COQPACKAGE)/test-suite/parser   # tests pcoq
+	@find $(COQPACKAGE) -name ".cvsignore" -exec rm {} \;
 	@echo done
 	@echo -n Building the tar.gz source package
-	@tar cvf ${COQPACKAGE}.tar ${COQPACKAGE}
-	@gzip --best --force ${COQPACKAGE}.tar
+	@tar cvf $(COQPACKAGE).tar $(COQPACKAGE)
+	@gzip --best --force $(COQPACKAGE).tar
+	@chmod g+w $(TARGZ)
 	@echo done
 	@echo Checking release parameters
 	./check-list
 	@echo done
 
-src-rpm: ${COQRPMPACKAGE}.src.rpm
-arch-rpm: ${COQRPMPACKAGE}.${ARCH}.rpm
-
-ide-src-rpm: ${COQIDERPMPACKAGE}.src.rpm
-ide-arch-rpm: ${COQIDERPMPACKAGE}.${ARCH}.rpm
-
 test:
-	cp ${COQPACKAGE}.tar.gz tmp.tar.gz
-	gunzip tmp.tar.gz
-	@echo Trying "make world check"
-	- rm -rf ${COQPACKAGE}
+	- rm -rf $(COQPACKAGE)
+	gunzip -c $(TARGZ) > tmp.tar
 	tar xf tmp.tar
-	(cd ${COQPACKAGE};\
-	./configure -local -opt -emacs emacs;\
-	make world check >& log.world;\
-	if [ $$? = 0 ];\
-	then echo '"make world check" succeeded';\
-	else echo '"make world check" failed'; exit 1;\
-	fi)
-	rm tmp.tar
+	rm -f tmp.tar
+	@echo Trying "$(MAKECOQ) $(BUILDTARGET) check"
+	(cd $(COQPACKAGE);\
+	 ./configure -local -opt -emacs emacs;\
+	 $(MAKECOQ) world check >& test.log;\
+	 if [ $$? = 0 ];\
+	 then echo '"$(MAKECOQ) $(BUILDTARGET) check" succeeded';\
+	 else echo '"$(MAKECOQ) $(BUILDTARGET) check" failed'; exit 1;\
+	 fi)
 	@echo "Compilation succeeded"
 
-release-bin:
-	@echo
-	@echo "***************"
-	@echo "   attention   "
-	@echo "***************"
-	@echo
-	@echo "   \"make release-bin\" suppose que vous venez de compiler"
-	@echo "   ET D'INSTALLER Coq. Tapez <Ctrl-C> pour abandonner"
-	@echo "   et <Return> pour continuer."
-	@echo
-	@read
-	tar -cvf $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar --files-from $(COQLIB)/COQFILES
-	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
-
-arch-tar-gz-final:
-	(cd ${ARCHBUILDROOT}/buildroot;\
-	tar -cvf ${DISTRIBDIR}/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
-	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+# where binaries are compiled
+ARCHBUILDROOT=$(DISTRIBDIR)/tar-$(ARCH)
+ARCHINSTALL=$(ARCHBUILDROOT)/buildroot
 
 arch-tar-gz:
 	$(MAKE) arch-image
 	$(MAKE) arch-tar-gz-final
 
-arch-image: ${COQPACKAGE}.tar.gz
-	@echo "Building $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz to be installed in /usr/local/"
-	@echo "Warning: leading / is removed"
-	- mkdir -p ${ARCHBUILDROOT}
-	(cd ${ARCHBUILDROOT};\
-	rm -rf ${COQPACKAGE} || true;\
-	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
-	cd ${COQPACKAGE};\
-	./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all -coqide no;\
-	make world check;\
-	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
-	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install)
-
-win: ${COQPACKAGE}.tar.gz
-	@echo "Building $(COQPACKAGE)-Win.zip to be installed in \coq\bin"
+arch-image: $(TARGZ)
+	@echo "Building $(ARCHTARGZ) to be installed in /usr/local/"
 	@echo "Warning: leading / is removed"
-	- mkdir -p ${ARCHBUILDROOT}
-	(cd ${ARCHBUILDROOT};\
-	rm -rf ${COQPACKAGE} || true;\
-	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
-	cd ${COQPACKAGE};\
-	./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
-	make world;\
-	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
-	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install;\
-	cd ${ARCHBUILDROOT}/buildroot;\
-	mv ../$(COQPACKAGE)/INSTALL.win .;\
-	zip -A -r $(COQPACKAGE)-win.zip *;\
-	mv $(COQPACKAGE)-Win.zip ../..)
-
-rpm-dirs:
-	- mkdir ${RPMTOPDIR}
-	- mkdir ${RPMTOPDIR}/BUILD
-	- mkdir ${RPMTOPDIR}/RPMS
-	- mkdir ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/SPECS
-	- mkdir ${RPMTOPDIR}/SRPMS
-	- mkdir ${RPMTMPPATHDIR}
-	- mkdir ${RPMBUILDROOT}
-
-rpm-config: rpm-dirs
-	- rm rpmrc rpmmacros
-	(if [ "${RPMVERSION}" != "2" ];\
-	then\
-	echo %_topdir ${RPMTOPDIR} > rpmmacros;\
-	echo %_tmppath ${RPMTMPPATHDIR} >> rpmmacros;\
-	echo %_arch ${ARCH} >> rpmmacros;\
-	echo macrofiles:/usr/lib/rpm/macros:rpmmacros > rpmrc;\
-	else\
-	echo topdir: ${RPMTOPDIR} > rpmrc;\
-	echo tmppath: ${RPMTMPPATHDIR} >> rpmrc;\
-	fi)
+	@-rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
+	@mkdir -p $(ARCHBUILDROOT) $(ARCHINSTALL)
+	@echo Building binaries... (see arch-image.log)
+	(cd $(ARCHBUILDROOT);\
+	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
+	 cd $(COQPACKAGE);\
+	 ./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all -coqide no;\
+	 $(MAKECOQ) coq check;\
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
+	@echo " .... done"
 
-# Les cibles suivantes ne sont pas acceptées sur DEC (car paramétrées)
-
-${COQPACKAGE}.tar.gz:
-	${MAKE} export tar-gz
-
-# rpm 3.0 met dans LOCALARCH mais rpm 2.5 dans ARCH...
-${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coq.spec
-	${MAKE} rpm-config
-	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
-	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- rm -fr $(RPMBUILDROOT)
-	${RPM} -ba RH/coq.spec
-	mv ${RPMTOPDIR}/SRPMS/${COQRPMPACKAGE}.src.rpm .
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+arch-tar-gz-final:
+	(cd $(ARCHBUILDROOT)/buildroot;\
+	 tar -cvf $(DISTRIBDIR)/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
+	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+	chmod g+w $(ARCHTARGZ)
 
-${COQIDERPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coqide.spec
-	${MAKE} rpm-config
-	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
-	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- rm -fr $(RPMBUILDROOT)
-	${RPM} -ba RH/coqide.spec
-	mv ${RPMTOPDIR}/SRPMS/${COQIDERPMPACKAGE}.src.rpm .
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+clean::
+	rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
 
-# Sera déjà fait si le src.rpm vient d'être fait
-${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	#- rm -fr $(RPMBUILDROOT)
-	${RPM} --rebuild ${COQRPMPACKAGE}.src.rpm
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+cleanall::
+	rm -f $(COQPACKAGE) $(TARGZ) $(ARCHTARGZ) arch-image.log test.log
+
+###################################################################
+# RPM (Coq and CoqIde are separated)
+#
+
+rpm: src-rpm arch-rpm
+ide-rpm: ide-src-rpm ide-arch-rpm
+
+RPMTOPDIR=$(DISTRIBDIR)/RH/src
+RPMTMPPATHDIR=$(RPMTOPDIR)/admin
+RPMBUILDROOT=$(RPMTOPDIR)/install
 
-${COQIDERPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQIDERPMPACKAGE}.src.rpm
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	#- rm -fr $(RPMBUILDROOT)
-	${RPM} --rebuild ${COQIDERPMPACKAGE}.src.rpm
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
+# rpm versions 2 and 3: replace rpmbuild by rpm 
+RAWRPM=rpmbuild
+RPMVERSION=`$(RAWRPM) --version | sed -e "s/RPM version \(.\).*/\1/"`
+
+# option --target avoids problem with i386/i686
+RPM=$(RAWRPM) --buildroot $(RPMBUILDROOT) --target $(ARCH) --rcfile RH/rpmrc
+
+# rpm files
+COQRPMPACKAGE=coq-$(VERSION)-$(RELEASENUM)
+COQIDERPMPACKAGE=coqide-$(VERSION)-$(RELEASENUM)
+COQSRCRPM=$(COQRPMPACKAGE).src.rpm
+COQRPM=$(COQRPMPACKAGE).$(ARCH).rpm
+COQIDESRCRPM=$(COQIDERPMPACKAGE).src.rpm
+COQIDERPM=$(COQIDERPMPACKAGE).$(ARCH).rpm
+
+RPMLOG=$(DISTRIBDIR)/RH/rpm.log
+RPMFILESLOG=$(DISTRIBDIR)/RH/coqfiles.log
+
+src-rpm: $(COQSRCRPM)
+arch-rpm: $(COQRPM)
+
+ide-src-rpm: $(COQIDESRCRPM)
+ide-arch-rpm: $(COQIDERPM)
+
+$(RPMTOPDIR):
+	@mkdir -p $(RPMTOPDIR)/BUILD
+	@mkdir -p $(RPMTOPDIR)/RPMS
+	@mkdir -p $(RPMTOPDIR)/SOURCES
+	@mkdir -p $(RPMTOPDIR)/SPECS
+	@mkdir -p $(RPMTOPDIR)/SRPMS
+	@mkdir -p $(RPMTMPPATHDIR)
+	@mkdir -p $(RPMTOPDIR)/RPMS/$(ARCH)
+
+RH/rpmrc: config.distrib
+	(if [ "$(RPMVERSION)" != "2" ];\
+	then\
+	echo %_topdir $(RPMTOPDIR) > RH/rpmmacros;\
+	echo %_tmppath $(RPMTMPPATHDIR) >> RH/rpmmacros;\
+	echo %_arch $(ARCH) >> RH/rpmmacros;\
+	echo macrofiles:/usr/lib/rpm/macros:RH/rpmmacros > RH/rpmrc;\
+	else\
+	echo topdir: $(RPMTOPDIR) > RH/rpmrc;\
+	echo tmppath: $(RPMTMPPATHDIR) >> RH/rpmrc;\
 	fi)
 
-RH/coq.list: ${COQPACKAGE}.tar.gz Makefile config.distrib
-	rm -rf RH/${COQPACKAGE} RH/build
-	cd RH ; tar xzf ../${COQPACKAGE}.tar.gz
-	cd RH/${COQPACKAGE} ; sh ../do_build
-	cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install-coq
+$(COQSRCRPM): $(RPMTOPDIR) RH/coq.spec RH/coq.list $(TARGZ) RH/rpmrc
+	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
+	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
+	cp -f RH/coq.list $(RPMTOPDIR)
+	$(RPM) -bs RH/coq.spec
+	mv $(RPMTOPDIR)/SRPMS/$(COQSRCRPM) .
+	chmod g+w $(COQSRCRPM)
+	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coq.list
+
+$(COQRPM): $(COQSRCRPM)
+	@-rm -fr $(RPMBUILDROOT)
+	@mkdir -p $(RPMBUILDROOT)
+	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
+	cp -f RH/coq.list $(RPMTOPDIR)
+	$(RPM) --rebuild $(COQSRCRPM)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQRPM) .
+	chmod g+w $(COQRPM)
+	rm -f $(RPMTOPDIR)/coq.list
+
+$(COQIDESRCRPM): $(RPMTOPDIR) RH/coqide.spec $(TARGZ) RH/rpmrc
+	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
+	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
+	$(RPM) -bs RH/coqide.spec
+	mv $(RPMTOPDIR)/SRPMS/$(COQIDESRCRPM) .
+	chmod g+w $(COQIDESRCRPM)
+	rm -fr $(RPMTOPDIR)/SOURCES/*
+
+$(COQIDERPM): $(COQIDESRCRPM)
+	@-rm -fr $(RPMBUILDROOT)
+	@mkdir -p $(RPMBUILDROOT)
+	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
+	$(RPM) --rebuild $(COQIDESRCRPM)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQIDERPM) .
+	chmod g+w $(COQIDERPM)
+
+RH/coq.list: $(TARGZ) config.distrib
+	rm -rf RH/$(COQPACKAGE) RH/build
+	cd RH ; tar xzf ../$(TARGZ)
+	@echo "Building coq files list... (see RH/coqfiles.log)"
+	cd RH/$(COQPACKAGE) ; sh ../do_build > $(RPMFILESLOG)
+	cd RH/$(COQPACKAGE) ; $(MAKECOQ) COQINSTALLPREFIX=$(DISTRIBDIR)/RH/build install-coq >> $(RPMFILESLOG)
+	@echo " ... done"
 	echo "# This file has been generated" > RH/coq.list
 	echo "# Do not edit" >>RH/coq.list
 	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g' >> ../coq.list
+	rm -rf RH/$(COQPACKAGE) RH/build
 
-RH/coq.spec: RH/coq.list RH/coq.spec.tpl
-	echo "# This file has been generated from RH/coq.spec.tpl" > RH/coq.spec
-	echo "# Do not edit" >> RH/coq.spec
-	cd RH ; m4 -P coq.spec.tpl >> coq.spec
+clean::
+	rm -fr $(RPMTOPDIR) RH/coq.list RH/$(COQPACKAGE) RH/build RH/rpmmacros RH/rpmrc
 
-##########
-contrib-tag:
-	echo -n "Tagging the contrib with version number $(DASHEDVERSION)...";\
-	cvs rtag -F $(DASHEDVERSION) contrib
-	@echo done
+cleanall::
+	rm -f $(COQSRCRPM) $(COQRPM) $(COQIDESRCRPM) $(COQIDERPM) $(RPMLOG) $(RPMFILESLOG)
 
-contrib-tar-gz:
-	- rm -rf contrib-${VERSION}
-	@echo -n Exporting a fresh copy of the contribs...
-	cvs export -d contrib-${VERSION} -r $(DASHEDVERSION) contrib
-	@echo -n Removing the maintenance files ...
-	@rm -rf contrib-${VERSION}/*/*/bench.log
-	@rm -rf contrib-${VERSION}/Lyon/PROGRAMS
-	@find contrib-${VERSION} -name ".cvsignore" -exec rm {} \;
-	@echo done
-	- rm contrib-${VERSION}.tar.gz
-	@echo -n Building the tar.gz contrib package
-	@tar cvf contrib-${VERSION}.tar contrib-${VERSION}
-	@gzip --best contrib-${VERSION}.tar
-	@echo done
+###################################################################
+# Zip for Windows (package does not contain coqide)
+#
 
-##########
-patch:
-	@echo ******** ATTENTION, plante sur pc-linux, essayez pauillac ******
-	cp $(FTPDIR)/V$(PREVIOUSVERSION)/coq-$(PREVIOUSVERSION).tar.gz .
-	rm -rf coq-$(PREVIOUSVERSION)
-	gunzip -c coq-$(PREVIOUSVERSION).tar.gz | tar x
-	rm -rf ${COQPACKAGE}
-	gunzip -c ${COQPACKAGE}.tar.gz | tar x
-	diff -rc coq-$(PREVIOUSVERSION) ${COQPACKAGE} > patch-${VERSION}-$(PREVIOUSVERSION)
-	gzip --best patch-${VERSION}-$(PREVIOUSVERSION)
+COQWINZIP=$(COQPACKAGE)-Win.zip
+WINBUILDROOT=$(DISTRIBDIR)/winbuildroot
+WININSTALL=$(DISTRIBDIR)/wininstallroot
 
-##########
-clean:
-	- rm -rf ${COQPACKAGE} ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} RH/build RH/${COQPACKAGE}
 
-cleanall:
-	- rm -rf ${COQPACKAGE}* ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} 
+win: $(COQWINZIP)
 
-########## Installation in the ftp repository
+$(COQWINZIP): $(TARGZ)
+	@echo "Building $(COQWINZIP) to be installed in \coq\bin"
+	@echo "Warning: leading / is removed"
+	@-rm -fr $(WINBUILDROOT) $(WININSTALL)
+	@-mkdir -p $(WINBUILDROOT) $(WININSTALL)
+	@echo "Compiling and installing coq... (see win.log)"
+	(cd $(WINBUILDROOT);\
+	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
+	 cd $(COQPACKAGE);\
+	 ./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
+	 $(MAKECOQ) coq;\
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(WININSTALL) install-coq) > win.log
+	mv $(WINBUILDROOT)/$(COQPACKAGE)/INSTALL.win $(WININSTALL)
+	cd $(WININSTALL); zip -A -r $(DISTRIBDIR)/$(COQWINZIP) *
+
+clean::
+	rm -fr $(WINBUILDROOT) $(WININSTALL)
+
+cleanall::
+	rm -f $(COQWINZIP) win.log
+
+###################################################################
+# Debian
+#
+
+COQDEBPACKAGE=coq_$(VERSION)-$(RELEASENUM)_i386.deb
+COQDEBCHANGES=coq_$(VERSION)-$(RELEASENUM)_*.changes
+COQDEBORIG=coq_$(VERSION).orig
+COQDEBTARGZ=$(COQDEBORIG).tar.gz
+COQIDEDEBPACKAGE=coqide_$(VERSION)-$(RELEASENUM)_i386.deb
+
+DEBIANBUILD=$(DISTRIBDIR)/deb/build
+DEBIANLOG=$(DISTRIBDIR)/deb/deb.log
+LINTIANLOG=$(DISTRIBDIR)/deb/lintian.log
 
-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}/CHANGES ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README.win ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README.macosx ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}.tar.gz
-	cp ${COQPACKAGE}-*.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}-*.tar.gz
-	cp ${COQRPMPACKAGE}.*.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.*.rpm
-
-# prep-ftp-install: $(FTPDIR)/V${VERSION}
-prep-ftp-install: 
-	- mkdir $(FTPDIR)/V${VERSION}
-	- chmod g+w ${FTPDIR}/V${VERSION}
+deb: prep-deb
+	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
+	 dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee $(DEBIANLOG)
+	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
+
+$(COQDEBTARGZ): $(TARGZ)
+	tar xzf $(TARGZ)
+	mv $(COQPACKAGE) $(COQDEBORIG)
+	tar czf $(COQDEBTARGZ) $(COQDEBORIG)	
+	rm -rf $(COQDEBORIG)
+
+prep-deb: $(COQDEBTARGZ) $(TARGZ)
+	@rm -rf $(DEBIANBUILD)
+	@mkdir -p $(DEBIANBUILD)
+	cp $(COQDEBTARGZ) $(DEBIANBUILD)
+	cd $(DEBIANBUILD) ; tar xzf $(DISTRIBDIR)/$(TARGZ)
+	cp -a debian $(DEBIANBUILD)/$(COQPACKAGE)
+	rm -rf $(DEBIANBUILD)/$(COQPACKAGE)/debian/CVS
+	date > prep-deb
 
-final-ftp-install:
-	(cd $(FTPDIR); rm -f current;ln -sf V${VERSION} current)
+deb-sign: prep-deb
+	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
+	 dpkg-buildpackage -rfakeroot 2>&1 | tee $(DEBIANLOG)
+	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
 
-tar-gz-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}.tar.gz
 
-src-rpm-ftp-install: prep-ftp-install
-	cp ${COQRPMPACKAGE}.src.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.src.rpm
+clean::
+	rm -fr $(DEBIANBUILD)
 
-arch-rpm-ftp-install: prep-ftp-install
-	cp ${COQRPMPACKAGE}.${ARCH}.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.${ARCH}.rpm
+cleanall::
+	rm -f $(DEBIANLOG) $(LINTIANLOG)
 
-arch-tar-gz-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}-$(SYSTEM)-$(ARCH).tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}-$(SYSTEM)-$(ARCH).tar.gz
+###################################################################
+# Mac OS X
+#
 
-contrib-ftp-install: prep-ftp-install
-	cp contrib-${VERSION}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/contrib-${VERSION}.tar.gz
-
-patch-ftp-install: prep-ftp-install
-	cp patch-${VERSION}-$(PREVIOUSVERSION).gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz
-
-${COQDEBORIG}.tar.gz: ${COQPACKAGE}.tar.gz
-	tar xzf ${COQPACKAGE}.tar.gz
-	mv ${COQPACKAGE} ${COQDEBORIG}
-	tar czf ${COQDEBORIG}.tar.gz ${COQDEBORIG}	
-	rm -rf ${COQDEBORIG}
-
-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
-	date > prep-deb
-
-deb: prep-deb
-	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee ../../deb.log
-	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
-
-deb-sign: prep-deb
-	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot 2>&1 | tee ../../deb.log
-	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
+MACOSXPKG=coq-$(VERSION).pkg
+MACOSXDMG=coq-$(VERSION)-macosx.dmg
 
 macosx:
 	# Builds the /usr/local/bin image
@@ -389,29 +368,118 @@ macosx:
 
 macosx-pkg:
 	# Builds the info file
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/coq.info.template > MacOS-X/coq-${VERSION}.info
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/coq.info.template > MacOS-X/coq-$(VERSION).info
 	# Builds the resources files
 	rm -rf MacOS-X/Resources
 	mkdir MacOS-X/Resources
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/Licence.rtf.template > MacOS-X/Resources/License.rtf
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/Welcome.rtf.template > MacOS-X/Resources/Welcome.rtf
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Licence.rtf.template > MacOS-X/Resources/License.rtf
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Welcome.rtf.template > MacOS-X/Resources/Welcome.rtf
 	cp MacOS-X/ReadMe.rtf.template MacOS-X/Resources/ReadMe.rtf
 	# Builds the pkg file
-	package MacOS-X/buildroot MacOS-X/coq-${VERSION}.info -r MacOS-X/Resources
+	package MacOS-X/buildroot MacOS-X/coq-$(VERSION).info -r MacOS-X/Resources
+
 
 macosx-dmg:
-	rm -f coq-${VERSION}-macosx.dmg
+	rm -f $(MACOSXDMG)
 	# We successively :
 	# - create the dmg file
 	# - bind it to a device /dev/diskXs2 (name)
 	# - create the file system and name it "Coq X.X"
 	# - unbind the device to mount the image on /Volumes
 	# - copy the package
-	(export size=`du -s coq-${VERSION}.pkg | cut -dc -f 1`;\
-	hdiutil create -sectors `expr $$size + 1000` coq-${VERSION}-macosx.dmg;\
-	export name=`hdid -nomount coq-${VERSION}-macosx.dmg | tail -1 | cut -d" " -f 1`;\
-	newfs_hfs -v "Coq ${VERSION}" $$name;\
-	hdiutil eject $$name; hdid coq-${VERSION}-macosx.dmg;\
-	mkdir "/Volumes/Coq ${VERSION}/coq-${VERSION}.pkg";\
-	ditto -rsrcFork -v coq-${VERSION}.pkg "/Volumes/Coq ${VERSION}/coq-${VERSION}.pkg")
+	(export size=`du -s $(MACOSXPKG) | cut -dc -f 1`;\
+	hdiutil create -sectors `expr $$size + 1000` $(MACOSXDMG);\
+	export name=`hdid -nomount $(MACOSXDMG) | tail -1 | cut -d" " -f 1`;\
+	newfs_hfs -v "Coq $(VERSION)" $$name;\
+	hdiutil eject $$name; hdid $(MACOSXDMG);\
+	mkdir "/Volumes/Coq $(VERSION)/coq-$(VERSION).pkg";\
+	ditto -rsrcFork -v $(MACOSXPKG) "/Volumes/Coq $(VERSION)/$(MACOSXPKG)")
+
+
+###################################################################
+# contribs and patches
+#
+contrib-tag:
+	echo -n "Tagging the contrib with version number $(CVSTAG)...";\
+	cvs rtag -F $(CVSTAG) contrib
+	@echo done
+
+contrib-tar-gz:
+	- rm -rf contrib-$(VERSION)
+	@echo -n Exporting a fresh copy of the contribs...
+	cvs export -d contrib-$(VERSION) -r $(CVSTAG) contrib
+	@echo -n Removing the maintenance files ...
+	@rm -rf contrib-$(VERSION)/*/*/bench.log
+	@rm -rf contrib-$(VERSION)/Lyon/PROGRAMS
+	@find contrib-$(VERSION) -name ".cvsignore" -exec rm {} \;
+	@echo done
+	- rm contrib-$(VERSION).tar.gz
+	@echo -n Building the tar.gz contrib package
+	@tar cvf contrib-$(VERSION).tar contrib-$(VERSION)
+	@gzip --best contrib-$(VERSION).tar
+	@echo done
+
+
+patch:
+	@echo ******** ATTENTION, plante sur pc-linux, essayez pauillac ******
+	$(CP) $(FTPDIR)/V$(PREVIOUSVERSION)/coq-$(PREVIOUSVERSION).tar.gz .
+	rm -rf coq-$(PREVIOUSVERSION)
+	gunzip -c coq-$(PREVIOUSVERSION).tar.gz | tar x
+	rm -rf $(COQPACKAGE)
+	gunzip -c $(TARGZ) | tar x
+	diff -rc coq-$(PREVIOUSVERSION) $(COQPACKAGE) > patch-$(VERSION)-$(PREVIOUSVERSION)
+	gzip --best patch-$(VERSION)-$(PREVIOUSVERSION)
+
+###################################################################
+# Installation in the ftp repository
+#
+
+ftp-install: prep-ftp-install
+	$(CP) $(COQPACKAGE)/CHANGES $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README.win $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README.macosx $(FTVPDIR)/
+	$(CP) $(TARGZ) $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)-*.tar.gz $(FTPVDIR)/
+	$(CP) $(COQRPMPACKAGE).*.rpm $(FTPVDIR)/
+
+# prep-ftp-install: $(FTPDIR)/V$(VERSION)
+prep-ftp-install: 
+	- $(SERVEREXEC) mkdir -m g+w $(FTPDIR)/V$(VERSION)
+
+final-ftp-install:
+	$(SERVEREXEC) "'(cd $(FTPDIR); rm -f current;ln -sf V$(VERSION) current)'"
+
+tar-gz-ftp-install: prep-ftp-install
+	chmod g+w $(TARGZ)
+	$(CP) $(TARGZ) $(FTPVDIR)/
+
+src-rpm-ftp-install: prep-ftp-install
+	chmod g+w $(COQSRCRPM)
+	$(CP) $(COQSRCRPM) $(FTPVDIR)/
+
+arch-rpm-ftp-install: prep-ftp-install
+	chmod g+w $(COQRPM)
+	$(CP) $(COQRPM) $(FTPVDIR)/
+
+arch-tar-gz-ftp-install: prep-ftp-install
+	chmod g+w $(ARCHTARGZ)
+	$(CP) $(ARCHTARGZ) $(FTPVDIR)/
+
+contrib-ftp-install: prep-ftp-install
+	chmod g+w contrib-$(VERSION).tar.gz
+	$(CP) contrib-$(VERSION).tar.gz $(FTPVDIR)/
+
+patch-ftp-install: prep-ftp-install
+	chmod g+w patch-$(VERSION)-$(PREVIOUSVERSION).gz
+	$(CP) patch-$(VERSION)-$(PREVIOUSVERSION).gz $(FTPVDIR)/
+
+###################################################################
+# Special targets
+#
+
+#clean::
+
+cleanall:: clean
+	rm -f config.distrib