| Age | Commit message (Collapse) | Author |
|---|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
|
|
|
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
|
It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.
|
|
|
|
Previously, newlines were missing if a node had no children.
|
|
This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.)
|
|
|
|
Changes:
- data structures are purely functional (so retracting do work)
- profiling data flows towards master using the feedback bus
- master aggregates the data on printing
|
|
|
|
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
using a custom feedback message in response to "Show Ltac Profile."
|
|
|
|
Introduced by b21fefc0ec0aab2560d0b654f1a1f4203898388b
|
|
|
|
|
|
|
|
|
|
|
|
|
