Recent Changes for "Front Page" - Coquille

Front Page

tcnsc — 2011-10-15 00:46:29

Revert to version 29.

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 49:	Line 49:
- [http://www.goodassur.com Un comparateur de mutuelles]

Front Page

2011-10-13 21:47:38

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 49:	Line 49:
	+ [http://www.goodassur.com Un comparateur de mutuelles]

Front Page

2011-04-06 13:32:12

Reverting spam/vandalism

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 12:	Line 12:
- Ceci est le wiki du [http://graal.ens-lyon.fr/coquille/ projet COQUILLE], développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE. [http://cv-writing-services.org.uk/ cv writing]	+ Ceci est le wiki du [http://graal.ens-lyon.fr/coquille/ projet COQUILLE], développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.
Line 49:	Line 49:
- 2. [http://essay-for.me/ online essays]

Front Page

2011-02-01 08:29:38

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 49:	Line 49:
	+ 2. [http://essay-for.me/ online essays]

Front Page

AndeyBox — 2011-01-24 14:45:56

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 12:	Line 12:
- Ceci est le wiki du [http://graal.ens-lyon.fr/coquille/ projet COQUILLE], développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.	+ Ceci est le wiki du [http://graal.ens-lyon.fr/coquille/ projet COQUILLE], développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE. [http://cv-writing-services.org.uk/ cv writing]

Front Page

JabberWokky — 2010-07-23 17:12:32

Revert to version 22 (spam).

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 16:	Line 16:
- Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-paper-writing.com/custom_essay_writing write my essay] du projet est plus adapté à une vue d'ensemble extérieure.	+ Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] du projet est plus adapté à une vue d'ensemble extérieure.

Front Page

homyak — 2010-07-19 17:47:55

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 16:	Line 16:
- Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-essay-writing-service.org/custom-research-papers.php do my research] du projet est plus adapté à une vue d'ensemble extérieure.	+ Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-paper-writing.com/custom_essay_writing write my essay] du projet est plus adapté à une vue d'ensemble extérieure.

Front Page

homyak — 2010-07-19 17:47:25

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 16:	Line 16:
- Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-paper-writing.com/custom_essay_writing write my essay] du projet est plus adapté à une vue d'ensemble extérieure.	+ Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-essay-writing-service.org/custom-research-papers.php do my research] du projet est plus adapté à une vue d'ensemble extérieure.

Front Page

homyak — 2010-07-19 17:46:06

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 16:	Line 16:
- Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] du projet est plus adapté à une vue d'ensemble extérieure.	+ Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] [http://custom-paper-writing.com/custom_essay_writing write my essay] du projet est plus adapté à une vue d'ensemble extérieure.

Front Page

WilliamLewis — 2010-07-19 16:14:57

Revert to version 19.

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 49:	Line 49:
- - == Links == - [http://cvresumewritingservices.org/professional-resume.php Professional resume service] - [http://customwritingservices.org/ writing services]

Front Page

fagot — 2010-07-05 20:36:03

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 52:	Line 52:
	+ *[http://customwritingservices.org/ writing services]

Front Page

fagot — 2010-07-01 10:32:07

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 49:	Line 49:
	+ + == Links == + *[http://cvresumewritingservices.org/professional-resume.php Professional resume service]

Front Page

2010-01-26 19:35:44

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 5:	Line 5:
	+ = =
Line 6:	Line 7:
	+ = =
Line 7:	Line 9:
	+ = Ancienne page d'accueil =

Front Page

2010-01-26 19:31:48

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 1:	Line 1:
	+ = Projet fini = + + Le projet COQUILLE est terminé. Il a donné naissance à deux projets annexes : [http://sourceforge.net/projects/coqtail/ COQTAIL] et [http://code.google.com/p/coquille/ COQUILLE / IDE]. + + + + +

Front Page

2009-12-14 19:45:20

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 1:	Line 1:
- Ceci est le wiki du projet COQUILLE, développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.	+ Ceci est le wiki du [http://graal.ens-lyon.fr/coquille/ projet COQUILLE], développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.

Front Page

madiot — 2009-12-06 16:01:51

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 5:	Line 5:
- Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page].	+ Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page]. Le [http://graal.ens-lyon.fr/coquille site officiel] du projet est plus adapté à une vue d'ensemble extérieure.
Line 24:	Line 24:
- Pour l'instant, c'est un peu dangereux et imprécis. - 1. ["Indécidabilité et heuristiques"] : état de l'art - 1. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? - 1. Réponses aux remarques : « Ça ne va jamais marcher ! »	+ 1. À partir d'exemples, génération d'un arbre de décision + 1. À partir de cet arbre, création d'une tactique
Line 30:	Line 28:
- 1. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) - 1. Affichage des formules (en LaTeX ou autre) (voir avec Yves Bertot) - 1. Un logiciel plus facile à utiliser ? Mais pour qui ? - 1. Indentation automatique (conserver au possible l'actuelle) ou forcée. - 1. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré)	+ Interface en Qt, avec quelques fonctionnalités supplémentaires.
Line 41:	Line 35:
- 1. Nom de projet (on l'a déjà, COQUILLE !) - 1. Site web. (coquille.ens-lyon.fr ? Ouaaa) - 1. Proposition de Yann : interface web pour le logiciel. (reste qu'il faudra faire un logiciel !) - 1. ... ?	+ 1. Site web : [graal.ens-lyon.fr/coquille graal.ens-lyon.fr/coquille] + 1. Communication interne + 1. Rapports

Front Page

2009-10-06 08:14:22

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 45:	Line 45:
- - = Workpackages obsolètes = - Qui sont là, temporairement, pour des raisons historiques. - - == Preuves de programmes == - Ce WP risque de ne pas exister, tant ça existe déjà. Attention, c'est un peu ce qui intéresse (vaguement) les entreprises. On peut regarder du côté de [http://why.lri.fr/ why], de [http://caduceus.lri.fr caduceus], qui est devenu obsolète et un autre projet apparaît ... Oh [http://frama-c.cea.fr un site chiadé du CEA]. - 1. Etat de l'art : au moins des exemples de bout de code prouvés ? ou seulement des lambda-termes ? - 1. Ça vous dit de mettre des monades ? - 1. ["Et du C"] ? -> why, caduceus. - - == Étude de faisabilité == - Ceci n'est plus vraiment un WP, il sera intégré dans "preuves". Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés. Certaines preuves sont difficiles pour des problèmes simples. (Le dm1 de preuves nous donne un exemple de propriétés de bijection qui se fait bien dans un sens mais moins bien dans l'autre) - - == Des idées, des remarques ? == - Reste-t-il des idées de workpackages ? C'est probablement le cas. Blâmez-moi (JM) mais faîtes-en. [Mention à supprimer le cas échéant]

Front Page

madiot — 2009-10-05 00:03:21

mise à jour de la liste des WP et nettoyage

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 4:	Line 4:
	+ + Le forum du développement du projet est disponible [http://perso.ens-lyon.fr/jeanmarie.madiot/coquille/forum sur cette page].
Line 14:	Line 16:
- == Formalisation des notions d'analyse et d'algèbre ==	+ == Preuves == + Il s'agira d'augmenter la liste des théorèmes qui existent dans stdlib (ou c-corn) n'hésitez pas à approfondir ou à élaguer la liste obsolète ci-dessous.
Line 34:	Line 37:
- Ltac est le langage de tactiques de coq. Il faut voir ce qu'il en est (état de l'art) et répondre aux questions : - 1. Peut-on utiliser Ltac pour créer de nouvelles tactiques - 1. Peut-on utiliser Ltac pour manipuler les preuves - 1. Peut-on utiliser Ltac ?	+ C'est l'idée originale, qui est ''l'aide aux prouveurs''. Comme Ltac est le langage de tactiques de coq, cette partie sera probablement codée en ltac. À approfondir, mais ce WP semble mieux défini à présent.
Line 39:	Line 39:
- == Preuves de programmes/fonctions == - Attention, c'est un peu ce qui intéresse (vaguement) les entreprises. On peut regarder du côté de [http://why.lri.fr/ why], de [http://caduceus.lri.fr caduceus], qui est devenu obsolète et un autre projet apparaît ... Oh [http://frama-c.cea.fr un site chiadé du CEA].	+ == Communication == + Diffuser les résultats, c'est très important. (On le verra bien, rien que dans l'état de l'art). Liste à compléter : + 1. Nom de projet (on l'a déjà, COQUILLE !) + 1. Site web. (coquille.ens-lyon.fr ? Ouaaa) + 1. Proposition de Yann : interface web pour le logiciel. (reste qu'il faudra faire un logiciel !) + 1. ... ? + + = Workpackages obsolètes = + Qui sont là, temporairement, pour des raisons historiques. + + == Preuves de programmes == + Ce WP risque de ne pas exister, tant ça existe déjà. Attention, c'est un peu ce qui intéresse (vaguement) les entreprises. On peut regarder du côté de [http://why.lri.fr/ why], de [http://caduceus.lri.fr caduceus], qui est devenu obsolète et un autre projet apparaît ... Oh [http://frama-c.cea.fr un site chiadé du CEA].
Line 43:	Line 53:
- 1. ["Et du C"] ?	+ 1. ["Et du C"] ? -> why, caduceus.
Line 46:	Line 56:
- Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés. Certaines preuves sont difficiles pour des problèmes simples. (Le dm1 de preuves nous donne un exemple de propriétés de bijection qui se fait bien dans un sens mais moins dans l'autre)	+ Ceci n'est plus vraiment un WP, il sera intégré dans "preuves". Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés. Certaines preuves sont difficiles pour des problèmes simples. (Le dm1 de preuves nous donne un exemple de propriétés de bijection qui se fait bien dans un sens mais moins bien dans l'autre)
Line 48:	Line 58:
- == ... ==	+ == Des idées, des remarques ? ==

Front Page

madiot — 2009-10-04 23:47:11

(quick edit)

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 33:	Line 33:
- == Ltac ==	+ == Tactiques ==

Front Page

matthieuP — 2009-10-03 20:01:38

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 20:	Line 20:
- == [Apprentissage] ==	+ == ["Apprentissage"] ==

Front Page

matthieuP — 2009-10-03 19:37:07

Ajout d'un lien sur apprentissage pour développer ce point

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 20:	Line 20:
- == Apprentissage ==	+ == [Apprentissage] ==

Front Page

2009-10-03 13:45:44

Small changes - gallais

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 15:	Line 15:
- 1. État de l'art : beaucoup, beaucoup de choses existent. ([http://flint.cs.yale.edu/cs428/coq/library/Coq.Reals.Rtopology.html youpi]) - 1. Fera-t'on du constructif ? Pour l'analyse, C-CoRN ?	+ 1. ["État de l'art"] : beaucoup, beaucoup de choses existent. + 1. Fera-t-on du constructif ? Pour l'analyse, C-CoRN ?
Line 18:	Line 18:
- 1. UP : Trouver des axiomes à éliminer (Gallais ?)	+ 1. ["UP"] : Trouver des axiomes à éliminer (Gallais ?)
Line 22:	Line 22:
- 1. Indécidabilité et heuristiques : état de l'art (?)	+ 1. ["Indécidabilité et heuristiques"] : état de l'art
Line 28:	Line 28:
- 1. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement)	+ 1. Affichage des formules (en LaTeX ou autre) (voir avec Yves Bertot)
Line 43:	Line 43:
- 1. Et du C ?	+ 1. ["Et du C"] ?
Line 49:	Line 49:
- Reste-t'il des idées de workpackages ? C'est probablement le cas. Blâmez-moi (JM) mais faîtes-en. [Mention à supprimer le cas échéant]	+ Reste-t-il des idées de workpackages ? C'est probablement le cas. Blâmez-moi (JM) mais faîtes-en. [Mention à supprimer le cas échéant]

Front Page

madiot — 2009-10-03 00:49:00

reformattage, quelques détails en plus

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 13:	Line 13:
- 1. Formalisation des notions d'analyse et d'algèbre - a. État de l'art : beaucoup, beaucoup de choses existent. ([http://flint.cs.yale.edu/cs428/coq/library/Coq.Reals.Rtopology.html youpi]) - a. Fera-t'on du constructif ? Pour l'analyse, C-CoRN ? - a. DOWN : Supposer des lemmes plus généraux pour paralléliser - a. UP : Trouver des axiomes à éliminer (Gallais ?) - 1. Apprentissage : pour l'instant, c'est dangereux et imprécis. - a. Indécidabilité et heuristiques : état de l'art (?) - a. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? - a. Réponses aux remarques : « Ça ne va jamais marcher ! » - 1. IDE - a. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) - a. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement) - a. Un logiciel plus facile à utiliser ? Mais pour qui ? - a. Indentation automatique (conserver au possible l'actuelle) ou forcée. - a. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré) - 1. Ltac (langage de tactiques) : état de l'art - a. Peut-on utiliser Ltac pour créer de nouvelles tactiques - a. Peut-on utiliser Ltac pour manipuler les preuves - a. Peut-on utiliser Ltac ? - 1. Preuves de programmes/fonctions (ce qui intéresse (vaguement) les entreprises) - a. Etat de l'art : au moins des exemples de bout de code prouvés ? ou seulement des lambda-termes ? - b. Ça vous dit de mettre des monades ? - c. Et du C ? - 1. Étude de faisabilité - a. Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés - 1. (...)	+ + == Formalisation des notions d'analyse et d'algèbre == + 1. État de l'art : beaucoup, beaucoup de choses existent. ([http://flint.cs.yale.edu/cs428/coq/library/Coq.Reals.Rtopology.html youpi]) + 1. Fera-t'on du constructif ? Pour l'analyse, C-CoRN ? + 1. DOWN : Supposer des lemmes plus généraux pour paralléliser + 1. UP : Trouver des axiomes à éliminer (Gallais ?) + + == Apprentissage == + Pour l'instant, c'est un peu dangereux et imprécis. + 1. Indécidabilité et heuristiques : état de l'art (?) + 1. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? + 1. Réponses aux remarques : « Ça ne va jamais marcher ! » + + == IDE == + 1. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) + 1. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement) + 1. Un logiciel plus facile à utiliser ? Mais pour qui ? + 1. Indentation automatique (conserver au possible l'actuelle) ou forcée. + 1. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré) + + == Ltac == + Ltac est le langage de tactiques de coq. Il faut voir ce qu'il en est (état de l'art) et répondre aux questions : + 1. Peut-on utiliser Ltac pour créer de nouvelles tactiques + 1. Peut-on utiliser Ltac pour manipuler les preuves + 1. Peut-on utiliser Ltac ? + + == Preuves de programmes/fonctions == + Attention, c'est un peu ce qui intéresse (vaguement) les entreprises. On peut regarder du côté de [http://why.lri.fr/ why], de [http://caduceus.lri.fr caduceus], qui est devenu obsolète et un autre projet apparaît ... Oh [http://frama-c.cea.fr un site chiadé du CEA]. + 1. Etat de l'art : au moins des exemples de bout de code prouvés ? ou seulement des lambda-termes ? + 1. Ça vous dit de mettre des monades ? + 1. Et du C ? + + == Étude de faisabilité == + Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés. Certaines preuves sont difficiles pour des problèmes simples. (Le dm1 de preuves nous donne un exemple de propriétés de bijection qui se fait bien dans un sens mais moins dans l'autre) + + == ... == + Reste-t'il des idées de workpackages ? C'est probablement le cas. Blâmez-moi (JM) mais faîtes-en. [Mention à supprimer le cas échéant]

Front Page

madiot — 2009-10-03 00:31:27

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 3:	Line 3:
- '''COQUILLE''' est l'acronyme de « Coq User-Interactive Library Learning Expert », mais ça ne veut pas dire grand chose, l'apprentissage de bibliothèques. (Si ?)	+ '''COQUILLE''' est l'acronyme de « Coq User-Interactive Library Learning Expert ». ["Acronyme" Pourquoi ?]
Line 6:	Line 6:
- 1. Faciliter l'utilisation de Coq pour la démonstration de propriétés mathématiques. - 1. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types. - 1. Encourager l'utilisation d'assistants de preuves dans les entreprises. - 1. Faire du coq	+ 1. Faciliter l'utilisation de Coq pour la démonstration de propriétés mathématiques. + 1. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types. + 1. Encourager l'utilisation d'assistants de preuves dans les entreprises. + 1. Faire du coq + 1. Augmenter la liste des propriétés démontrées en coq
Line 12:	Line 13:
	+ 1. Formalisation des notions d'analyse et d'algèbre + a. État de l'art : beaucoup, beaucoup de choses existent. ([http://flint.cs.yale.edu/cs428/coq/library/Coq.Reals.Rtopology.html youpi]) + a. Fera-t'on du constructif ? Pour l'analyse, C-CoRN ? + a. DOWN : Supposer des lemmes plus généraux pour paralléliser + a. UP : Trouver des axiomes à éliminer (Gallais ?) + 1. Apprentissage : pour l'instant, c'est dangereux et imprécis. + a. Indécidabilité et heuristiques : état de l'art (?) + a. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? + a. Réponses aux remarques : « Ça ne va jamais marcher ! » + 1. IDE + a. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) + a. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement) + a. Un logiciel plus facile à utiliser ? Mais pour qui ? + a. Indentation automatique (conserver au possible l'actuelle) ou forcée. + a. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré)
Line 16:	Line 32:
- 1. Formalisation des notions d'analyse et d'algèbre, ... en coq : état de l'art	+ 1. Preuves de programmes/fonctions (ce qui intéresse (vaguement) les entreprises) + a. Etat de l'art : au moins des exemples de bout de code prouvés ? ou seulement des lambda-termes ? + b. Ça vous dit de mettre des monades ? + c. Et du C ?
Line 19:	Line 38:
- 1. Apprentissage - a. Indécidabilité et heuristiques : état de l'art (?) - a. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? - 1. IDE - a. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) - a. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement) - a. Un logiciel plus facile à utiliser ? Mais pour qui ? - a. Indentation automatique (l'actuelle est à garder en partie) ou forcée. - a. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré)

Front Page

madiot — 2009-10-02 23:53:08

+latex, reformulations

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 7:	Line 7:
- 2. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types. - 3. Encourager l'utilisation d'assistants de preuves dans les entreprises. - 4. Faire du coq	+ 1. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types. + 1. Encourager l'utilisation d'assistants de preuves dans les entreprises. + 1. Faire du coq
Line 16:	Line 16:
- 1. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art	+ 1. Formalisation des notions d'analyse et d'algèbre, ... en coq : état de l'art + 1. Étude de faisabilité + a. Étant donnés (autant que l'on veut) certains théorèmes d'analyse, prouver quelques propriétés
Line 21:	Line 23:
- a. CoqIde : ce qu'il manque vraiment - a. Un logiciel plus facile à utiliser ? - a. Indentation automatique (l'actuelle est à garder en partie) ou forcée - a. Structuration du code	+ a. CoqIde : ce qu'il manque vraiment (~ état de l'art et sondage des forums / mailing lists) + a. Affichage des formules (en LaTeX ou autre ~ état de l'art, ça existe probablement) + a. Un logiciel plus facile à utiliser ? Mais pour qui ? + a. Indentation automatique (l'actuelle est à garder en partie) ou forcée. + a. Structuration du code (forcée ? Une preuve est souvent imbuvable, et même si ce n'est que des tactiques, ça peut être structuré)

Front Page

madiot — 2009-10-02 23:37:23

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 13:	Line 13:
- a. Peut-on utiliser Ltac pour créer de nouvelles tactiques - b. Peut-on utiliser Ltac pour manipuler les preuves - c. Peut-on utiliser Ltac ? - 2. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art - 3. Apprentissage - a. Indécidabilité et heuristiques : état de l'art (?) - b. Une tactique DOIT être déterministe : vrai logiciel au dessus de coq(ide) ? - 4. IDE - a. CoqIde : ce qu'il manque vraiment - b. Un logiciel plus facile à utiliser ? - c. Indentation automatique (l'actuelle est à garder en partie) ou forcée - d. Structuration du code - 5. (...)	+ a. Peut-on utiliser Ltac pour créer de nouvelles tactiques + a. Peut-on utiliser Ltac pour manipuler les preuves + a. Peut-on utiliser Ltac ? + 1. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art + 1. Apprentissage + a. Indécidabilité et heuristiques : état de l'art (?) + a. Une tactique doit être déterministe donc l'apprentissage en est (presque) exclus : vrai logiciel au dessus de coq(ide) ? + 1. IDE + a. CoqIde : ce qu'il manque vraiment + a. Un logiciel plus facile à utiliser ? + a. Indentation automatique (l'actuelle est à garder en partie) ou forcée + a. Structuration du code + 1. (...)

Front Page

madiot — 2009-10-02 23:30:06

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 12:	Line 12:
- 1. Ltac (langage de tactiques) : état de l'art - A. Peut-on utiliser Ltac pour créer de nouvelles tactiques - B. Peut-on utiliser Ltac pour manipuler les preuves - C. Peut-on utiliser Ltac ? - 2. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art - 3. Apprentissage - A. Indécidabilité et heuristiques : état de l'art (?) - B. Une tactique DOIT être déterministe : vrai logiciel au dessus de coq(ide) ? - 4. IDE - A. CoqIde : ce qu'il manque vraiment - B. Un logiciel plus facile à utiliser ? - C. Indentation automatique (l'actuelle est à garder en partie) ou forcée - D. Structuration du code - 5. (...)	+ 1. Ltac (langage de tactiques) : état de l'art + a. Peut-on utiliser Ltac pour créer de nouvelles tactiques + b. Peut-on utiliser Ltac pour manipuler les preuves + c. Peut-on utiliser Ltac ? + 2. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art + 3. Apprentissage + a. Indécidabilité et heuristiques : état de l'art (?) + b. Une tactique DOIT être déterministe : vrai logiciel au dessus de coq(ide) ? + 4. IDE + a. CoqIde : ce qu'il manque vraiment + b. Un logiciel plus facile à utiliser ? + c. Indentation automatique (l'actuelle est à garder en partie) ou forcée + d. Structuration du code + 5. (...)

Front Page

madiot — 2009-10-02 23:28:21

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 10:	Line 10:
	+ + = Workpackages = + 1. Ltac (langage de tactiques) : état de l'art + A. Peut-on utiliser Ltac pour créer de nouvelles tactiques + B. Peut-on utiliser Ltac pour manipuler les preuves + C. Peut-on utiliser Ltac ? + 2. Formalisation des notions d'intégration, de calcul, ... en coq : état de l'art + 3. Apprentissage + A. Indécidabilité et heuristiques : état de l'art (?) + B. Une tactique DOIT être déterministe : vrai logiciel au dessus de coq(ide) ? + 4. IDE + A. CoqIde : ce qu'il manque vraiment + B. Un logiciel plus facile à utiliser ? + C. Indentation automatique (l'actuelle est à garder en partie) ou forcée + D. Structuration du code + 5. (...)

Front Page

madiot — 2009-10-02 23:11:25

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 10:	Line 10:
- - == Quick Start Guide! == - 1. First read the rest of this page! - 2. If you haven't already, read the [wiki:wikispot:"Wiki Creator Guide"] and [wiki:wikispot:"Wiki Guide"]. - 3. Go to ["Wiki Settings"] and change the settings for your wiki! - 4. Click the edit button up top of this page and create your new front page. - 5. Start adding content to your wiki and read about [wiki:wikispot:"building community"] - 6. Tell your friends, family, acquaintances, enemies, multiple personalities, etc. - 7. Celebrate! - - == Default Pages Included With Your Wiki == - - * ["All Pages"] is an automatically generated list of all the pages in your wiki. - * ["Bookmarks"] is for your bookmarks on this wiki. Every user has his/her own bookmarks page based on what they choose to bookmark on this wiki. To bookmark a page, simply click "Bookmark" at the bottom of the page! ([wiki:wikispot:"Interwiki Bookmarks"] on wikispot shows you all of your bookmarks on all wikis.) - * ["Front Page"] is the page you're currently viewing. - * ["Events Board"] is a page where anyone can post events in the community. - * ["Help"] links to the main help pages on wikispot -- useful for reference. - * ["Interwiki Map"] -- link to non-Wiki Spot wikis using [wiki:wikispot:"interwiki links"] by adding names and URLs of wikis to this page. - * ["Orphaned Pages"] contains an automatically generated list of pages with no links to them. Ideally, this page should be empty -- keep your wiki well-linked! - * ["Outgoing Links"] lists all pages sorted by the number outgoing links on each page. This provides a good place to start if you're feeling [wiki:c2:"WikiGnome" gnomeish] and want to link-up some pages with few to no links. - * ["Quick Wiki Tips"] -- At the top of ["Recent Changes"] shows randomly selected tips from this page. - * ["Recent Changes"] shows all the recent activity on the wiki in a given time period. This page lets everybody see what's happening in your wiki! ([wiki:wikispot:"Interwiki Recent Changes"] on wikispot shows you the recent changes on all the wikis you're watching.) - * ["Random Pages"] is a randomly generated list of twenty-five pages. Good for finding pages to edit once your wiki grows large. - * ["Site Organization"] has links to pages that help you keep your wiki well organized. - * ["Templates"] is a user created list of template pages -- pages that you can use as starting blocks for making new pages. ["Templates/Business"] is there just to give you an idea of what a template should be. - * ["User Statistics"] is a page that displays statistics, such as the number of edits, for each person who's edited your wiki. - * ["Wanted Pages"] contains all the pages that are linked to, but do not yet exist. This is another good place to start [wiki:c2:"WikiGnome" gnomeing]. - * ["Wiki Sandbox"] is a place for users to play around with the wiki without disturbing your content. - * ["Wiki Settings"] contains the administrative settings for your wiki. - * ["Wiki Settings/CSS"] is the page where you can upload different style sheets that change your wiki's appearance. - * ["Wiki Settings/General"] contains general settings for your wiki. - * ["Wiki Settings/Images"] allows you to customize images on your wiki, such as your logos. - * ["Wiki Settings/Security"] lets you change the default security settings of your wiki and create user groups to control access. - - = Making new pages! = - To create a new page, simply search for the name of the page you wish to create and then click the "Create a new page with this title" link. Another way to create a new page is by making a link to the page you wish to create from a page that already exists, following the link, and clicking "Create this page."

Front Page

madiot — 2009-10-02 23:06:08

Differences for Front Page

Deletions are marked with - .	Additions are marked with +.
Line 1:	Line 1:
- Welcome to your new wiki! This is your wiki's Front Page. So what do you do now?	+ Ceci est le wiki du projet COQUILLE, développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.
Line 3:	Line 3:
- = Quick Start Guide! =	+ '''COQUILLE''' est l'acronyme de « Coq User-Interactive Library Learning Expert », mais ça ne veut pas dire grand chose, l'apprentissage de bibliothèques. (Si ?) + + = Buts = + 1. Faciliter l'utilisation de Coq pour la démonstration de propriétés mathématiques. + 2. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types. + 3. Encourager l'utilisation d'assistants de preuves dans les entreprises. + 4. Faire du coq + + == Quick Start Guide! ==
Line 12:	Line 20:
- = Default Pages Included With Your Wiki = - This is a simple list of of all pages included with your wiki. You will hopefully create many, many more!	+ == Default Pages Included With Your Wiki ==