| Age | Commit message (Collapse) | Author |
|---|
|
Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
|
|
|
|
|
|
|
|
|
|
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
|
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
|
|
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
|
|
|
|
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
|
This paves the way to detecting error boundaries via indentation
|
|
Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap). It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).
In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
|
|
A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.
Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).
Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.
|
|
|
|
|
|
|
|
|
|
|
|
This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily. I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid. That said, a few simple tests seem to indicate that this
works as expected.
|
|
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
|
Implement the suggestion of @mattam82 to check whether or not we're
profiling before inserting the tclFINALLY.
Timing stats:
Using:
```bash
make clean && git clean -xfd && ./configure -local -with-doc no -coqide no && /usr/bin/time -f "all coq (real: %e, user: %U, sys: %S, mem: %M ko)" make STDTIME='/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 -j4 2>&1
```
Without LtacProf (4c078b0362542908eb2fe1d63f0d867b339953fd), two runs:
```
real: 147.96, user: 467.93, sys: 30.80, mem: 820468 ko
real: 148.04, user: 467.92, sys: 30.49, mem: 820680 ko
```
With LtacProf, two runs:
```
real: 148.32, user: 469.09, sys: 30.57, mem: 818588 ko
real: 148.38, user: 469.71, sys: 30.56, mem: 816720 ko
```
Overall overhead on building Coq: about 0.24%
Differences in the slowest files:
```
After | File Name | Before || Change
---------------------------------------------------------------------------
7m07.32s | Total | 7m05.16s || +0m02.15s
---------------------------------------------------------------------------
0m44.90s | Numbers/Rational/BigQ/QMake | 0m44.11s || +0m00.78s
0m15.94s | plugins/setoid_ring/Ncring_polynom | 0m15.72s || +0m00.21s
0m14.04s | Numbers/Cyclic/DoubleCyclic/DoubleCyclic | 0m14.05s || -0m00.01s
0m10.65s | Numbers/Cyclic/DoubleCyclic/DoubleSqrt | 0m10.45s || +0m00.20s
0m09.57s | FSets/FMapAVL | 0m09.53s || +0m00.04s
0m09.51s | MSets/MSetRBT | 0m09.45s || +0m00.06s
0m07.00s | Numbers/Cyclic/DoubleCyclic/DoubleDiv | 0m07.05s || -0m00.04s
0m06.88s | Numbers/Cyclic/Int31/Cyclic31 | 0m06.94s || -0m00.06s
0m05.82s | plugins/setoid_ring/Field_theory | 0m05.87s || -0m00.04s
0m05.74s | FSets/FMapFullAVL | 0m05.71s || +0m00.03s
0m05.37s | Reals/Ratan | 0m05.42s || -0m00.04s
0m05.36s | plugins/setoid_ring/Ring_polynom | 0m05.37s || -0m00.00s
0m05.09s | plugins/micromega/EnvRing | 0m04.96s || +0m00.12s
```
|
|
|
|
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Since d09def34, only the summary of libraries was included in the checksum, not
the actual content of the library. This quick fix performs the checking of the
checksum immediately, even if the loading is delayed.
|
|
|
|
Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.
|
|
|
|
|
|
Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
|
|
|
|
|
|
|
|
|
|
|
|
#4770).
This also fixes comments not being properly skipped when looking for eol.
|
|
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
|
|
This breaks compilation via ocamlbuild, and also leads to awkward
commands via make
|
|
Thanks to HH for pointing it out.
|
|
|
|
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
|
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
|
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
|
|
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.
|
