| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Instead of the current hack that won't work as soon as we check some
part of the document asynchronously, we make the warning processor
recover a proper location if the warning doesn't have one attached.
This is what CoqIDE does [but it queries it's own document model].
Fixes: #6172
|
| | |
|
| |
|
|
|
|
|
| |
If coqtop was started with "-w none" yet the script used "Set Warnings
Append", then all the warnings were turned back to their default value.
This commit turns "none" (whatever its sign) into "-all" whenever some
warning status is modified afterward, in order to prevent the issue.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The status of a warning can now be set before the warning is declared
(typically by a plugin). However, I had to remove the "unknown warning"
warning.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| |/ /
| |
| |
| | |
Now it is a private field, locations are optional.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| |\| |
|
| | |
| |
| |
| |
| | |
The default value of the warnings flag was printed as an empty string,
now replaced by "default".
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| | |
|
| |
|
|
|
|
| |
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
|
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Théo Zimmermann
Guillaume Melquiond
Pierre-Marie Pédrot
Maxime Dénès
Pierre Letouzey