Re: [GeOCaml] news

[Julien Narboux]

Rebonjour,

Je vais peut-être lancer la discussion en resumant rapidement mon projet 
: (désolé pour les redondances pour ceux à qui j'en ai déjà parlé)

Je suis en thèse dans l'équipe Logical (http://logical.inria.fr) qui 
developpe Coq (http://coq.inria.fr), je travaille sur la formalisation 
et l'automatisation des preuves en géométrie.
J'ai commencé par implémenter la méthode de démonstration automatique de 
Chou Gao Zhang en Coq.
Je veux travailler sur une interface géométrique pour la géométrie afin 
de pouvoir saisir et visualiser les énnoncés de théorèmes.
(et eventuellement des étapes de la démonstration)
Pour cela j'avais envie de developper un plugin pour CoqIde (un 
interface graphique pour Coq écrite en Ocaml + lablgtk2).
Je travaille aussi avec Frédérique Guilhot, nous projetons de combiner 
son developpement Coq et le mien afin de pouvoir insérer des étapes 
automatiques au sein de preuves écrites à la main, dans une optique 
pédagogique.

Dans un premier temps, je pense qu'il serait plus simple de se 
concentrer sur la réalisation d'une application fonctionnelle de 
géométrie interactive avant de lier le tout à Coq et Phox. Je pense que 
c'est une bonne idée de faire des ponts vers plusieurs prouveurs et que 
ce n'est pas très compliqué à faire, la logique sous jacente aux 
raisonnements géométriques est très simple et facilement formalisable 
dans tous les prouveurs, il suffit me semble-t-il  de se mettre d'accord 
sur un langage. On a déjà fait du travail dans ce sens avec Frédérique 
Guihlot.

Pour DrGeoCaml et GeoCaml, je pense que lorsque le site sur gna sera 
disponible on pourra mettre les deux applications dans un même cvs et 
commencer à réunir les deux mais pour l'instant j'ai envie de continuer 
un peu à developper l'interface de DrGeoCaml et intégrer des 
fonctionnalités de GeoCaml par tout petits morceaux peut être en 
commençant par :
- la gestion des .deb et des rpms
- la lecture des fichiers .geo

Peut être on pourrait faire un bilan de ce qui existe dans les deux 
applications et faire un TODO en même temps.
Notation : un x si c'est géré et un - sinon.

Je vous laisse remplacer les ? par des "x" ou des "-" et rajouter les 
rubrique qu'il faut.

DrGeoCaml / GeoCaml

[x]/[?] - points libre
[x]/[?] - points sur cercle
[x]/[?] - points sur droites
[x]/[?] - points milieu
[x]/[?] - segments
[x]/[?] - vecteurs
[x]/[?] - droites deux points
[x]/[?] - droites paralleles
[x]/[?] - droites orthogonales
[x]/[?] - intersection droites, cercle/droite, cercles
[x]/[?] - cercles centre point
[x]/[?] - cercles diamètre

[x]/[?] - translation
[x]/[?] - symétrie centrale
[x]/[?] - symétrie axiale
[-]/[?] - homothetie
[-]/[?] - rotation

[-]/[?] - labels noms
[-]/[?] - labels distances
[-]/[?] - labels angles
[-]/[?] - labels coordonnées
[-]/[?] - labels équations

[-]/[?] - labels faits géométriques (ex: être alignés) (calculés sur la 
figure)
[-]/[?] - labels faits géométriques démontrés (ex: être alignés) 
(démontrés automatiquement)

[x]/[?] - déplacement d'un point libre et mise à jour en temps réel

[x]/[?] - mécanisme de séléction
[x]/[?] - gestion des objets cachés ou pas
[x]/[?] - suppression d'objets

[x]/[?] - zoom, deplace du cadre
[x]/[?] - attributs : couleur, style, epaisseur, nom

[x]/[?] - interface graphique
[x]/[?] - mode plein écran

[-]/[?] - faire changer le pointeur de la souris suivant le contexte
[-]/[?] - un clique milieu fait cycler entre les modes selection, 
deplacement et creer un objet (le dernier mode de créatio
n utilisé)

[-]/[?] - un double clique pour faire un point libre
[-]/[?] - selectionner les objets cachés
[-]/[?] - selectionner tous les objets visibles etc ...
gérer des couches, chaque objet appartient à une couche
[-]/[?] - les couches peuvent être visibles ou cachées
[-]/[?] - les couches ont des couleurs, selon une option afficher les 
objets de la couleur de la couche ou avec leur couleu
r réelle
[-]/[?] - que la séléction ne puisse pas se confondre avec une mise en 
couleur, genre mettre en valeur l'objet avec un halo
comme dans eukleide sous windows
[-]/[?] - gérer l'internationnalisation
[-]/[?] - gérer l'export eukleide, metapost
[-]/[?] - gérer l'import Kig, Cabri, Dr Geo, geoplan ... ?
[-]/[?] - gérer nouveau, ouvrir, enregistrer
[-]/[?] - demander la confirmation avant de supprimer des objets
[-]/[?] - faire une boite de dialogue d'astuces au démarrage
[-]/[?] - rajouter les macros
[-]/[?] - gérer les lieux géométriques et les coniques
[-]/[?] - pouvoir visualiser un arbre des dépendances entre les objets, 
ainsi que leurs attributs (epaisseur, couleur, nom,
style, ...)
[-]/[?] - pouvoir selectionner les points libres
[-]/[?] - mettre en valeur les points libres quand on utilise l'outil de 
deplacement
[-]/[?] - exporter vers svg ? ou bien faire carrement le rendu en svg 
pour beneficier de l'antialiasing, de la transp
arence etc...
[-]/[?] - faire du double buffering si je garde la version "drawable", 
pour eviter que cela clignote
[-]/[?] - avoir un outil pour faire glisser la feuille de papier
[-]/[x] - exporter vers latex / ps
[-]/[?] - pouvoir imprimer
[-]/[?] - faire une boite de dialogue a propos
[-]/[x] - faire une doc
[-]/[x] - gestion des .deb


Maintenant ce qui a un lien avec Coq :

[-]/[-] - pouvoir selectionner un théorème de géometrie en Coq dans 
CoqIde, exprimé  avec des "let" et des noms de définiti
ons que j'aurai standardisé, et que la figure se dessine dans une autre 
fenêtre (ou un tab).
[-]/[-] - que le but du théorème s'affiche en une couleur et les 
hypothese en d'autres,
par exemple si le but est de prouver qu'un point est un milieu, le 
mettre en rouge et mettre des marques pour dire
que les deux segments sont de même longueur en rouge aussi, mettre un 
petit carré si on sait que deux droites sont
perpendiculaire
[-]/[-] - d'avoir un menu "fait" pour pouvoir saisir un fait géométrique 
au moyen de la souris quand on a fini la figure :
par exemple trois point alignes, on selectionne les trois points et on 
les affiche en rouge, et ca genere en coq le
predicat
(Aligne A B C)
[-]/[-] - que la figure se mette a jour quand un nouveau point est 
rajouté pendant la preuve
[-]/[-] - permettre de se restreindre aux constructions a la regle et au 
compas , etc ...
[-]/[-] - générer une preuve d'existence de construction, grâce à la 
saisie de la construction graphiquement par l'utilisat
eur.
[-]/[-] - que l'utilisateur puisse construire un point graphiquement et 
celui si apparait dans le contexte Coq.

A bientôt

Julien