| Age | Commit message (Collapse) | Author |
|---|
|
There is little point in telling the user the error report is sub optimal.
In this particular case, such error has already been reported (on
the correct location) so reminding it in a non-localized way is not
even that bad.
|
|
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
|
|
|
|
|
|
|
|
|
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
|
|
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
and global for 8.4 and 8.5.
|
|
|
|
|
|
Since this is really what they are.
Squashing this renaming back to the root of the feature branch is hard.
|
|
By default we enable only {} and par: that are detectable in
a complete way.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
