diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-05 21:31:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-05 21:31:14 +0200 |
| commit | d411a796341a138cacd72350715871f48f82920b (patch) | |
| tree | 8068f080cbe12d79a4b09641c7a1c836a5d372f4 /toplevel/vernac.ml | |
| parent | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (diff) | |
[toplevel] Fix a couple of logical errors in error printing.
In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use
exceptions for error printing. However a couple of mistakes were
present in that commit:
- We wrongly absorbed the exception on `Vernac.compile`. However, it
should be propagated as the caller will correctly print the error
now. This introduced a critical bug as now `coqc` return the wrong
exit status on error, breaking all sort of things.
- We printed parsing exceptions twice; now it is not necessary to
print the exception in the parsing handler as it will be propagated.
I've checked this commit versus all previously reported bugs and it
seems to work; we should definitively add a test-suite case to check
that the exit code of `coqc` is correct, plus several other cases such
as bugs
https://coq.inria.fr/bugs/show_bug.cgi?id=5467
https://coq.inria.fr/bugs/show_bug.cgi?id=5485
https://coq.inria.fr/bugs/show_bug.cgi?id=5484
etc... See also PR #583
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9f6f77ef1..4fca4ea18 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -323,8 +323,5 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - begin - try compile v f - with any -> Topfmt.print_err_exn any - end; + compile v f; CoqworkmgrApi.giveback 1 |