Re: [GeOCaml] news

[Julien Narboux]

> les macros : le dernier problème traité dans GeOCaml ! ;-) maintenant
> faut voir ce que sa donne (projet étudiant) et éventuellement s'adapter
> à une autre proposition. L'idée que j'ai eu récemment et qui va
> contenter probablement tout le monde c'est de voir (syntaxiquement) les
> macros comme des énoncés de théorèmes (ou vice-versa ;-)
>  

Quel genre d'énoncés ? tu peux donner un exemple ?
l'idée est séduisante, on pourrait voir les macros aussi comme des 
PREUVES de théorèmes du style :
Axiomes 1 -> Axiome 2 -> ... -> Axiome n -> il existe A tel que P(A).

où les "Axiomes i"  expriment l'existence des points construits grâce 
aux n constructions de base.

On pourrait autoriser l'utilisateur à se restreindre à certaines 
constructions de base par exemple :
- la regle et le compas
- avoir trois points non alignés et pouvoir prendre un point sur une 
droite à une distance donnée (c'est en gros les axiomes que j'ai dans 
mon développement Coq)

Mais tout cela risque d'être bien compliqué par les conditions de non 
degenerescence, et je pense qu'il faut présenter les choses sous forme 
de théorèmes que si les théorèmes correspondant sont vrais. (faire 
attention aux conditions du style point alignés ou confondus etc)

> > Il y a pas
> > mal d'options en ce domaine, et des choses deja faites : le langage
> > geocaml, eukleides... Il y a de bonnes idees a prendre dans chacun, et
> > tout depend un peu de ce qu'on veut qu'une telle application soit
> > capable de faire.
> >    
>
> tout à fait d'accord, et des rapports inria intéressants également ;-)
>
>  

Est-ce que tu peux me donner des pointeurs vers ces rapports inria ?

>  
>
> > On peut maintenir deux projets separes dans Gna ? Ou bien faut-il
> > creer deux projets, plus un troisieme pour les eventuelles rencontres
> > de technologies ?
> >    
> Je viens juste de recevoir la confirmation du projet GeOCaml sur gna ...
> (on a déjà la liste geocaml-cvs ;-) là j'ai été un peu vite, j'eu du
> prendre un autre nom plus générique... cela dit, GeOCaml me semble
> générique non ? ;-)

cela me convient très bien.

> Ensuite, s'il y a des contribution/fusion, ça peut
> simplement se faire par modules/sous-répertoire
>
>  

je pense que c'est suffisant oui

> > de se placer au centre de l'univers ;-) : il devrait etre a la racine,
> > et se decliner en toutes les syntaxes possibles par des fichiers xslt.
> > Et AUSSI vers .geo ;-)
> >    
>
> Sauf que dans une optique pédagogique, il est plus facile de saisir du
> .geo. Mais sinon effectivement sur le principe xml devrait être au
> centre. Il y a juste un point d'entrée ex-centré, le .geo 
>
> Et définir un langage pseudo-naturel est en soit intéressant ;-)
>
>  
Peut-être que l'on devrait avoir deux outils d'un part  l'interface et 
d'autre part un outil ou une librairie de traduction qui pourait être 
distribuée de manière indépendante.
Cela permettrait de faciliter le codage car c'est plus modulaire et en 
plus on  peut espèrer obtenir des utilisateurs (voir même des 
contributeurs) au delà de geocaml, les gens de Kig, DrGeo, Kseg etc ...

- 1 - un outil qui permet de traduire des descriptions de figures d'un 
langage vers l'autre,

.geo / .cabri / .kig etc... -> AstCaml ->  .geoxml -> .coqxml / .phox /  
.svg / .ps / .latex / eukleide etc ...
                                          .coqxml   ->


- 2 - une interface graphique qui utilise 1 et qui permet de construire 
et de visualiser les figures interactivement.

Peut-être que l'on pourrait éditer la figure à la souris et en même en 
temps en mode texte les .geo ceci grâce à deux onglets un peu comme dans 
mozilla composer, voir même un troisième onglet avec une vue de la 
construction sous forme d'arbre.

> [c'est pas dans coq qu'on pouvait avoir les preuves en langage naturel
> ? ;-)]
>  

les gens de pcoq et de mowgli travaillent là dessus.

>  
>
> > PS : puis-je etre inscrit sur la liste address@hidden pour
> > faciliter les conversations ?
> >    
>
> ben je vais créer la liste analogue sur gna (geocaml-devel ?) ... et
> ensuite on fait comme ça
>
> A+
>
>  
enfin une petite question sur votre langage : est-ce qu'il est prevu de 
pouvoir fournir les coordonnées de points libres ?



A+