- 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

4 files changed, 452 insertions, 372 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 869130f6d..79dcdae71 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
 
diff --git a/distrib/RELEASE b/distrib/RELEASE
index 0ef0b09fa..11b795db2 100644
--- a/distrib/RELEASE
+++ b/distrib/RELEASE
@@ -43,7 +43,7 @@ A1) VÉRIFICATIONS
 
   Dans le cas simple d'une recompilation sur une autre architecture,
 sauter A3. Sauter aussi A4 s'il est possible de mettre le fichier
-coq-6.2.5.tar.gz à la main dans distrib.
+coq-X.Y.Z.tar.gz à la main dans distrib.
 
 A2) CONFIGURATION DES PARAMETRES DE LA DISTRIBUTION
 
@@ -62,7 +62,8 @@ A3) ESTAMPILLAGE DE L'ARCHIVE
 
      make tag
 
-  pour poser le tag V6-2-5 à l'archive V6-2 (on suppose que le numéro de version donné dans configure.distrib est V6.2.5).
+  pour poser le tag V'X'-Y-Z à l'archive V'X' (on suppose que le numéro
+  de version donné dans configure.distrib est V'X'.Y.Z).
 
   La commande "make tag" peut être refaite plusieurs fois auquel cas
 l'ancienne marque est supprimée avant d'être remise à la nouvelle
@@ -74,7 +75,7 @@ l'archive faire "cvs tag -F V6-2-5 nom_du_fichier".
 
 A4) CREATION DU PACKAGE SOURCE
 
-  Créer le coq-6.2.5.tar.gz des sources à partir d'un extrait tout
+  Créer le coq-X.Y.Z.tar.gz des sources à partir d'un extrait tout
 frais (obtenu par cvs export) de l'archive avec
 
      make tar-gz
@@ -96,13 +97,13 @@ A5a) Création d'un package binaire tar.gz
       make arch-tar-gz
 
   dans le répertoire distrib sous l'architecture ARCH avec le système SYS
-crée un fichier coq-6.2.5-SYS-ARCH.tar.gz (ex : coq-6.2.5-alpha-OSF1.tar.gz).
+crée un fichier coq-X.Y.Z-SYS-ARCH.tar.gz (ex : coq-6.2.5-alpha-OSF1.tar.gz).
 
   Pour compiler sur plusieurs machines en parallèle, il faut des
 répertoires "distrib" distincts pour que les compilations ne se
 téléscopent pas. Sur une 2ème machine dans un autre répertoire
 "distrib", refaire "make tar-gz" en interrompant la check-list (ou
-simplement copier le coq-6.2.5.tar.gz déjà fait) puis "make arch-tar-gz".
+simplement copier le coq-X.Y.Z.tar.gz déjà fait) puis "make arch-tar-gz".
 
   Pour l'installation sous ftp voir A7.
 
@@ -114,7 +115,7 @@ A5b) Création du source rpm et du premier package rpm
      make rpm
 
   dans le répertoire distrib sous l'architecture ARCH crée un package
-source coq-6.2.5-1.src.rpm et un package binaire coq-6.2.5-1.ARCH.rpm
+source coq-X.Y.Z-1.src.rpm et un package binaire coq-X.Y.Z-1.ARCH.rpm
 (ex : coq-6.2.5-1.i386.rpm).
 
   Remarques : 1) Les packages Intel s'appellent i386 même si
@@ -133,7 +134,16 @@ A5c) Création d'un second package rpm à partir des sources rpm
 
   Pour l'installation sous ftp voir A7.
 
-A5d) Création du package debian
+A5d) Création d'un package coq-ide
+
+  Faire un
+
+     make rpm-ide
+
+  pour produire un package source coqide-X-Y-Z-1.src.rpm et un package
+  bianire coqide-X-Y-Z-1.ARCH.rpm.
+
+A5e) Création du package debian
 
   Faire un
 
@@ -144,7 +154,7 @@ A5d) Création du package debian
   binaire sur toutes les architectures : ce sera fait par les machines
   de Debian dès que le paquet source leur sera fourni.
 
-A5e) Création du package windows
+A5f) Création du package windows
 
   Habituellement fait sur jurancon.inria.fr, sous Windows NT, avec la
   version Win32 de ocaml (pas la version cygwin car elle produit un
@@ -160,7 +170,7 @@ A5e) Création du package windows
 
   Envoyer ensuite l'archive par ftp dans
 
