aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Collapse)AuthorAge
* coqc: print debug feedback coming from workersGravatar Enrico Tassi2016-09-13
| | | | This way par:eauto and all:eato print the same debugging traecs
* fix get_host_port error message (#4724)Gravatar Enrico Tassi2016-08-23
|
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
| * Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
| |
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | | | | | We also add a Coq86.v compat file.
* | 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
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
| | | | | | | | | | | | | | | | What one needs to know in 3rd party makefiles, like plugins ones, is the Coq version and the OCaml version number. This option prints the 2 values on a single line separated by spaces. The already existing --version outputs the same piece of info but in a format meant for user consumption, and hence harder to parse.
* | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ | | | | | | | | | Add -o option to coqc
* \ \ Merge remote-tracking branch 'origin/pr/182' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* \ \ \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ | | | | | | | | | | | | | | | This is the "error resiliency" mode for STM
* | | | | Moving back Ltac profiling to the Ltac folder.Gravatar Pierre-Marie Pédrot2016-06-14
| | | | |
| * | | | STM: each proof block can be enabled separatelyGravatar Enrico Tassi2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | By default we enable only {} and par: that are detectable in a complete way.
| * | | | STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
| | | | |
* | | | | -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ```
* | | | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
|/ / / / | | | | | | | | | | | | | | | | | | | | This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
| * | | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The command line option is named: - async-proofs-delegation-threshold Values are of type float, default 1.0 (seconds). Proofs taking less that the threshold are not delegated to a worker.
| | | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
| | | | | | | | | | | | | | | | This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
* | | | 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.
| * / coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
| |
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
| | | | | | | | | | | | | | (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| |
* | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| |
* | CLEANUP: simplifying "Coqtop.init_gc" implementationGravatar Matej Kosik2015-12-18
| |
* | CLEANUP: removing unnecessary wrapper functionGravatar Matej Kosik2015-12-18
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
| | | | | | | | | | Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
| | | | | | | | | | Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Prevent States.intern_state and System.extern_intern from looking up files ↵Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | | | | | | | in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner.
| * Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files.
| * Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
| | | | | | | | | | | | | | | | | | | | This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | command line. Documenting only the former for simplicity and uniformity with predating option -with-geoproof.