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
|
Proc�dure d'ajout d'une nouvelle contribution Coq
-------------------------------------------------
A) INT�GRATION DE LA CONTRIBUTION � L'ARCHIVE CVS
Dans l'archive des contributions nouvelle syntaxe ("constr/contrib8",
alias�e � "contrib" dans l'archive pauillac:/net/pauillac/constr/ARCHIVE).
1) Si la contribution provient d'une institution qui n'a pas encore
contribu�, cr�er un r�pertoire du nom de l'institution.
2) Dans le r�pertoire associ� � l'institution, cr�er un r�pertoire du nom de
la contribution. S'assurer que le nom est significatif.
3) Placer la contribution soumise dans ce r�pertoire et v�rifier
qu'elle compile avec la version bugfix de la version de Coq
actuellement distribu�e (ci-dessous appel�e version X.XX).
4) S'assurer que les fichiers Make et Makefile existent et sont dans
le format standard de coq_makefile, et r�cursivement dans les
sous-r�pertoires. Sinon, standardiser Make et Makefile et v�rifier
que cela continue de compiler.
5) Ajouter le nouveau r�pertoire du Make se trouvant dans le
r�pertoire de l'institution et reconstruire le Makefile associ�.
6) Si l'institution est nouvelle, ajout� son nom au Make et au
Makefile principal de l'archive contrib (attention, Makefile n'est
pas auto-engendr�, c'est Makefile.sites qui l'est).
7) V�rifier que l'auteur de la contribution a soumis un fichier
description et que les champs sont correctement nomm�s. V�rifier
l'orthographe, etc. S'assurer que le fichier description est � la
racine du r�pertoire associ� � la contribution. V�rifier que
l'identifiant "Name" (ci-dessous appel� CONTRIBNAME) associ� � la
contribution est significatif et pas d�j� pris par une autre
contribution.
8) Si la contribution a un fichier jouant le r�le d'un README,
s'assurer qu'il s'appelle bien README quitte � le renommer (par
exemple "readme" doit �tre renomm�).
9) Commiter l'ajout du ou des nouveaux r�pertoires et fichiers, ainsi
que la modification des diff�rents Make et Makefile (et �ventuellement
Makefile.sites).
10) Si la contribution compile bien, on peut d�placer le tag associ� �
la version actuellement distribu�e vers les nouveaux fichiers et
r�pertoires (utiliser "cvs tag -F nom-du-tag noms-des-fichiers").
B) INT�GRATION � LA SECTION CONTRIBUTIONS UTILISATEURS DU SITE WEB
Sur la section contributions du site web de Coq (module www sur
pauillac.inria.fr:/net/pauillac/constr/ARCHIVE, sous-r�pertoire
coq/contribs)
1) D�terminer la ou les cat�gories et sous-cat�gories dans laquelle
classer la nouvelle contribution. Le cas �ch�ant, ajouter une
nouvelle sous-cat�gorie.
2) Dans le ou les fichiers .prehtml associ�s � cette ou ces
cat�gories, ajouter un item bilingue avec le nom de la
contribution, son identifiant, et les auteurs.
3) Faire "make" dans le r�pertoire www/coq/contribs apr�s avoir
configurer ../config avec le tag de la version courante de Coq et
s'�tre assur� que contrib-X.XX �tait effac�.
Cette �tape n�cessite la pr�sence de htmlpp.
Attention il y a (au moins) deux programmes qui portent ce nom sur le web.
Ici on a besoin de celui-ci : http://htmlpp.sourceforge.net/
4) Faire une mise � jour partielle du site web de coq:
export MACHINE=pauillac.inria.fr
export WEB=/net/yquem/infosystems/www/logical/coq/contribs
export FTP=/net/pauillac/infosystems/ftp/coq/coq/current
#
# installer les infos des contributions dans le r�pertoire web coq/contribs
#
scp all-contribs/CONTRIBNAME.{tar.gz,html,description}\
all-contribs/search.db all-contribs/summary.html *.html $MACHINE:$WEB
ssh $MACHINE chmod -f g+w $WEB/*
#
# installer la nouvelle archive de toutes les contribs
#
scp contrib-X.XX.tar.gz $MACHINE:$FTP
ssh $MACHINE chmod -f g+w $FTP/contrib-X.XX.tar.gz
#
# installer la nouvelle contribution dans le r�pertoire d'archivage
# des contribution par num�ro de version de Coq
#
scp all-contribs/CONTRIBNAME.tar.gz \
$MACHINE:/net/yquem/infosystems/www/logical/coq/contributions/VX.XX
5) S'assurer que le site web de coq a �t� mis � jour correctement, que
la nouvelle contribution appara�t dans les versions anglaise et
fran�aise du classement th�matique, ainsi que dans la liste
compl�te. V�rifier que l'outil de recherche par mot-cl� la trouve.
6) Commiter les modifications faites � l'archive www/coq/contribs
7) Confirmer � l'auteur l'installation de sa contribution
|