-    pauillac:/net/pauillac/infosystems/ftp/coq/coq/V6.2.5
+    pauillac:/net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z
 
 A6) CREATION DU FICHIER DE PATCH (attention ne marche pas sur DEC je crois)
 
@@ -183,7 +193,7 @@ A7) INSTALLATION SOUS FTP
 
    make ftp-install # Avec les droits du groupe coq
 
-   - crée le dossier /net/pauillac/infosystems/ftp/coq/coq/V6.2.5, le
+   - crée le dossier /net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z, le
    lie symboliquement à /net/pauillac/infosystems/ftp/coq/coq/current.
 
    - installe sous ftp tous les fichiers tar.gz ou .rpm du répertoire
diff --git a/distrib/check-list b/distrib/check-list
index 8e277fef5..be39bc665 100755
--- a/distrib/check-list
+++ b/distrib/check-list
@@ -11,7 +11,7 @@ COQPACKAGE=coq-$VERSION
 CONFIGFILE=$COQPACKAGE/configure
 
 version=`grep "^VERSION=" $CONFIGFILE | sed -e 's/^VERSION=\(.*\)/\1/'`
-versionsi=`grep "^VERSIONSI=" $CONFIGFILE | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
+#versionsi=`grep "^VERSIONSI=" $CONFIGFILE | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
 coqdate=`grep "^DATE=" $CONFIGFILE | sed -e 's/^DATE=\(.*\)/\1/'`
 
 echo "According to the configure file of the archive to be released"
@@ -24,9 +24,9 @@ echo "Comparing datas with expected ones"
 if [ ! "$version" = "$VERSION" ]; then
 	 echo "Inconsistent version number";exit
 fi
-if [ ! "$versionsi" = "$VERSIONSI" ]; then
-	echo "Inconsistent SearchIsos version number";exit
-fi
+#if [ ! "$versionsi" = "$VERSIONSI" ]; then
+#	echo "Inconsistent SearchIsos version number";exit
+#fi
 if [ ! "$date" = "$DATE" ]; then
 	echo "Inconsistent date release";exit
 fi
@@ -75,8 +75,8 @@ echo -n " is that OK? "
 read a
 if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
 
-versionspec1=`grep "^Version: " ./RH/coq.spec.tpl | sed -e 's!^Version: \(.*\)!\1!'`
-versionspec2=`grep "^Source: " ./RH/coq.spec.tpl | sed -e 's!.*coq-\(.*\)\.tar\.gz.*!\1!'`
+versionspec1=`sed -n -e 's!^Version: \(.*\)!\1!p' ./RH/coq.spec`
+versionspec2=`sed -n -e 's!.*coq-\(.*\)\.tar\.gz.*!\1!' ./RH/coq.spec`
 if [ "$versionspec1" = "$version" -a "$versionspec2" = "$version" ];
 then echo "Version number in coq.spec seems OK ($versionspec1)";
 else
diff --git a/distrib/configure.distrib b/distrib/configure.distrib
index ac52c65b2..bd4faf442 100755
--- a/distrib/configure.distrib
+++ b/distrib/configure.distrib
@@ -6,12 +6,13 @@
 # 
 ####################################
 #
-#  Default values comes from ../configure which is probably consistent with the archive
+#  Default values comes from ../configure which is probably consistent
+#  with the archive
 #
 
