| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
|
|
|
|
| |
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.
|
| |\
| |
| |
| | |
Add -o option to coqc
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
This is the "error resiliency" mode for STM
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
By default we enable only {} and par: that are detectable in
a complete way.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
| |/ / /
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |\ |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
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).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
| | |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
| | |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
Pierre Letouzey
Maxime Dénès
Pierre-Marie Pédrot
Enrico Tassi
Jason Gross
Emilio Jesus Gallego Arias
Hugo Herbelin
Guillaume Melquiond
Matej Kosik
Thomas Sibut-Pinote
Gabriel Scherer