aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
Commit message (Collapse)AuthorAge
...
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
| | | | | | | | | | | | | * Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
| | | | | | | We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | | | | | | | | | - We now use create_process instead of open_process, and stores the answered pid. - The "Stop" button now sends a Sigint signal to this coqtop pid. - The "Goto Start" button now works even if a computation is ongoing, a new process is spawned and the previous one is killed -9, and then a waitpid is done to avoid having zombies around. Note that currently a vm_compute won't be stopped by a "Stop", but only by a "Goto Start". This can be quite confusing. How to properly document that "Goto Start" has the side effect of being a kill ? Maybe we could check someday if the Ctrl-C has been successful, and kill -9 if not ? Or maybe make coqide aware of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C in this case ? TODO: - for the moment a forced "Goto Start" displays an unfriendly anomaly - check if all this works under Windows (probably but not sure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted r13715 "Add improved indenters that rely on the current proof state ↵Gravatar gmelquio2011-01-06
| | | | | | | | to choose the indentation depth." It seems to be the cause for bug #2472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add improved indenters that rely on the current proof state to choose the ↵Gravatar gmelquio2010-12-14
| | | | | | | | | | indentation depth. Patch by Cedric Auger. These two indenters need to be exercised a bit to see if they are actually useful to users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved error messages in CoqIDE:Gravatar herbelin2010-11-07
| | | | | | | | | | | - add a check that coqtop can be run before starting the interface - returns the error message in case of problem - made illegal option message more informative - use coqtop.byte when coqide.byte (is it a good heuristic?) - made debugging messages silent by default in ide/undo.ml (Ctrl-C was calling Pervasives.prerr_endline instead of Ideutils.prerr_endline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13627 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
| | | | | | | | | | Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Robustness fix : clean restart of coqtop on pipe error + force matchingGravatar vgross2010-07-05
| | | | | | of coqtop return codes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stronger checks on coqtop termination, warning when zombies.Gravatar vgross2010-07-05
| | | | | | Also, reindentation + typed_notebook simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13241 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing error message display.Gravatar vgross2010-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13082 85f007b7-540e-0410-9357-904b9bb8a0f7
* added -args option to coqide to pass options to coqtopsGravatar vgross2010-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13046 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE goes multiprocessGravatar vgross2010-05-31
| | | | | | | | | | | | | | | This commit changes many things in CoqIDE, and several breakage are to be expected. So far, evaluation in standard tactic mode and backtracking seems to be working. Future work : - clean up the thread management crud remaining in ide/coqide.ml - rework the exception handling - rework the init system in Coqtop plus many other things git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
| | | | | | Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
| | | | | | Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing types to reflect futur separation between toplevel and ide.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goal generation deported into ide/coq.ml, single function to obtainGravatar vgross2010-03-23
| | | | | | all current goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
* New functions for goals fetching.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12877 85f007b7-540e-0410-9357-904b9bb8a0f7
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
| | | | | | Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a dual stack setupGravatar vgross2010-02-26
| | | | | | | The first stack lives in coqide and tracks the tagging and locking, the second lives in coq and tracks the commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12822 85f007b7-540e-0410-9357-904b9bb8a0f7
* New API for backtracking.Gravatar vgross2010-02-26
| | | | | | | Aside the command stack, the only parameter is the number of step to go back. Went back and forth without sync losses on tests-suite/ide/undo.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redispatch of printing tweaking hooks.Gravatar vgross2010-02-26
| | | | | | | We want to tweak the printing options when we want to display the results, not when we are evaluating vernac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify backtrackingGravatar vgross2010-02-12
| | | | | | | As we can now jump right onto a closed segment, there is no need for complicated pattern matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring of the printing optionsGravatar vgross2010-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
| | | | | | | This reverts commit 8162ee31152eb2f99af724e88a7e15a899c17811. Not the smartest thing to do on the verge of tagging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolation of proof-displaying codeGravatar vgross2010-01-11
| | | | | | | | | | The formatting logic is now isolated in ide/proofBrowser.ml, and the goal printing logic is deported inside ide/coq.ml. Also, the proof mode special printing has been cut out. Finally, turn every call to show_goals_full into show_goals, and use show_goals_full as the body of show_goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deport the backtracking code out of the ideGravatar vgross2009-12-11
| | | | | | | Backtracking code now lies entirely into ide/coq.ml. Datatypes have been tweaked to easen the separation to come. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
| | | | | | | | | This reverts commit 12537 This reverts commit 12199 This reverts commit 12198 This reverts commit 12172 (introduced the bug) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
| | | | | | | | into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
| | | | | | This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
| | | | | | ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* clearing unused functionsGravatar vgross2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
| | | | | | | | is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial simplification of undo mechanism, relying only on Courtieu'sGravatar herbelin2009-06-07
| | | | | | | marks and no longer on old-fashioned reset to id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12172 85f007b7-540e-0410-9357-904b9bb8a0f7
* keeping interface synch'edGravatar vgross2009-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12144 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: 2 problèmes de undo encore:Gravatar herbelin2008-06-13
| | | | | | | | | | | | - dans le "replay", l'état n'était pas correctement sauvegardé d'où une perte d'efficacité en cas de rejeux répétés, - bug de synchronisation dans le calcul de la pile des lemmes ouverts. + réajout de la variante standard de Set Printing All dans le menu display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plutôt que de reposer sur le vernacexpr pour détecter les débuts deGravatar herbelin2008-06-11
| | | | | | | | | | buts, on se base sur les informations de Pfedit (comme le fait Pierre Courtieu). Permet d'être plus robuste sur les extensions de syntaxe ouvrant des buts, style Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
* On prend des risques en tentant d'optimiser encore plus le undo en casGravatar herbelin2008-06-09
| | | | | | | | de preuves imbriquées. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11078 85f007b7-540e-0410-9357-904b9bb8a0f7
* - On adopte finalement la méthode de Pierre Courtieu pour le undo deGravatar herbelin2008-06-06
| | | | | | | | | | | | proof general (caractérisation des undos comme triplet d'un nombre de Undo, n'un nombre de Abort et d'un Reset vers un état/id). C'est plus simple et cela permet en plus d'avoir des buts imbriqués. Au passage, "goto point" se comporte comme une suite de "one step back". - Quelques bricoles sur la fenêtre préférences de Shortcuts. - Quelques réorganisations autour du menu Display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deGravatar herbelin2008-05-28
| | | | | | | | coq (mais ça ne rend pas très bien -- faudrait centrer l'image) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation des points d'appui du undo de CoqIDE (type reset_info).Gravatar herbelin2008-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10990 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
| | | | | | | | | | l'affichage des instances des evars. - Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté l'affichage des implicites, coercions, notations, etc dans CoqIDE (reste à trouver des icônes appropriées !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10983 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
| | | | | | | | | | | améliorer l'efficacité du undo. Restent les Qed et les End dont le undo peut nécessiter de rejouer un segment arbitrairement complexe (pour le undo du Qed, il faudrait typiquement que Coq se souvienne de l'entrelacement de déclarations et de tactiques). - Code mort concernant les mots-clés dans coq.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la colorisation, du backtrack et des messages de CoqIDEGravatar herbelin2008-05-10
| | | | | | | | | | | | | | | | | | | - Colorisation: - on ne colorie que les noms de commandes que si en début de phrase (par exemple: Definition F := fun Local => Local) ne colorie pas Local), - ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset sont uniformément mis en valeur). - Backtracking: résolution bug #1538 et réactivation de la possibilité de déclarer des défs, types, etc pendant une session de preuve. En revanche, il n'est pas clair que cela fonctionne bien avec le mode déclaratif. - Messages d'erreur : on ne capture la sortie de coq qu'après l'initialisation pour que les erreurs d'initialisation soit affichées (cf bug #1424 and item 5 of #1123). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Suppression d'une source de fuite mémoire dans declare_mod.ml (la table de hash library_table n'était pas synchronisée avec le reset et elle grossissait à chaque rejeu de la session; utilisation au passage d'une map pour que la synchronisation avec le reset soit plus rapide). [mod_typing.ml] - Correction d'un bug de synchronisation pour le niveau pattern 200. [pcoq.ml4] - Suppression d'un vieux reste du traducteur [constructeur VernacVar] - Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de chacune des commandes vernaculaires par l'utilisation d'une fonction d'assignation d'attributs à chaque commande vernac. Correction de ce qui semble être des bizarreries (VernacDeclareTacticDefinition considéré comme ouvrant un but; suppression des "loc" dans les Reset: ne pouvait pas faire fonctionner correctement update_on_end_of_segment). Suppression de la nécessité d'expliciter si une commande retourne des messages dépendants du mode "verbose" (on suppose que chaque commande sait ce qu'elle doit dire selon la position du flag verbose). Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne sait revenir qu'aux états associés à des noms et cela ne vaut pas l'approche de Proof General. Il sera sans doute opportun de se brancher sur l'architecture de Pierre Courtieu à base de "Backtrack". La restriction des buts imbriqués a-t-elle vraiment une raison d'être ? En plus les commandes non cablées en dur comme Next Obligation ne sont pas prises en compte. Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours. Réparation approximative de l'option "Help for Keyword" de Coqide mais encore à faire pour plus de robustesse (makefile, installation, synchronisation entre la version du fichier index_urls.txt et la version du refman, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10904 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin des conclusions multiplesGravatar corbinea2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:04:42 +0000