-VERSION=`grep "^VERSION=" ../configure | sed -e 's/^VERSION=\(.*\)/\1/'`
-VERSIONSI=`grep "^VERSIONSI=" ../configure | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
-DATE=`grep "^DATE=" ../configure | sed -e 's/^DATE=\(.*\)/\1/'`
+VERSION=`sed -n -e 's/^VERSION=\(.*\)/\1/p' ../configure`
+#VERSIONSI=`sed -n -e 's/^VERSIONSI=\(.*\)/\1/p' ../configure`
+DATE=`sed -n -e 's/^DATE=\(.*\)/\1/p' ../configure`
 RELEASENUM=1
 DISTRIBDIR=`pwd`
 
@@ -23,32 +24,33 @@ echo Default values are taken from ../configure
 echo ------------------------------------------
 
 # Determine the release number
-echo -n "What is the version number of the current release [$VERSION]? "
+echo -n "Version number of the current release [$VERSION]? "
 read ANSWER
 case $ANSWER in
  "") true;;
  *) VERSION=$ANSWER;
 esac
 
-DASHEDVERSION=V`echo $VERSION | sed -e 's/\./-/g'`
-#MAJORVERSION=V`echo $VERSION | sed -e 's/^\([0-9]\)\.[0-9].*/\1/'`
-MAJORVERSION=V7
-MAINNUMBER=`echo $VERSION | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
-LASTNUMBER=`echo $VERSION | sed -e 's/.*\.\([0-9]*\)$/\1/'`
-if [ "$LASTNUMBER" = "0" ]; then
-        LASTNUMBER=`echo $MAINNUMBER | sed -e 's/.*\.\([0-9]*\)$/\1/g'`
-	MAINNUMBER=`echo $MAINNUMBER | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
-fi
+# The main number of the release
+MAINNUMBER=`echo $VERSION | sed -e 's/^\([0-9]\+*\)\.[0-9]\+.*$/\1/'`
+# The minor number
+LASTNUMBER=`echo $VERSION | sed -e 's/^[0-9]\+\.\([0-9]\+\).*$/\1/'`
+# The release level: alpha, beta, etc.
+LEVEL=`echo $VERSION | sed -e 's/^[0-9]\+\.[0-9]\+\(.*\)$/\1/'`
+
+MAJORVERSION=V$MAINNUMBER
+CVSMODULE=V7
+CVSTAG=V`echo $VERSION | sed -e 's/\./-/g'`
 if [ "$LASTNUMBER" = "0" ]; then
-        LASTNUMBER=`echo $MAINNUMBER | sed -e 's/.*\.\([0-9]*\)$/\1/g'`
-	MAINNUMBER=`echo $MAINNUMBER | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
+    PREVIOUSMAINNUMBER=`expr $MAINNUMBER - 1`
+    PREVIOUSVERSION=$PREVIOUSMAINNUMBER.99
+else
+    PREVIOUSLASTNUMBER=`expr $LASTNUMBER - 1`
+    PREVIOUSVERSION=$MAINNUMBER.$PREVIOUSLASTNUMBER
 fi
-PREVIOUSLASTNUMBER=`expr $LASTNUMBER - 1`
-PREVIOUSVERSION=$MAINNUMBER.$PREVIOUSLASTNUMBER
 
 # Determine the previous release number
-echo -n "What is the version number of the previous release "
-echo -n "(for the patch file) [$PREVIOUSVERSION]? "
+echo -n "Version number of the previous release (for the patch file) [$PREVIOUSVERSION]? "
 read ANSWER
 case $ANSWER in
  "") true;;
@@ -57,15 +59,15 @@ esac
 
 
 # Determine the searchisos version number
-echo -n "What is the version number of the current SearchIsos release [$VERSIONSI]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) VERSIONSI=$ANSWER;;
-esac
+#echo -n "What is the version number of the current SearchIsos release [$VERSIONSI]? "
+#read ANSWER
+#case $ANSWER in
+# "") true;;
+# *) VERSIONSI=$ANSWER;;
+#esac
 
 # Determine the date of the release
-echo -n "What is the date of the current release [$DATE]? "
+echo -n "Date of the current release [$DATE]? "
 read ANSWER
 case $ANSWER in
  "") true;;
@@ -73,21 +75,21 @@ case $ANSWER in
 esac
 
 # Determine the rpm release number
-echo -n "What is the release number for the RPM packages [1]? "
+echo -n "Release number for the RPM packages [$RELEASENUM]? "
 read ANSWER
 case $ANSWER in
  "") true;;
  *) RELEASENUM=$ANSWER;;
 esac
 
-echo VERSION=$VERSION > config.distrib
-echo VERSIONSI=$VERSIONSI >> config.distrib
-echo PREVIOUSVERSION=$PREVIOUSVERSION >> config.distrib
+echo CVSMODULE=$CVSMODULE > config.distrib
+echo CVSTAG=$CVSTAG >> config.distrib
 echo DISTRIBDIR=$DISTRIBDIR >> config.distrib
-echo DASHEDVERSION=$DASHEDVERSION >> config.distrib
-echo MAJORVERSION=$MAJORVERSION >> config.distrib
+echo VERSION=$VERSION >> config.distrib
 echo RELEASENUM=$RELEASENUM >> config.distrib
 echo ARCH=$ARCH >> config.distrib
+echo PREVIOUSVERSION=$PREVIOUSVERSION >> config.distrib
+#echo VERSIONSI=$VERSIONSI >> config.distrib
 chmod +x config.distrib
 
 # $Id$