| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | | |
versions.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| | |
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| |
|
|
|
| |
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
and avoid duplication
|
| | |/ / |
|
| | |\ \ |
|
| | |\ \ \ |
|
| | | |_|/
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We allow for a dynamic setting of the STM debug flag, and we print
some more information about the result of `process_transaction`.
We also fix a printing bug due to mixing `Printf` and `Format`, which
are not compatible.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In non-interactive mode, `edit_at` seems to do very weird things, for
instance will try to recompute all the previous states which seems
weird.
We better avoid that to approximate 8.6 behavior while we investigate
more.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
When porting the toplevel to the STM, the logic for goal printing was
simplified too much under optimistic assumptions. The idea was not to
rely on the `vernac_classifier` which is an internal and complicated
beast.
However, it seems there are many cases to consider other than
`is_query`, so at the risk of reimplementing the classifier we revert
to the old approach of using the full classification.
This gives maximum 8.6 compatibility, with the pitfall of having to
call the classifier. Indeed, due to the dynamic nature of the "undo
classifier", we cannot call it after `Stm.add`, as the document tree
will be not the right one, making the classification of undo commands
incorrect (actually raising an error "Cannot undo").
|
| | |\ \
| | |/
| |/| |
|
| | | | |
|
| | | |\
| | | |
| | | |
| | | | |
"Print Assumptions".
|
| | |\ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings
after 30 UTF-8 characters instead of using the standard String function.
|
| | |/ / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Off by default.
+ small refactoring of emacs hacks in printer.ml.
|
| | | |/ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.
However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479
Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.
This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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 fixes a logical error introduced in
ce2b2058587224ade9261cd4127ef4f6e94d356b
Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| | |
Indeed we were not correctly backtracking in the case of
StackOverflow. It makes sense to remove the inner handler which is a
leftover of a previous attempt, and handle interpretation errors in
load as non-recoverable.
This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
PR #441 and #530 had an interesting interaction creating two bugs:
- #441 stopped emitting feedback for the parser, however #530 changed
the mechanism to print parser errors to the feedback, thus when the
two patches were applied, parsing errors were not printed in
batch_mode.
- Additionally, #530 contains an error: prior to `Stm.init` we must
take care of exceptions `require ()`/etc... otherwise they won't get
printed.
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This header file had accumulated quite a bit of cruft over the
years, we clean it up while we are at it.
No functional change as all the removed variables/methods were noops
long time ago.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
|
| |\ \ \ |
|
Guillaume Melquiond
Matej Košík
Emilio Jesus Gallego Arias
Jason Gross
Maxime Dénès
Enrico Tassi
Pierre-Marie Pédrot
Hugo Herbelin
Gaetan Gilbert
Pierre Courtieu
Cyprien Mangin