| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Makes printing rules more explicit and should close #6799.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
| | |
|
| | |
|
| |
|
|
|
|
| |
It is not doing the same thing as coqtop, and the corresponding coqtop
semantics is irrelevant in the checker as the latter does not rely on ML
code.
|
| |
|
|
|
|
| |
It has exactly the same effect as -R, because there is no such thing as
implicit relativization for object files in coqchk, contrarily to what
Require does in coqtop.
|
| | |
|
| |
|
|
|
| |
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fixes longstanding bug likely introduced in the first `pp` to
`Feedback` migration, namely the checker didn't register a feedback
printer, thus no calls to `Feedback.msg_*` were printed in the
checker.
This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587
We fix this by adding a custom printer to the checker, this is correct
as the checker owns now the full console, however a cleanup should
happen in any of these two directions:
- all the calls to feedback are removed, and the checker always uses
its own printing mechanism.
- all the calls to `Format/Printf` are removed and the checker always
uses the `Feedback` mechanism.
Currently, I have no opinion on this.
|
| |/
|
|
|
|
|
|
|
|
|
| |
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |\ |
|
| | |\
| | |
| | |
| | | |
Was PR#257: [checker] Fix/fine tune printing.
|
| | | |
| | |
| | |
| | | |
in error messages
|
| |/ /
| |
| |
| | |
Suggested by @ppedrot
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct
access to the console, recommending instead to provide information to
the user by means of the `Feedback.msg_*` facilities.
However, we introduced a display bug in the checker printer as it is
special and doesn't use the Pp facilities (likely for trust reasons),
spotted by @herbelin
This patch fixes this bug and performs a couple more of fine tunings in
the input.
However, it could be desirable to port the `checker/printer.ml` to `Pp`
and use the feedback mechanism; this would allow IDEs to use the checker
in a more convenient way, at the cost of trusting `Pp` (which is already
a bit trusted currently)
A start of that idea can be found at:
https://github.com/ejgallego/coq/tree/fix_checker_printing
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
| |
I had to remove code handling the -type-in-type option introduced by commit
9c732a5. We should fix it at some point, but I am not sure that using the
checker with a system known to be blatantly inconsistent makes much sense
anyway.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| |/
|
|
| |
There is no location to print anyway, so it will never be useful.
|
| |
|
|
|
|
|
|
|
|
| |
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?
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
| |
|
|
| |
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
| | |
|
| |
|
|
|
|
|
| |
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).
|
| | |
|
| | |
|
| |
|
|
| |
were never used and were responsible for code duplication.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Revised Coqtop.parse_args in a cleaner and lighter style
- Improved error message in case of argument parse failure:
* tell which option is expecting a related argument
* in case of unknown options, warn about them all at once
* do not hide the previous error messages by filling the
screen with usage(). Instead, suggest the use of --help.
- Specialized boolean config field Coq_config.arch_is_win32
- Faster Envars.coqlib, which is back to (unit->string), and
just access Flags.coqlib. Caveat: it must be initialized once
via Envars.set_coqlib
- Avoid keeping an opened channel to the "revision" file
- Direct load of theories/init/prelude.vo, no detour via Loadpath
Beware : ./configure must be runned after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
We use Errors.print for anomalies and other uncaught exceptions
in the checker: this should print the same message, it is shorter
this way, and we avoid using Errors.is_anomaly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Why? : avoid catching (and probably ignoring) exceptions
such as Sys.Break, anomalies, assertions, leading to undetected
bugs and ignored Ctrl-C.
How? : when the precise exception(s) concerned by the try is
known, use them explicitely in the "with". Otherwise, let's use
the pattern "with e when Errors.noncritical e -> "
Particular case : when an exception is catched and reraised
immediately after some adjustments, we leave it untouched.
Simply, for easily identifying these situations later, the name
of the exception variable is changed to "reraise".
Please also adopt this coding style. Automatic checks based
on the "mascot" tool of X. Clerc will be runned regularly.
If you want to avoid to check a particular try...with, use
the variable name "any" after the "with".
All these changes have been tested using the standard library
and the test-suite, but unfortunately this is far from ensuring
that coqtop behaves as before. We'll see after the nightly bench...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Emilio Jesus Gallego Arias
Théo Zimmermann
Ralf Jung
Pierre-Marie Pédrot
Maxime Dénès
Gaetan Gilbert
Yves Bertot
Pierre Letouzey
Guillaume Melquiond
Hugo Herbelin
Xavier Clerc
Matthieu Sozeau
Enrico Tassi
letouzey