Pour créer les archives distribuées

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

7 files changed, 908 insertions, 0 deletions

diff --git a/distrib/.cvsignore b/distrib/.cvsignore
new file mode 100644
index 000000000..da1304664
--- /dev/null
+++ b/distrib/.cvsignore
@@ -0,0 +1,14 @@
+rpmbuildroot
+i386
+sun4
+alpha
+apx
+alpha
+ppc
+redhat
+rpmrc
+rpmmacros
+config.distrib
+coq-*
+contrib-*
+patch-*
diff --git a/distrib/Makefile b/distrib/Makefile
new file mode 100644
index 000000000..786dc4c11
--- /dev/null
+++ b/distrib/Makefile
@@ -0,0 +1,276 @@
+# Building the different files of the coq distribution
+
+include config.distrib
+LOCALARCH=`uname -m`
+ARCH=`uname -m | sed -e 's/i.86/i386/'`
+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}
+RAWRPM=rpm
+RPMVERSION=`${RAWRPM} --version | sed -e "s/RPM version \(.\).*/\1/"`
+RPM=${RAWRPM} ${RPMBUILDROOTOPT} --rcfile rpmrc
+
+FTPDIR=/net/pauillac/infosystems/ftp/coq/coq
+WWWDIR=/net/pauillac/infosystems/www/coq
+
+COQPACKAGE=coq-${VERSION}
+COQRPMPACKAGE=coq-${VERSION}-${RELEASENUM}
+
+######################
+
+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 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 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"
+
+################## Main targets
+
+distrib: tag tar-gz
+rpm: src-rpm arch-rpm
+
+#################
+tag:
+	@dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\
+	majorversion=V`echo ${VERSION} | sed -e 's/^\([0-9]\.[0-9]\).*/\1/g'`;\
+	echo -n "Tagging the archive with version number $$dashedversion... ";\
+	cvs rtag -F $$dashedversion $$majorversion
+
+tar-gz:
+	@echo -n Exporting a fresh copy of the archive...
+	@- rm -rf ${COQPACKAGE}
+	@cvs export -d $(COQPACKAGE) -r $(DASHEDVERSION) $(MAJORVERSION)
+	@echo done
+	@echo -n Removing the maintenance files and doc...
+	@rm -rf ${COQPACKAGE}/doc
+	@rm -rf ${COQPACKAGE}/distrib
+	@rm -rf ${COQPACKAGE}/{KNOWN-BUGS,TODO,ANNONCE}
+	@find ${COQPACKAGE} -name ".cvsignore" -exec rm {} \;
+	@echo done
+	@echo -n Building the tar.gz source package
+	@tar cvf ${COQPACKAGE}.tar ${COQPACKAGE}
+	@gzip ${COQPACKAGE}.tar
+	@echo done
+	@echo Checking release parameters
+	./check-list
+	@echo done
+
+src-rpm: ${COQRPMPACKAGE}.src.rpm
+arch-rpm: ${COQRPMPACKAGE}.${ARCH}.rpm
+
+test:
+	cp ${COQPACKAGE}.tar.gz tmp.tar.gz
+	gunzip tmp.tar.gz
+	@echo Trying "make world" then "make world-opt"
+	- rm -rf ${COQPACKAGE}
+	tar xf tmp.tar
+	(cd ${COQPACKAGE};\
+	configure -local -opt -emacs emacs;\
+	make world >& log.world;\
+	if [ `tail -1 log.world` = "=== Compilation in bytecode is done ===" ];\
+	then echo make world succeeded;\
+	else echo make world failed; exit 1;\
+	fi;\
+	make world-opt >& log.world-opt;\
+	if [ `tail -1 log.world` = "=== Compilation in native code is done ===" ];\
+	then echo make world-opt succeeded;\
+	else echo make world-opt failed; exit 1;\
+	fi)
+	rm -r ${COQPACKAGE}
+	@echo Trying "make world" then "make world-opt"
+	tar xf tmp.tar
+	(cd ${COQPACKAGE};\
+	configure -local -opt -emacs emacs;\
+	make world >& log.world;\
+	if [ `tail -1 log.world` = "=== Compilation in bytecode is done ===" ];\
+	then echo make world succeeded;\
+	else echo make world failed; exit 1;\
+	fi;\
+	make world-opt >& log.world-opt;\
+	if [ `tail -1 log.world` = "=== Compilation in native code is done ===" ];\
+	then echo make world-opt succeeded;\
+	else echo make world-opt failed; exit 1;\
+	fi)
+	rm tmp.tar
+	@echo "Both orders of compilation suceeded"
+
+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 $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+
+arch-tar-gz-final:
+	(cd ${ARCHBUILDROOT}/buildroot;\
+	tar -cvf ${DISTRIBDIR}/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
+	gzip $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+
+arch-tar-gz: ${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;\
+	make world-opt world;\
+	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
+	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install)
+	$(MAKE) arch-tar-gz-final
+
+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}" = "3" ];\
+	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)
+
+# Les cibles suivantes ne sont pas acceptées sur DEC (car paramétrées)
+
+${COQPACKAGE}.tar.gz:
+	${MAKE} tar-gz
+
+# rpm 3.0 met dans LOCALARCH mais rpm 2.5 dans ARCH...
+${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz
+	${MAKE} rpm-config
+	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
+	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
+	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
+	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
+	${RPM} -ba coq.spec
+	mv ${RPMTOPDIR}/SRPMS/${COQRPMPACKAGE}.src.rpm .
+	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
+	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${RPMT\
+OPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm;
+	fi)
+	- mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .
+
+# Sera déjà fait si le src.rpm vient d'être fait
+${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm
+	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
+	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
+	${RPM} --rebuild ${COQRPMPACKAGE}.src.rpm
+	mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .
+
+##########
+contrib-tag:
+	@dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\
+	echo -n "Tagging the contrib with version number $$dashedversion... ";\
+	cvs rtag -F $$dashedversion contrib
+	@echo done
+
+contrib-tar-gz:
+	- rm -rf contrib-${VERSION}
+	@echo -n Exporting a fresh copy of the contribs...
+	@dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\
+	cvs export -d contrib-${VERSION} -r $$dashedversion contrib
+	@echo done
+	- rm contrib-${VERSION}.tar.gz
+	@echo -n Building the tar.gz contrib package
+	@tar cvf contrib-${VERSION}.tar contrib-${VERSION}
+	@gzip 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 ${COQPACKAGE}.tar.gz | tar x
+	diff -rc coq-$(PREVIOUSVERSION) ${COQPACKAGE} > patch-${VERSION}-$(PREVIOUSVERSION)
+	gzip patch-${VERSION}-$(PREVIOUSVERSION)
+
+##########
+clean:
+	- rm -rf ${COQPACKAGE} ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT}
+
+cleanall:
+	- rm -rf ${COQPACKAGE}* ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} 
+
+########## Installation in the ftp repository
+
+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}.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}
+	(cd $(FTPDIR); rm -f current;ln -sf V${VERSION} current)
+
+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
+
+arch-rpm-ftp-install: prep-ftp-install
+	cp ${COQRPMPACKAGE}.${ARCH}.rpm ${FTPDIR}/V${VERSION}/
+	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.${ARCH}.rpm
+
+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
+
+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
diff --git a/distrib/RELEASE b/distrib/RELEASE
new file mode 100644
index 000000000..8290856dc
--- /dev/null
+++ b/distrib/RELEASE
@@ -0,0 +1,353 @@
+(**************************************************************************)
+(*               Liste des choses à faire pour une release                *)
+(**************************************************************************)
+
+PLAN
+
+A) LE LOGICIEL (SOURCES ET BINAIRES)
+B) LES CONTRIBS
+C) LA DOC
+D) LE SERVEUR WEB
+E) LE CDROM (indépendant de la release)
+
+(**************************************************************************)
+A) LE LOGICIEL
+
+A1) VÉRIFICATIONS
+
+  S'assurer que les choses suivantes été réalisées et COMMITÉES.
+
+  - Changement du magic number dans src/meta/library.ml si la syntaxe
+    interne des .vo a changé
+
+  - Changement des variables en tête du fichier "configure" et
+    vérification du numéro de versions de OCaml et Camlp4 demandées
+  - Mise à jour des champs Version, Source et Require et vérifier la
+    liste des "%files" dans "distrib/coq.spec"
+  - Relecture des fichiers "README", "README.win", en particulier,
+    vérification du numéro de version, des adresses internet et des
+    coordonnées de Coq
+  - Relecture des fichiers "INSTALL", "INSTALL.win" en particulier numéro
+    de version de coq et numéros des versions de OCaml et Camlp4 demandées
+
+  - S'assurer après un "make cleanall" que "make world" et "make
+    world-opt" commutent                      # Caduc pour la V7
+
+  - Mise à jour/nettoyage du fichier CHANGES et du fichier ANNONCE
+
+  EN CAS DE MODIFICATION DE L'ARCHIVE, REPRENDRE EN A3
+  (ou en A2 si la date ou le numéro de version a changé)
+
+  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.
+
+A2) CONFIGURATION DES PARAMETRES DE LA DISTRIBUTION
+
+  Se placer dans le répertoire distrib et faire
+
+     ./configure.distrib
+
+  pour positionner les paramètres de la distrib (les paramètres par
+défaut sont obtenus via le fichier "../configure". Si celui-ci n'est
+pas conforme à l'archive (sans doute peu probable, mais cela m'est
+arrivé), il faut donner les valeurs à la main.
+
+A3) ESTAMPILLAGE DE L'ARCHIVE
+
+  Toujours dans le répertoire distrib, faire
+
+     make tag
+
+  pour (on suppose que le numéro de version donné dans
+configure.distrib est V6.2.5) poser le tag V6-2-5 à l'archive V6-2.
+
+  La commande "make tag" peut être refaite plusieurs fois auquel cas
+l'ancienne marque est supprimée avant d'être remise à la nouvelle
+place.
+
+  Pour ne modifier qu'un fichier isolément sans retagger toute
+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
+frais (obtenu par cvs export) de l'archive avec
+
+     make tar-gz
+
+  En particulier, les fichiers à ne pas distribuer (dont la doc) sont
+retirés. Cette commande fait dérouler une check-list. Si on
+l'interrompt ou qu'elle échoue, le tar-gz reste créé et c'est à la
+charge de l'utilisateur de s'assurer que les paramètres sont corrects.
+
+  Pour l'installation sous ftp voir A7.
+
+
+A5) CREATION DES PACKAGES BINAIRES (ad libitum)
+   (prévoir pour chaque package près de 100Mo dispo sur la partition)
+
+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).
+
+  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".
+
+  Pour l'installation sous ftp voir A7.
+
+  Remarque : ce binaire est prévu pour être dé-tar-ré dans / avec une
+installation dans /usr/local/bin.
+
+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
+(ex : coq-6.2.5-1.i386.rpm).
+
+  Remarques : 1) Les packages Intel s'appellent i386 même si
+l'architecture est i586 ou i686 (faux avec rpm 3.0). 2) Les rpm sont
+prévus pour une installation dans /usr/bin (!).
+
+  Pour l'installation sous ftp voir A7.
+
+A5c) Création d'un second package rpm à partir des sources rpm
+
+  Refaire 
+
+     make rpm
+
+  sous une autre architecture pour créer un deuxième package rpm binaire.
+
+  Pour l'installation sous ftp voir A7.
+
+A6) CREATION DU FICHIER DE PATCH (attention ne marche pas sur DEC je crois)
+
+    make patch (pas déboggué)
+
+  Pour créer un fichier de patch entre la version à distribuer et la
+version précédente se trouvant dans l'archive (supposée être la même
+que celle taggée V6-2-4 (version -1) dans l'archive CVS...).
+
+Remarque: On peut faire un patch aussi par
+
+  cvs rdiff -r V6-2-4 -r V6-2-5 V6-2 > patch-coq-6.2.4-6.2.5
+
+  Mais il faut alors éditer pour supprimer les références aux
+répertoires distrib et doc, aux fichiers TODO, KNOWNBUGS, ANNONCE et
+les .cvsignore .
+
+
+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
+   lie symboliquement à /net/pauillac/infosystems/ftp/coq/coq/current.
+
+   - installe sous ftp tous les fichiers tar.gz ou .rpm du répertoire
+  distrib (sources et binaires), ainsi que le fichier CHANGES
+
+  Pour installer seulement un des packages, faire au choix
+
+    make tar-gz-ftp-install
+    make src-rpm-ftp-install
+    make arch-rpm-ftp-install
+    make arch-tar-gz-ftp-install
+
+  À faire : ne mettre le lien current qu'au dernier moment.
+
+A8) VÉRIFICATION GÉNÉRALE
+
+  Télécharger et utiliser 24 heures la version FTP
+
+    # sur SunOS, Next, ...
+    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/V6.2.5.tar.gz
+    tar xvzf V6.2.5.tar.gz
+    cd V6.2.5
+    yes "" | ./configure
+    make world-opt world
+    make cleanall world world-opt
+    make install	
+
+    # sur i586
+    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/coq-6.2.5-1.i586.rpm
+    rpm -Uvh coq-6.2.5-1.i586.rpm
+    coqtop      # etc...
+    coqtop -opt # etc...
+
+    # sur linux ppc et apx
+    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/coq-6.2.5-1.src.rpm 
+    rpm --recompile coq-6.2.5-1.src.rpm
+    coqtop      # etc...
+    coqtop -opt # etc...
+
+  Cliquer un peu partout sur le serveur coq.inria.fr (rubrique coq
+proof assistant).
+
+  Si jamais quelque chose ne va pas, reprendre à l'étape A2 en retaggant
+l'archive après les modifications (le tag est automatiquement déplacé)
+
+A9) DIFFUSION
+
+  Préparer les contribs (B), la doc (C), le serveur web (D)
+
+  Ouf, c'est prêt... faire l'annonce sur coq-club
+
+
+(**************************************************************************)
+B) LES CONTRIBS
+
+B1) PRÉPARATION
+
+  - se placer dans une version à jour des contribs (si pas déjà fait,
+le faire avec un "cvs checkout contrib" quelque part en dehors de
+l'archive V6).
+
+  - positionner les variables COQTOP et COQBIN (avec un / à la fin !!)
+sur une version à jour de l'archive V6 et s'assurer que make opt et
+make passent.
+
+B2) POSE DU TAG
+
+  Dans le répertoire distrib, faire
+
+    make contrib-tag
+
+  pour poser le tag V6-2-5
+  (ceci est équivalent à "cvs rtag -F V6-2-5 contrib")
+
+B3) CRÉATION DU PACKAGE
+
+  Dans le répertoire distrib, faire
+
+    make contrib-tar-gz
+
+  pour créer contrib-6.2.5.tar.gz
+
+B4) INSTALLATION SOUS FTP
+
+  Dans le répertoire distrib, faire
+
+    make contrib-ftp-install
+
+  pour installer le package contrib-6.2.5.tar.gz en ftp
+
+
+(**************************************************************************)
+C) LA DOC
+
+  Dans l'état actuel des choses, la doc est compilée dans le
+répertoire doc d'une copie locale des sources de Coq. Il n'y a pas
+pour la doc d'export relatif au tag V6-2-5 comme c'est le cas pour la
+creation de l'exécutable.
+
+C1) PRÉPARATION
+
+  S'assurer que les outils suivants sont disponibles
+
+    Dvi: latex (latex2e), bibtex, makeindex, dviselect (rpm dviutils)
+    Ps: dvips, psselect (package psutils)
+    Pdf: pdflatex (optionnel)
+    Html: hevea (par Luc Maranget), htmlsplit (par David Delahaye)
+
+  Mettre à jour les fichiers suivants :
+
+  - Tutorial.tex : numéro de version (2 fois) et date
+  - title.tex    : numéro de version
+  - cover.html   : numéro de version et date (2 fois)
+  - README       : numéros de version (3 fois)
+  - macros.tex   : numéro de version
+
+  Vérification que "CHANGES" est à jour par rapport à "Changes.tex"
+
+  Faire un make clean; grep V6 *.{tex,sty,html} pour s'assurer
+qu'aucun autre V6.? ne traine.
+
+  Les fichiers Tutorial-cover.tex et RefMan-cover.tex ne servent que
+pour faire des rapports INRIA.
+
+  Si un fichier Anomaly.dvi doit être distribué, s'en occuper à la main
+(ou modifier le Makefile en conséquence).
+
+C2) COMPILATION
+
+  Pour compiler l'ensemble des fichiers de documentation à installer
+sous ftp et/ou sur le serveur web, faire dans le répertoire doc
+
+    make distrib
+
+  qui crée les versions dvi.gz, ps.gz, pdf.gz de la doc, les packages
+all-ps-doc.tars.gz et doc-html.tar.gz ainsi qu'un répertoire www
+recopiable sur le site web
+
+  Si la doc est modifiée après le tagguage des sources Coq, retagguer
+la doc séparemment depuis le répertoire doc avec
+
+  cvs tag -F V6-2-5 * library/*
+
+C3) INSTALLATION SOUS FTP
+
+    Après avoir positionner la variable VERSION à V6.2.5, installer
+la doc sous ftp depuis le répertoire doc avec
+
+    make doc-ftp-install
+
+    On retrouve alors sous ftp avec le README, plusieurs couples
+    .dvi.gz et .ps.gz, le tar de la doc html, le tar des docs en ps.
+
+
+(**************************************************************************)
+D) LE SERVEUR WEB
+
+D1) PRÉPARATION
+
+   Cela se fait sous CVS : faire un check-out ou update du module
+"www" quelque part chez soi en dehors de l'archive V6, puis
+
+   - mettre à jour les fichiers (numéro de version, version
+     nécessaires de ocaml et camlp4, date de mise à jour)
+     distrib1-fra.html et distrib1-eng.html,
+     contribs1-fra.html et contribs1-eng.html
+     assis1-eng.html et assis1-fra.html
+     tools1-eng.html et tools1-fra.html (pas de V devant le numéro)
+
+   - commiter
+
+   - À partir de votre copie locale du répertoire www, faire
+  
+     (cd contribs; make pages)
+
+   - Puis positionner la variables THEORIES sur le repertoire theories
+     d'une copie fraîche de l'archive et faire (sur PAUILLAC et avec
+     gmake parce que fabrique un binaire devant tourner sur pauillac)
+
+     (cd library; gmake pages)
+
+D2) ACTUALISATION DU SERVEUR WEB
+
+     Enfin, faites-en part au monde entier :
+
+     make install
+     (cd contribs; make install)
+     (cd library; make install)
+
+
+(**************************************************************************)
+E) LE CDROM
+
+  Tout est en place dans /net/pauillac/constr/cdrom. S'y rendre et 
+
+  - mettre à jour les fichiers prog/{unix,pc,mac}/coq/{fra,eng}.htm
+  - mettre à jour les liens dans ftp/coq 
+	(1 lien pour la version Mac, 1 lien pour les autres architectures).
+  - vérifier que projs/coq/{fra,eng}.htm sont corrects
diff --git a/distrib/check-list b/distrib/check-list
new file mode 100755
index 000000000..6f2298748
--- /dev/null
+++ b/distrib/check-list
@@ -0,0 +1,99 @@
+#!/bin/sh
+
+. ./config.distrib
+
+echo
+echo The Coq Check List
+echo ------------------
+echo
+
+COQPACKAGE=coq-$VERSION
+CONFIGFILE=$COQPACKAGE/configure
+
+version=`grep "^VERSION=" $CONFIGFILE | sed -e 's/^VERSION=\(.*\)/\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"
+echo "  The release version is V$version"
+echo "  The SearchIsos release version is V$versionsi"
+echo "  The date is $coqdate"
+echo
+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 [ ! "$date" = "$DATE" ]; then
+	echo "Inconsistent date release";exit
+fi
+
+echo "Please answer y or n to questions"
+
+if grep $version $COQPACKAGE/src/meta/library.ml > /dev/null; then
+  echo "Found a reference to $version in library.ml..."
+  echo "   ... I guess the magic numbers have been changed"
+else
+  echo 'Found no trace that the magic numbers are changed in library.ml'
+  echo -n 'Is it still OK? '
+  read a
+  if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
+fi
+
+readmeversion=`grep "THE COQ .* SYSTEM" $COQPACKAGE/README | sed -e 's/.*THE COQ \(.*\) SYSTEM.*/\1/'`
+if [ "$readmeversion" = "" ]
+then echo "Failed to find version number in README; please check by hand"
+else
+  echo -n The README file seems to mention version number $readmeversion ...
+  if [ $readmeversion = V$version ]
+  then echo " it seems OK"
+  else echo -n " is that really OK? "
+     read a
+     if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
+  fi
+fi
+
+readmewinversion=`grep "THE COQ .* SYSTEM" $COQPACKAGE/README.win | sed -e 's/.*THE COQ \(.*\) SYSTEM.*/\1/'`
+if [ "$readmewinversion" = "" ]
+then echo "Failed to find version number in README.win; please check by hand"
+else
+  echo -n The README.win file seems to mention version number $readmewinversion ...
+  if [ $readmewinversion = V$version ]
+  then echo " it seems OK"
+  else echo -n " is that really OK? "
+     read a
+     if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
+  fi
+fi
+
+ocamlversion=`grep "You need Objective-Caml .* or later" $CONFIGFILE | sed -e 's/.*Objective-Caml \(.*\) or later.*/\1/'`
+echo -n The configure file seems to require O\'Caml version $ocamlversion ...
+echo -n " is that OK? "
+read a
+if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
+
+versionspec1=`grep "^Version: " ./coq.spec | sed -e 's!^Version: \(.*\)!\1!'`
+versionspec2=`grep "^Source: " ./coq.spec | sed -e 's!.*coq-\(.*\)\.tar\.gz.*!\1!'`
+if [ "$versionspec1" = "$version" -a "$versionspec2" = "$version" ];
+then echo "Version number in coq.spec seems OK ($versionspec1)";
+else
+  echo "Wrong version numbers in coq.spec ($versionspec1 and $versionspec2)"
+  echo Aborting; exit 1
+fi
+#  ocamlversionspec=`grep "^Requires: ocaml" ./coq.spec | sed -e 's/Requires: ocaml >= \(.*\)/\1/'`
+#  if [ "$ocamlversionspec" = "$ocamlversion" ]
+#  then echo "Required version of Objective Caml in coq.spec seems OK ($ocamlversionspec)"
+#  else
+#    echo "Wrong version of required Objective Caml in coq.spec ($ocamlversionspec)"
+#    echo Aborting; exit 1
+#  fi
+
+camlp4version=`grep "You need Camlp4 .* or later" $CONFIGFILE | sed -e 's/.*Camlp4 \(.*\) or later.*/\1/'`
+echo -n The configure file seems to require Camlp4 version $camlp4version ...
+echo -n " is that OK? "
+read a
+if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
+echo Check list completed
diff --git a/distrib/configure.distrib b/distrib/configure.distrib
new file mode 100755
index 000000000..5bb5e7657
--- /dev/null
+++ b/distrib/configure.distrib
@@ -0,0 +1,88 @@
+#!/bin/sh
+
+####################################
+#
+#  Configuration script for releases
+# 
+####################################
+#
+#  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/'`
+RELEASENUM=1
+DISTRIBDIR=`pwd`
+
+echo Default values are taken from ../configure
+echo ------------------------------------------
+
+# Determine the release number
+echo -n "What is the 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/'`
+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
+if [ "$LASTNUMBER" = "0" ]; then
+        LASTNUMBER=`echo $MAINNUMBER | sed -e 's/.*\.\([0-9]*\)$/\1/g'`
+	MAINNUMBER=`echo $MAINNUMBER | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
+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]? "
+read ANSWER
+case $ANSWER in
+ "") true;;
+ *) PREVIOUSVERSION=$ANSWER;;
+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
+
+# Determine the date of the release
+echo -n "What is the date of the current release [$DATE]? "
+read ANSWER
+case $ANSWER in
+ "") true;;
+ *) DATE=$ANSWER;;
+esac
+
+# Determine the rpm release number
+echo -n "What is the release number for the RPM packages [1]? "
+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 DISTRIBDIR=$DISTRIBDIR >> config.distrib
+echo DASHEDVERSION=$DASHEDVERSION >> config.distrib
+echo MAJORVERSION=$MAJORVERSION >> config.distrib
+echo RELEASENUM=$RELEASENUM >> config.distrib
+chmod +x config.distrib
+
+# $Id$
+
diff --git a/distrib/coq.spec b/distrib/coq.spec
new file mode 100644
index 000000000..14e5af155
--- /dev/null
+++ b/distrib/coq.spec
@@ -0,0 +1,78 @@
+Name: coq
+Version: 7.0beta
+Release: 1
+Summary: The Coq Proof Assistant
+Copyright: freely redistributable
+Group: Applications/Math
+Vendor: INRIA Rocquencourt
+URL: http://coq.inria.fr
+Source: ftp://ftp.inria.fr/INRIA/coq/V7.0/coq-7.0beta.tar.gz
+Icon: petit-coq.gif
+
+%description
+Coq is a proof assistant which: 
+  - allows to handle calculus assertions, 
+  - check mechanically proofs of these assertions, 
+  - helps to find formal proofs, 
+  - extracts a certified program from the constructive proof
+    of its formal specification, 
+
+# Ocaml is required but it is better to install it not with rpm but by
+# hand in /usr/local
+# Requires: ocaml >= 3.01
+
+
+%prep
+%setup
+
+%build
+./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt         # Need ocamlc.opt and ocamlopt.opt
+make world-opt world       # Use native coq to compile theories
+
+%clean
+make cleanall
+
+%install
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install
+# To install only locally the binaries compiled with absolute paths
+
+%post
+# This is because the Coq Team usually build Coq with Ocaml in /usr/local
+# but ocaml is actually in /usr if coming from a rpm package
+where=`ocamlc -v | tail -1 | sed -e 's/.*: \(.*\)/\1/'`
+if [ ! "$where" = "/usr/local/lib/ocaml" ]; then
+	ln -s $where /usr/local/lib/ocaml
+fi
+
+%postun
+# This is because the Coq Team usually build Coq with Ocaml in /usr/local
+# but ocaml is actually in /usr if coming from a rpm package
+where=`ocamlc -v | tail -1 | sed -e 's/.*: \(.*\)/\1/'`
+if [ ! "$where" = "/usr/local/lib/ocaml" ]; then
+	rm $where /usr/local/lib/ocaml
+fi
+
+%files
+/usr/bin/coqc
+/usr/bin/coqtop
+/usr/bin/coqtop.byte
+/usr/bin/coqtop.opt
+/usr/bin/coq-tex
+/usr/bin/coqdep
+/usr/bin/gallina
+/usr/bin/coq_makefile
+#/usr/bin/coq_searchisos.out
+/usr/bin/coqmktop
+#/usr/bin/coq2html
+#/usr/bin/coq2latex
+/usr/lib/coq
+#/usr/man/man1/coqc.1
+#/usr/man/man1/coqtop.1
+#/usr/man/man1/coqmktop.1
+/usr/man/man1/coqdep.1
+/usr/man/man1/gallina.1
+/usr/man/man1/coq-tex.1
+#/usr/man/man1/coq2latex.1
+#/usr/man/man1/coq2html.1
+/usr/share/emacs/site-lisp/coq.el
+/usr/share/emacs/site-lisp/coq.elc
diff --git a/distrib/petit-coq.gif b/distrib/petit-coq.gif
new file mode 100644
index 000000000..2d1228311
--- /dev/null
+++ b/distrib/petit-coq.gif