(**************************************************************************) (* Liste des choses à faire pour une release *) (* Mise à jour V7 *) (**************************************************************************) 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 library/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 éventuellement Require et setup dans RH/coq*.spec - Mise à jour des dépendances dans debian/control. Ajouter une référence à la version et un "* New upstream version" dans debian/changelog. [Note: archive debian maintenant engendrée par Debian eux-mêmes] - 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", "INSTALL.macosx", en particulier numéro de version de coq et numéros des versions de OCaml et Camlp4 demandées - Mise à jour/nettoyage du fichier CHANGES et du fichier ANNONCE - Mise à jour des fichiers .dep.ps dans le répertoire doc (faire make depend depuis ce répertoire) S'assurer aussi que make world, make doc et make check fonctionnent ! 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-X.Y.Z.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 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). Si le tag est à poser sur une branche, il ne faut pas utiliser "make tag" mais faire à la main cvs rtag -r branch-tag VX-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 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-X.Y.Z.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 le répertoire distrib, le TODO, etc) sont retirés (rebrancher aussi dans le Makefile le répertoire theories/Num quand il sera opérationnel). 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-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-X.Y.Z.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 des sources rpm et des premiers packages rpm make rpm dans le répertoire distrib sous l'architecture ARCH crée un package 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 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 Faire make arch-rpm sous une autre architecture pour créer un deuxième package rpm binaire. Pour l'installation sous ftp voir A7. A5d) Création d'un package coq-ide (normalement fait par "make rpm") 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 make deb pour faire paquets source et binaire sur une machine debian (pc8-118.lri.fr par exemple). Pas la peine d'essayer de créer le binaire sur toutes les architectures : ce sera fait par les machines de Debian dès que le paquet source leur sera fourni. 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 coqtop exécutable que sous cygwin) installée dans un répertoire ne contenant pas d'espace, avec les variables CAMLLIB et CAMLP4LIB positionnée (ainsi que ocamlc et camlp4 dans le PATH). Faire un make win pour créer une archive zip. Envoyer ensuite l'archive par ftp dans 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) 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/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 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) Positionner le lien current du répertoire FTP vers le répertoire de la version ftp à distribuer avec make final-ftp-install Ouf, c'est prêt... faire l'annonce sur coq-club (**************************************************************************) B) LES CONTRIBS B1) PRÉPARATION Cette phase de vérification est actuellement remplacée par le test nocturne coqbench de J.-C. qui permet de savoir ce qui ne passe pas et pourquoi. Ancienne méthode de vérification : - 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") B4) SUPPRESSION DES FICHIERS INUTILES ET CRÉATION DU PACKAGE Dans le répertoire distrib, faire make contrib-tar-gz pour créer contrib-6.2.5.tar.gz Attention, le répertoire PROGRAMS est actuellement retiré (le réactiver dans le Makefile si besoin est). Les fichiers bench.log sont aussi retirés. B5) 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 La doc se prépare à partir du répertoire cvs "doc". Sa compilation nécessite la présence dans le path d'une archive Coq correspondant au tag de la release. 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 (plus utilisé depuis Coq 8.0) Mettre à jour les fichiers suivants : - Tutorial.tex : numéro de version et date (1 fois) - title.tex : numéro de version - cover.html : numéro de version (2 fois) et date - README : numéros de version (2 fois) - Makefile : numero de version Vérification que "CHANGES" est à jour par rapport à "Changes.tex" (obsolète, plus de Changes.ps mais un Changes.html engendré manuellement à partir de CHANGES). 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). Si un fichier Changes.dvi doit être distribué, s'en occuper à la main (ou modifier le Makefile en conséquence). C2) ESTAMPILLAGE Faire cvs rtag -F V7-1 doc pour tagger l'archive avec le numéro de la version de Coq auquel elle correspond C3) 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/* C4) LA BIBLIO STANDARD AU FORMAT COQDOC Le package library-X.Y.tar.gz sa fait dans l'archive cvs du site web, répertoire www/coq/library. Il faut au préalable mettre à jour le fichier www/coq/config avec le bon tag de version. La cible est alors make pages Elle exporte une archive fraiche correspondant au tag du fichier config, puis recompile la bibliothèque standard en exportant les références globales. Elle applique ensuite coqdoc à la bibliothèque standard puis crée un paquet des pages html obtenues. Il faut ensuite installer ce paquet à la main sur le site ftp. C5) 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. Ajouter à la main le fichier CHANGES de l'archive Coq dans /net/pauillac/infosystems/ftp/coq/coq/V6.2.5/doc (**************************************************************************) 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 - se placer dans le sous-répertoire "coq" de l'archive "www" - mettre à jour les fichiers suivants du répertoire coq (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 (dont un ajout de ligne à la fin) coq1-eng.html et coq1-fra.html doc1-eng.html et doc1-fra.html - commiter - créer un fichier Changes.html à partir du fichier CHANGES et le déposer dans /net/pauillac/infosystems/ft/coq/V6.2.5/doc (ce fichier est pointé par les pages coq1-fra.html et coq1-eng.html) - à partir de sa copie locale du répertoire www, faire (cd coq/contribs; make pages) - positionner la variable THEORIES sur le repertoire theories d'une copie fraîche de l'archive et faire (sur PAUILLAC et avec gmake parce qu'un binaire devant tourner sur pauillac est fabriqué) (cd coq/library; gmake pages) D2) ACTUALISATION DU SERVEUR WEB Enfin, faites-en part au monde entier : make install-coq (cd coq/contribs; make install) (cd coq/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/logical/{fra,eng}.htm et *.html sont corrects Pour les sites www (coq et logical) faire une copie et modifier les liens relatifs suivant l'architecture du cdrom.