Re:[GeOCaml]news

[LECLERCQ Régis]

> >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).
Mais dans ce cas il me semble qu'il faudrait donner les objets de base que 
nous utilisons (points, angles?,....) . 
> 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
ouai, mais tout n'est pas constructible a la regle et au 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)
Ca serait interessant de pouvoir lire les axiomes...
> 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. 
il me semble qu'on pourrait justement distinguer par exemple le triangle 
aplati ou le parallelogramme aplati (certaines proprietes restent vraies...); 
ce sont des cas particuliers qu'on etudie avec les eleves!Evidemment moi je 
me place d'un point vu matheux et enseignant de maths, c'est peut etre pas si 
facile a mettre en oeuvre, je le reconnais.
> (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 ;-)
tout a fait d'accord pour celui que georges et arnaud m'ont prete!
> 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. 
Je confirme! L'idee est de faire en sorte que les eleves saisissent un texte a 
partir d'une figure par exemple deja faite et de la refaire avec une syntaxe 
claire, mathematique et soignée! C'est un exemple de sequence derivee de la 
dictee au maitre. La generation de figures plus ou moins aleatoires permettra 
de degager les invariants de la figure, ce qui est un theme riche en 
geometrie! 
> >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 me semble coherent
> 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+

Cordialement,
Regis

> _______________________________________________
> GeOCaml-contact mailing list
> address@hidden
> http://mail.nongnu.org/mailman/listinfo/geocaml-contact