path: root/distrib/RELEASE

(**************************************************************************)
(*               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.