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 Require dans RH/coq.spec.tpl
  - Mise � jour des d�pendances dans debian/control. Ajouter une r�f�rence
    � la version et un "* New upstream version" dans debian/changelog.
  - 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
  - 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-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 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).

  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 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.


 tag -F V6-2-5 nom_du_fichierqq5) 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.

A5d) 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.

A5e) 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/V6.2.5

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)

  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

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

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