| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
To fix #5081, that LtacProf associates time spent in tactic-evaluation
with the wrong tactic, I added two additional calls to the profiler
during tactic evaluation phase. These two calls do not update the call
count of the relevant tactics, but simply add time to them.
Although this fixes #5081, it introduces a new bug, involving tactics
which are aliases of other tactics, which I am not sure how to fix.
Here is the explanation of the issue, as I currently understand it (also
recorded in a comment in `profile_ltac.mli`):
Ltac semantics are a bit insane. There isn't
really a good notion of how many times a tactic has been "called",
because tactics can be partially evaluated, and it's unclear
whether the number of "calls" should be the number of times the
body is fetched and unfolded, or the number of times the code is
executed to a value, etc. The logic in `Tacinterp.eval_tactic`
gives a decent approximation, which I believe roughly corresponds
to the number of times that the engine runs the tactic value which
results from evaluating the tactic expression bound to the name
we're considering. However, this is a poor approximation of the
time spent in the tactic; we want to consider time spent evaluating
a tactic expression to a tactic value to be time spent in the
expression, not just time spent in the caller of the expression.
So we need to wrap some nodes in additional profiling calls which
don't count towards to total call count. Whether or not a call
"counts" is indicated by the `count_call` boolean argument.
Unfortunately, at present, we can get very strange call graphs when
a named tactic expression never runs as a tactic value: if we have
`Ltac t0 := t.` and `Ltac t1 := t0.`, then `t1` is considered to
run 0(!) times. It evaluates to `t` during tactic expression
evaluation, and although the call trace records the fact that it
was called by `t0` which was called by `t1`, the tactic running
phase never sees this. Thus we get one call tree (from expression
evaluation) that has `t1` calls `t0` calls `t`, and another call
tree which says that the caller of `t1` calls `t` directly; the
expression evaluation time goes in the first tree, and the call
count and tactic running time goes in the second tree. Alas, I
suspect that fixing this requires a redesign of how the profiler
hooks into the tactic engine.
|
|
This way, `Time Show Ltac Profile` shows the profile in `*response*` in
PG, without an extra `infomsg` tag on the timing.
|
|
This fixes #6378. Previously the ML module was never declared anywhere.
Thanks to @cmangin for the pointer.
|
|
Fixes GH#6384 and GH#6385.
|
|
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
|
|
|
And some code simplification.
|
|
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.
The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
|
|
|
|
|
|
|
|
|
|
|
|
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
|
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
|
|
|
We generalize the possible use of levels to raw and glob printers.
This is potentially useful for printing ltac expressions which are the
glob level.
|
|
The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
|
|
|
|
|
|
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
|
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|
|
|
Was broken since 8.6.
|
|
|
|
We preserve the level instead of resetting it at level 0.
Probably it would be the same as giving level ltop since Tacexp
apparently comes only from using a tactic in an Ltac "let", which is
where I observed a problem.
|
|
This is to avoid excessive parentheses, in particular when printing
"constr:()" in "Print Ltac f".
|
|
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
Adding a file fixing #5996 and which uses this feature.
|
|
|
|
|
|
We do it so as to preserve non-focussing semantics for non-focussing
generic arguments.
This assumes that the code treats them consistently, which is not
enforced statically, but which is reasonable in the sense that when we
need a context for printing, we have no other choice as needing a
context and we needed one also at interpretation time.
|
|
This concerns pr_value and message_of_value.
This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".
But we also have more printers, satisfying e.g. request #5786.
|
|
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
|
|
|
|
|
|
In Tactic Notation and TACTIC EXTEND, when an argument not ending with
"_list_sep" was given with a separator, the separator was silently
ignored.
Now:
- we take it into account if it is a list (i.e. ending with "_list"), as if
"_list_sep" was given, since after all, the "_sep" is useless in the name.
- we fail if there is a separator but it is not a "_list" or "_list_sep".
|
|
We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
|
|
|
|
|
|
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
