| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| | | |
|
| | |\ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.
We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).
We also fix a couple of typos noticed by Paul, thanks Paul.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- 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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.
This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.
This commit supersedes PR#204.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.
Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.
XML protocol clients are unaffected, they rely on the instead on the
Fail value.
This commit supersedes PR#203.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
`process_error_hook` seems unnecesary, we just call the proper error
interpretation.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
`tactic_being_run_hook` was used for the "xml" pluging but I am not
sure we have a sensible use case here.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This fixes a few clear bugs, but the STM code handling Time, Fail and
Redirect before par: still needs to be rewritten. It does not implement
the same semantics as the vernac interpreter for Fail Fail [c] and
ignores Redirect.
This commit was already reviewed with Enrico and tested on Travis.
|
| |\| | | |
|
| | |\| | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Need to check inside control expressions. Also fixes handling of
[Redirect "file" Defined.] and [Timeout n Defined.].
Fixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411):
coqc -quick hangs on [Time Defined.]
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
|
| | | |
| | |
| | |
| | |
| | | |
This is a small, but convenient refactoring, as it will allow common
argument parsing.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
| | | |
| | |
| | |
| | | |
It was always set to `greedy:true`.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We extend `Stm.vernac_interp` so it can handle the commands it should
by level. This reenables `Show Script` handling, and this
interpretation function should handle more commands in the future such
as Load.
However note that we must first refactor the parsing state handling a
bit and remove the legacy `Stm.interp` before that.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |\| |
|
| | | | |
|
| | |\| |
|
| | | | |
|
Gaetan Gilbert
Maxime Dénès
Emilio Jesus Gallego Arias
Guillaume Melquiond
Tej Chajed
Enrico Tassi
Pierre-Marie Pédrot