aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib/RELEASE
blob: ef84410f9a78c10311a73ea607067177dfae168f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
(**************************************************************************)
(*               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.