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
|
