aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Collapse)AuthorAge
* Flag ide_slave moved into Flags moduleGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
* minor cleanup in coqtop.mlGravatar letouzey2013-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqtop -compile : avoid saving init state when compiling just one fileGravatar letouzey2013-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove deprecated option -no-hash-consing (currently doing nothing)Gravatar letouzey2013-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dir_path --> DirPathGravatar letouzey2013-02-19
| | | | | | | | Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed parsing of -no-native-compiler flag.Gravatar mdenes2013-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using library string functions.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
| | | | | | This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restoring flush of Welcome message lost in r15148Gravatar herbelin2012-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Another GC testGravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed the modification of the GC pressure coefficient, in orderGravatar ppedrot2012-11-12
| | | | | | to see if that really changes anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15958 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq is a heavy user of persistent data structures and symbolic ASTs, so theGravatar ppedrot2012-11-06
| | | | | | | | | | minor heap is heavily sollicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major heap increment and the GC pressure coefficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15953 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid [Loading ML file ...] messages when launching coqtopGravatar letouzey2012-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use fully-qualified Coq.Init.Prelude when starting coqtopGravatar letouzey2012-08-24
| | | | | | | This avoids interferences with another Prelude.v around (cf. Orsay/Random) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15765 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* verbose compat notations : nicer option nameGravatar letouzey2012-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Colorization of coqtop messages is turned *off* by defaultGravatar letouzey2012-06-07
| | | | | | | | | | | | | This bling-bling feature is interacting badly with - the documentation generation - the bench logs - compilation in an emacs buffer - ... As long as these points aren't solved, no coloring by default, but on the contrary an option to manually activate it: coqtop -color git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing some str with strbrkGravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a color output to Coqtop.Gravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed printing error problem... A line had disappeared in a previous patch.Gravatar ppedrot2012-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Flushing formatters before program exit.Gravatar ppedrot2012-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
| | | | | | Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Migrate the backtracking code from ide_slave.ml into a new backtrack.ml. In particular the history stack of commands that used to be there is now non-coqide-specific. ** Adapted commands ** - "Show Script": a basic functional version is restored (and the printing of scripts at Qed in coqtop). No indentation, one Coq command per line, based on the vernac_expr asts recorded in the history stack, printed via Ppvernac. - "Back n" : now mimics the backtrack of coqide: it goes n steps back (both commands and proofs), and maybe more if needed to avoid re-entering a proof (it outputs a warning in this case). - "BackTo n" : still try to go back to state n, but it also handles the proof state, and it may end on some state n' <= n if needed to avoid re-entering a proof. Ideally, it could someday be used by ProofGeneral instead of the complex Backtrack command. ** Compatible commands ** - "Backtrack" is left intact from compatibility with current ProofGeneral. We simply re-synchronize the command history stack after each Backtrack. - "Undo" is kept as a standard command, not a backtracking one, a bit like "Focus". Same for "Restart" and "Abort". All of these are now accepted in coqide (Undo simply triggers a warning). - Undocumented command "Undo To n" (counting from start of proof instead of from end) also keep its semantics, it is simply made compatible with the new stack mechanism. ** New restrictions ** We now forbid backtracking commands (Reset* / Back*) inside files when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail. Too much work dealing with these situation that nobody uses. ** Internal details ** Internally, the command stack differs a bit from what was in Ide_slave earlier (which was inspired by lisp code in ProofGeneral). We now tag commands that are unreachable by a backtrack, due to some proof being finished, aborted, restarted, or partly Undo'ed. This induce a bit of bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code is straightforward: we simply search backward the first reachable state starting from the desired place. We don't depend anymore on the proof names (apart in the last proof block), It's more robust this way (think of re-entering a M.foo from an outside proof foo). Many internal clarifications in Lib, Vernac, etc. For instance "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls (Lib.label_before_name "foo"), and performs a BackTo to the corresponding label. Concerning Coqide, we directly suppress the regular printing of goals via a flag in Vernacentries. This avoid relying on a classification of commands in Ide_slave as earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for plugin initialization functionGravatar gareuselesinge2012-01-26
| | | | | | | | | | | Plugins can call add_known_plugin instead of add_known_module to specify an initialization function. That function is granted to be called after the system initialization (in case of static linking) and every time their are "loaded" with Declare ML Module (even if the .cmo or .cmxs is actually loaded only once since OCaml is unable to unload dynamically linked modules). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 739: forbid dumpglob while using Coqtop in interactive modeGravatar pboutill2012-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14935 85f007b7-540e-0410-9357-904b9bb8a0f7
* -user option removalGravatar pboutill2011-11-21
| | | | | | | it is imcompatible with the freedesktop policy that config directory is private. Feel absolutly free to revert this commit if you think -user should stay git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
| | | | | | | | Even if they are no-ops now, the commands Set/Unset Undo themselves are kept for compatibility, in particular to avoid error messages or warnings during the initialization of ProofGeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ↵Gravatar aspiwack2011-08-09
| | | | | | so that the files in Init can benefit from the full-blown tactic language. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add compatibility option "-compat 8.3".Gravatar herbelin2011-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
| | | | | | | | | inserting special chars for proof by pointing with emacs. This was interacting badly with utf8. It may be implemented back with xml-like tags instead of special chars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
| | | | | | | Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 20:52:55 +0000