| Age | Commit message (Collapse) | Author |
|---|
|
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
|
|
|
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
|
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.
|
|
|
|
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
|
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
|
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
|
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.
|
|
Mostly documentation and making a couple of local flags, local.
|
|
- 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.
|
|
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.
|
|
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
|
