aboutsummaryrefslogtreecommitdiff
path: root/ide/coq.ml
AgeCommit message (Collapse)Author
2010-02-26New backtracking code + fix bug #2082.vgross
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
2010-02-26Introducing a dual stack setupvgross
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
2010-02-26New API for backtracking.vgross
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
2010-02-26Redispatch of printing tweaking hooks.vgross
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
2010-02-12Simplify backtrackingvgross
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
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
Coq use case are mostly thoses : - parsing a char stream to get a vernac expr - evaluating a vernac expr with backtracking - turning a knob with a vernac expr, no backtracking - loading an entire file - compiling an entire file - backtracking (no clean API for this yet) - peeking Coq state info (no clean API for this yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-12Refactoring of the printing optionsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12755 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-11Revert "Isolation of proof-displaying code"vgross
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
2010-01-11Isolation of proof-displaying codevgross
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
2009-12-11Deport the backtracking code out of the idevgross
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
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib ↵letouzey
Interface the ProtectedLoop feature was used only by CoqInterface. Idem for stuff in Line_oriented_parser git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1vgross
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
2009-11-19Refactoring of coqide backtrack code, with the intent to put everythingvgross
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
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Integrate a few improvements on typeclasses and Program from the equations ↵msozeau
branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-29kills the old backtracking framework and replaces it withvgross
ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-03Added "etransitivity".herbelin
Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22remove some unused functions (which are part of a soon-to-be obsoletevgross
framework anyway) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-07Partial simplification of undo mechanism, relying only on Courtieu'sherbelin
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
2009-05-27dead code pruningvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12143 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-13minor bugfixes. CoqIde development will resume soon now ...vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12124 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-07- per session coq command stackvgross
- removed circular dependency between record and class used to keep track of sessions => no need for mutable option in record. - more 'a option ref pruning - more code splitting - more alpha-rewriting git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-06fixed groebner as a plugin + pattern matching Timeoutbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11967 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-04Temporary hack to make coqide.byte work (backport r11948) (see #2062)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11957 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-17DISCLAIMERpuech
========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵notin
dans le configure introduit par les révisions 11754 et 11755 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
guessing the binding name by default and making all generalized variables implicit. At the same time, continue refactoring of Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The AST is not completely satisfying, but leaning towards Record/Class as restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies are either of the form [meth : type] or [{ meth : type ; ... }], distinguishing singleton "definitional" classes and inductive classes based on records. The constructor syntax is accepted ([meth1 : type1 | meth1 : type2]) but raises an error immediately, as support for defining a class by a general inductive type is not there yet (this is a bugfix!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-28Native "Declare ML Module" when possibleglondu
Dynlink.add_{interfaces,available_units} are deprecated and not implemented natively. Currently, native "Declare ML Module" doesn't work because of this. Dynlink-related should be switched to the API introduced in OCaml 3.07. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
induction test-suite script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18- Rebranchement backtrack du langage déclaratif dans Coqideherbelin
- Divers: message d'erreur et typo relatifs au langage déclaratif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-10Bug résiduel du backtrack de coqide se produisant lorsque la limite deherbelin
la pile de undo de tactique est atteinte (il ne fallait pas oublier de faire un abort). On en profite pour porter cette limite à une valeur significativement plus élevée. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11219 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-01Encore une suite au 11188/11193 (c'était pas un bon jour)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11195 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-13CoqIDE: 2 problèmes de undo encore:herbelin
- 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
2008-06-11Plutôt que de reposer sur le vernacexpr pour détecter les débuts deherbelin
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
2008-06-09On prend des risques en tentant d'optimiser encore plus le undo en casherbelin
de preuves imbriquées. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11078 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06- On adopte finalement la méthode de Pierre Courtieu pour le undo deherbelin
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
2008-05-30- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"herbelin
n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deherbelin
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
2008-05-26Réorganisation des points d'appui du undo de CoqIDE (type reset_info).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10990 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Bug undo CoqIDE sur Endherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10985 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 06:46:10 +0000