Re: [GeOCaml] news

[Georges Mariano]

En réponse à Julien Narboux <address@hidden>:

> Rebonjour,
> 
> Je vais peut-être lancer la discussion en resumant rapidement mon projet

je fais une réponse courte juste sur la manière de procéder, il me faut du temps
pour dépouiller cette longue liste de propositions ! ;-)


a) Je suis pour une modularisation forte des développements de manière à bien
séparer les fonctionnalités et les technos. Il ne faut pas effectivement
fusionner trop rapidement mais il reste possible d'avoir des développements
distincts localisés au même endroit (ne serait-ce que pour profiter des services
Gna). Il s'agit donc essentiellement de se regrouper pour avoir une meilleur
visibilité ...

b)  Une liste aussi étoffée de proposition mérite d'être mise sous forme de wiki
de manière  à permettre de creuser les différents points de manière
"asynchrone"... Je suppose que Julien n'étant pas trop à l'aise avec ça, je
propose qu'Arnaud transforme son dernier message en une page wiki où nous
pourrons réagir plus facilement... Une fois cela fait, Julien devrait "capter"
les conventions utiles et prendre le relai ...

Je ferais un passage de relecture dès que possible (probablement ce soir) 

c) La génération des fichiers en entrée aux prouveurs doit se faire à partir de
la sortie XML de GeOCaml. Dès lors, pour des prouveurs "analogues" c'est XSLT
qui se charge de générer les bons formats d'entrée (pour Phox, COQ, Hol(?)...)

.geo --(GeOCaml/parser)-> .xml --XSLT/Phox -> .phx --> (PhoX)  
                               --XSLT/Coq  -> .v --> (COQ)  

c'est le principe en tout cas ;-)

-- 
mailto:address@hidden
val-libre : http://www.mjc-athena.org/cgi-bin/mailman/listinfo/val-libre
DebFr :  http://wiki.debian.net/index.cgi?DebianFrench