| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 brings a 10x speedup for going at the end of large .v files.
|
|
|
|
|
|
This brings a 10x speedup for going at the end of large .v files.
|
|
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
|
|
|
|
For Drop for example.
|
|
and Evar in notations, and there are anyway already forbidden.
|
|
|
|
|
|
uniformity.
|
|
|
|
- the particlar rule for dev/printers.cma is adapted as for %.cma:%.mllib
- some more removal of | .d in rules
|
|
We add a dependency of .cma over .mllib.
This dependency over the .mllib is somewhat artificial, since
ocamlc -a won't use this file, hence the $(filter-out ...) below.
But this ensures that the .cm(x)a is rebuilt when needed,
(especially when removing a module in the .mllib).
We also remove all "order-only" dependencies over *.d in rules,
since the -include mechanism should already ensure that we have
up-to-date dependencies known by make.
|
|
There were a forgotten CAMLP4DEPS macro.
We also avoid otags failure with camlp5 (in this case, it only
builds the tags of regular .ml files, not .ml4).
|
|
|
