aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.ml
Commit message (Collapse)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | Suggested by @ppedrot
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | | | | | | | Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Remove Mltop.add_path as it is no longer possible to import files from ↵Gravatar Guillaume Melquiond2015-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | subdirectories. Using Mltop.add_path instead of Mltop.add_rec_path causes the following kind of behavior: $ coqtop -nois Coq < Require Import Coq.Init.Datatypes. Error: Cannot find a physical path bound to logical path Coq.Init. The only case where its use is still warranted is the implicit "." path. It shall not be recursive because Coq might be called from about anywhere. This patch also removes -I-as since its behavior is no longer the one from 8.4 so it is not worth keeping it around.
| * Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
| |
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| | | | | | | | | | | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise.
| * Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | | | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
| * Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
|/ | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
| | | | | | | | This is done by adding a fourth type of loadpath, the ones that are neither implicit nor root, for the subdirectories of a -Q root. Note: this means that scanning for available directories is no longer done on the fly for -Q, but once and for all, as with -R.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* do not explode if a plugin is not up to date on -help (Close: 3673)Gravatar Enrico Tassi2014-09-29
|
* mltop: when a plugin is loaded store its full path in the summaryGravatar Enrico Tassi2014-09-18
| | | | | | | | | | | This fixes the following bug related to stm: if one passes -I to coqide, then such flag is passes to the workers; but if one uses "Add ML LoadPath" to extend the paths in which coq looks for plugins, this extra path was no passed to the slaves (via the command line) nor store in the system state and hence sent to the slaves. With this patch, when a cmxs is loaded, its full path is stored in the summary and hence sent to the workers as one may expect.
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* More informative message when Mltop.load_object fails.Gravatar Hugo Herbelin2014-07-01
|
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively.
* Adding the possibility for ML modules to declare functions to be called atGravatar Pierre-Marie Pédrot2014-05-12
| | | | | caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins.
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps ↵Gravatar Pierre Boutillier2014-04-09
| | | | | | | | | with -R. (Fix for Rocq/Rational.)" This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69. Conflicts: CHANGES
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
| | | | | | This option complements -I-as and -R. As the two other options, it adds a new loadpath, but contrarily to them, files are not looked into the directory unless fully qualified.
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵Gravatar Guillaume Melquiond2014-04-07
| | | | (Fix for Rocq/Rational.)
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
| | | | | | | | | | | | | - Option -I no longer handles loadpath, only mlpath. This is the same behavior as coq_makefile. Option -I-as is unchanged. - Option -R no longer recursively adds to mlpath; only the root directory is added. - user-contrib/ and xdg directories are no longer recursively added to the loadpath. - theories/ and plugins/ are no longer recursively added to the loadpath when option -nois is passed. - All the preconfigured directories are still recursively added to the mlpath though.
* Mltop: explicitly qualify calls to CUnixGravatar Pierre Letouzey2014-01-30
|
* Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Gravatar Pierre Boutillier2014-01-13
| | | | The exact filename has to be written. This is coherent with the RefMan.
* summary for ML modules made correctGravatar gareuselesinge2013-08-30
| | | | | | | | | This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small typo in Print Debug GCGravatar ppedrot2013-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
| | | | | | the OCaml GC, as indicated by [Gc.stat]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
| | | | | | | | States.freeze takes ~marshallable:bool, so that (only) when we want to marshal data to disk/network we can ask the freeze functions of the summary to force lazy values. The flag is propagated to Lib and Summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
| | | | | | the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 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
* More monomorphization.Gravatar ppedrot2013-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 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
* Updating the backtrace handling mechanism to accomodate the newGravatar ppedrot2013-02-18
| | | | | | exception information addition facility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
| | | | | | | I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16161 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 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
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Low-level hack to get some more informative message from dynamic loading errors.Gravatar herbelin2012-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16021 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
* When loading a plugin, prefer .cma to .cmoGravatar gareuselesinge2012-10-14
| | | | | | | | | | Imagine foo.cma contains foo_utils.cmo and foo.cmo. Also imagine that foo.cmo depends on foo_utils.cmo. With this patch, when asked to load foo, Coq loads the foo.cma archive. Loading simply foo.cmo would fail since foo_utils.cmo is needed to load foo.cmo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15883 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 17:39:49 +0000