| Age | Commit message (Collapse) | Author |
|---|
|
Using a unit test as it's way faster than messing with universes.
You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.
About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.
Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm. A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.
Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
"-diffs on|off|removed" on the OS command line. The "on" option shows only the
new item with added text, while "removed" shows each modified item twice--once
with the old value showing removed text and once with the new value showing
added text.
The highlights use 4 tags to specify the color and underline/strikeout.
These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".
The first two are for added or removed text; the last two are for
unmodified parts of a modified item.
Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and
"end.diff.*", but only on the first and last strings of the span.
|
|
|
|
Adding a space before the bar separating disjunctive patterns.
Removing an extra space after the bar for inner disjunctive patterns.
|
|
The typical Coq `Pp.t` document contains a lot of "gluing" which
produces efficient structures but it is quite painful in
serialization.
We optimize a common document building case so we don't create as much
glue nodes as with the "naive" strategy, and without incurring in the
large performance cost full flattening would produce.
This is a temporal fixup, see #505 for more context on the discussion
and medium-term plans.
|
|
|
|
|
|
Fix bug introduced by a Haskell programmer.
|
|
eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test
|
|
|
|
We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.
All error display is handled by a single, uniform path.
There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.
We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:
```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```
This commit also fixes:
- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429
|
|
Following a suggestion by @ppedrot in #390, we require `Pp` clients to
be aware that they are using a "view" on the `std_ppcmds` type.
This is not extremely useful as people caring about the documents will
indeed have to follow changes in the view, but it costs little to play
on the safe side here for now.
We also introduce a more standard notation, `Pp.t` for the main type.
|
|
- 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, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.
This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.
|
|
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
|
|
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.
|
|
|
|
We replace open/close box commands in favor of the create box ones.
|
|
We replace open/close tag commands by a well-balanced "tag" wrapper.
|
|
|
|
|
|
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
|
Mostly unused, we ought to limit spacing in the boxes themselves.
|
|
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
|
|
|
This made the whole pp code complicated only for the purpose of the
beautifier, while it is not clear when this was useful.
Removing the code for simplicity, not excluding to later address
beautifier issues when they show up.
|
|
|
|
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
|
|
We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.
We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.
Test suite passes.
|
|
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
This mechanism relied on functions that are deprecated in recent versions
of ocaml. It was incorrectly used for the most part anyway. The only place
that was using tabulations correctly is "print_loadpath", so there is a
minor regression there: physical paths of short logical paths are no longer
aligned.
|
|
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.
|
|
Now the casual Dyn user does not need to be a GADT guru
|
|
be used in the generic printer for tactics.
Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
So that they display in response buffer.
|
|
|
|
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
|
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.
|
|
|
|
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
|
|
as glued.
Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.
This commit makes the following command go from 7.9s to 3.0s:
coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
|
