| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
|
|
This patch restores the proper printing of anomalies in coqtop / coqc
/ coqide. Currently, they are printed with an `Error` header, whereas
they should be printed with an `Anomaly" header.
This reopens an unfinished debate started in #390 , about how to
properly do "message" headers. Prior to #390, headers were handled
inconsistently, sometimes, `Error` or `Anomaly` were added in
`CErrors`, which lives below of the tagging system, thus some times we
got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789),
but some other times the headers were added by the message handlers in
Feedback.
PR #390 takes the position of identifying the messages with the
`Feedback.level` tag, and letting the backends to the tagging. This
makes sense as the backends may want to interpret the "headers" in any
way they'd like. For instance, instead of printing: `Error: foo` they
may want to insert an image.
Note that this implies that CoqIDE doesn't currently insert an error
header on the first error case. This could be easily solved, but for
anomalies we could do in any of the ways explained below.
There are thus two natural ways to handle anomalies here: One is to
tag them as errors, but add a text header, this is done now, with the
small optimization in the case the handled has access to the exception
itself. The second way is to add a new `Feedback.level` category and
tag the anomalies appropriately. We would need also to modify Fail in
this case, or to completely remove it from the protocol.
I guess feedback from the rest of developers is needed before
committing to a strategy, for now this patch should be good.
|
|
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.
|
|
-> Candidate to be merge with the main feedback commit.
|
|
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.
|
|
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
|
|
|
|
|
|
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.
|
|
|
|
The current future system is lazy when "chaining" (*) a resolved
future, which implies that chaining with a resolved future will produce
a non-resolved one.
This misfeature interacts badly with the "purification" optimization,
which in turn provokes a swarm of spurious state setting calls in real
use.
To solve this problem, we revert to the more natural semantics of
respecting the evaluation semantics when mapping over a future, indeed
respecting the previous resolution status.
This commit solves a kind of _critical_ bug in the current system,
with the particular bad path origination in `Future.split2` due to the
following accumulation of circumstances:
```
split2 x -> chain x (fun x -> fst x)
=>
let y = chain ~pure x (fun x -> fst x) in
if is_over x && greedy then ignore(force ~pure y);
y
=> [y <- Closure (fun x -> fst x)]
ignore(force (Closure (fun x -> fst x)))
=>
purify_future (force ~pure) (Closure (fun x -> fst x))
```
and then, the test in `purify_future` fails, triggering the
spurious state reset operation.
This problem was first noted at
https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and
seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382
We fix the problem by making chaining eager, but other solutions would
be possible. Given that the main user of `chain` is `split2` which
does `snd/fst`, I recommend this solution.
The difference in calls to `unfreeze_state` is dramatic:
```
| File | Freeze Calls After | Freeze Calls Before |
|----------------------------------------+--------------------+---------------------|
| theories/Init/Notations.v | 0 | 0 |
| theories/Init/Logic.v | 57 | 614 |
| theories/Init/Datatypes.v | 13 | 132 |
| theories/Init/Logic_Type.v | 7 | 57 |
| theories/Init/Specif.v | 5 | 35 |
| theories/Init/Nat.v | 0 | 0 |
| theories/Init/Peano.v | 22 | 264 |
| theories/Init/Wf.v | 8 | 89 |
| theories/Init/Tactics.v | 2 | 24 |
| theories/Init/Tauto.v | 0 | 0 |
| theories/Init/Prelude.v | 0 | 0 |
| Bool/Bool.v | 104 | 1220 |
| Program/Basics.v | 0 | 0 |
| Classes/Init.v | 0 | 0 |
| Program/Tactics.v | 0 | 0 |
| Relations/Relation_Definitions.v | 0 | 0 |
| Classes/RelationClasses.v | 21 | 341 |
| Classes/Morphisms.v | 47 | 689 |
| Classes/CRelationClasses.v | 18 | 245 |
| Classes/CMorphisms.v | 50 | 587 |
| Classes/Morphisms_Prop.v | 3 | 127 |
| Classes/Equivalence.v | 6 | 105 |
| Classes/SetoidTactics.v | 0 | 0 |
| Setoids/Setoid.v | 4 | 33 |
| Structures/Equalities.v | 8 | 93 |
| Relations/Relation_Operators.v | 0 | 0 |
| Relations/Operators_Properties.v | 35 | 627 |
| Relations/Relations.v | 2 | 24 |
| Structures/Orders.v | 12 | 148 |
| Numbers/NumPrelude.v | 0 | 0 |
| Structures/OrdersTac.v | 13 | 234 |
| Structures/OrdersFacts.v | 73 | 931 |
| Structures/GenericMinMax.v | 82 | 1294 |
| Numbers/NatInt/NZAxioms.v | 0 | 0 |
| Numbers/NatInt/NZBase.v | 7 | 87 |
| Numbers/NatInt/NZAdd.v | 14 | 168 |
| Numbers/NatInt/NZMul.v | 12 | 144 |
| Logic/Decidable.v | 28 | 336 |
| Numbers/NatInt/NZOrder.v | 81 | 1174 |
| Numbers/NatInt/NZAddOrder.v | 24 | 288 |
| Numbers/NatInt/NZMulOrder.v | 46 | 552 |
| Numbers/NatInt/NZParity.v | 35 | 420 |
| Numbers/NatInt/NZPow.v | 29 | 348 |
| Numbers/NatInt/NZSqrt.v | 54 | 673 |
| Numbers/NatInt/NZLog.v | 64 | 797 |
| Numbers/NatInt/NZDiv.v | 49 | 588 |
| Numbers/NatInt/NZGcd.v | 36 | 432 |
| Numbers/NatInt/NZBits.v | 0 | 0 |
| Numbers/Natural/Abstract/NAxioms.v | 0 | 0 |
| Numbers/NatInt/NZProperties.v | 0 | 0 |
| Numbers/Natural/Abstract/NBase.v | 14 | 177 |
| Numbers/Natural/Abstract/NAdd.v | 6 | 72 |
| Numbers/Natural/Abstract/NOrder.v | 29 | 349 |
| Numbers/Natural/Abstract/NAddOrder.v | 5 | 60 |
| Numbers/Natural/Abstract/NMulOrder.v | 8 | 96 |
| Numbers/Natural/Abstract/NSub.v | 36 | 432 |
| Numbers/Natural/Abstract/NMaxMin.v | 18 | 216 |
| Numbers/Natural/Abstract/NParity.v | 4 | 48 |
| Numbers/Natural/Abstract/NPow.v | 26 | 312 |
| Numbers/Natural/Abstract/NSqrt.v | 9 | 108 |
| Numbers/Natural/Abstract/NLog.v | 0 | 0 |
| Numbers/Natural/Abstract/NDiv.v | 50 | 600 |
| Numbers/Natural/Abstract/NGcd.v | 14 | 168 |
| Numbers/Natural/Abstract/NLcm.v | 29 | 348 |
| Numbers/Natural/Abstract/NBits.v | 168 | 2016 |
| Numbers/Natural/Abstract/NProperties.v | 0 | 0 |
| Arith/PeanoNat.v | 77 | 990 |
| Arith/Le.v | 2 | 57 |
| Arith/Lt.v | 14 | 168 |
| Arith/Plus.v | 20 | 269 |
| Arith/Gt.v | 17 | 248 |
| Arith/Minus.v | 11 | 132 |
| Arith/Mult.v | 14 | 168 |
| Arith/Between.v | 19 | 299 |
| Logic/EqdepFacts.v | 26 | 539 |
| Logic/Eqdep_dec.v | 13 | 361 |
| Arith/Peano_dec.v | 3 | 26 |
| Arith/Compare_dec.v | 35 | 360 |
| Arith/Factorial.v | 3 | 36 |
| Arith/EqNat.v | 10 | 111 |
| Arith/Wf_nat.v | 18 | 173 |
| Arith/Arith_base.v | 0 | 0 |
| Numbers/BinNums.v | 0 | 0 |
| PArith/BinPosDef.v | 0 | 0 |
| PArith/BinPos.v | 229 | 2810 |
| NArith/BinNatDef.v | 0 | 0 |
| NArith/BinNat.v | 107 | 1330 |
| PArith/Pnat.v | 51 | 688 |
| NArith/Nnat.v | 30 | 360 |
| setoid_ring/Ring_theory.v | 43 | 756 |
| Lists/List.v | 195 | 2908 |
| setoid_ring/BinList.v | 6 | 90 |
| Numbers/Integer/Abstract/ZAxioms.v | 0 | 0 |
| Numbers/Integer/Abstract/ZBase.v | 3 | 36 |
| Numbers/Integer/Abstract/ZAdd.v | 46 | 552 |
| Numbers/Integer/Abstract/ZMul.v | 8 | 96 |
| Numbers/Integer/Abstract/ZLt.v | 21 | 252 |
| Numbers/Integer/Abstract/ZAddOrder.v | 45 | 543 |
| Numbers/Integer/Abstract/ZMulOrder.v | 24 | 288 |
| Numbers/Integer/Abstract/ZMaxMin.v | 22 | 264 |
| Numbers/Integer/Abstract/ZSgnAbs.v | 41 | 492 |
| Numbers/Integer/Abstract/ZParity.v | 6 | 72 |
| Numbers/Integer/Abstract/ZPow.v | 10 | 120 |
| Numbers/Integer/Abstract/ZDivTrunc.v | 68 | 816 |
| Numbers/Integer/Abstract/ZDivFloor.v | 70 | 840 |
| Numbers/Integer/Abstract/ZGcd.v | 29 | 348 |
| Numbers/Integer/Abstract/ZLcm.v | 50 | 600 |
| Numbers/Integer/Abstract/ZBits.v | 205 | 2460 |
| Numbers/Integer/Abstract/ZProperties.v | 0 | 0 |
| ZArith/BinIntDef.v | 0 | 0 |
| ZArith/BinInt.v | 212 | 2839 |
|----------------------------------------+--------------------+---------------------|
```
(*) I would call it `Future.map` better than chain.
|
|
No functional change.js
|
|
No functional change.
|
|
No functional changes.
|
|
It was always set to `greedy:true`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The same file name for .dot graphs could be used by concurrent processes.
|
|
Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.
This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
|
|
|
|
Was PR#351: Complete a truncated comment
|
|
Was PR#363: lib/Unicodetable: Update.
|
|
Richpp output depends on printing width, thus its internal formatter
should be seeded with the proper width value.
While we are at it, we increase the default buffer size to a more
sensible value.
|
|
|
|
When opening a file without extension, an uncaught exception was
occurring.
Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
|
|
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
|
|
|
Unicode tables using UUCD, an OCaml library to parse the official
Unicode tables.
|
|
|
|
|
|
Introduce by myself, I'm afraid, in #308. Noticed by PMP during the
review, but I forgot to fix it before merge.
|
|
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.
|
|
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
|
This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
|
