| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | |\ \ \
| |/ / /
|/| | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | |\ \ \
| |_|/ / /
|/| | | | |
|
| | | | | | |
|
| | | | | | |
|
| |/ / / / |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We need to do a bit of hacking, but it should be fine for the short
term.
c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ / / |
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Coq.
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We now allow the user to overlay contribution repositories and
branches by adding their own rules to `ci-basic-overlay.sh`.
This just provides very basic support.
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This commit also documents the behavior of said function;
and fix the location of the ssreflect clone to an absolute
path (this is now necessary).
|
| | | | | | | |
|
| | | | | | | |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | | |
- Move the git clones to a specific subfolder to avoid pollution.
- Do not fail when git clone already exist (but make sure it is up-to-date).
|
| | | | | |
| | | | |
| | | | |
| | | | | |
We need to agree a bit more with upstream.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
We need to agree a bit more with upstream.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This is required since we merged PR#309: Ltac as a plugin.
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
| |/ / / / |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We make math-comp overlays easier, we also start structuring the
scripts a bit more.
|
| | | |\ \
| |_|/ /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
|
| |/ / / / |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).
Any improvements are welcome.
|
Pierre-Marie Pédrot
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Matej Kosik
Théo Zimmermann
Pierre Letouzey
Tej Chajed