| Age | Commit message (Collapse) | Author |
|---|
|
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
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.
|
|
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".
|
|
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
|
|
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
|
Augment the "Illegal tactic application" error message with the number
of extra arguments passed.
Fixes BZ#5753.
|
|
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
|
|
|
|
(from module List).
|
|
|
|
This fixes bug 5650: evar (x : Prop) should not be slow.
|
|
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
|
|
|
|
|
|
|
|
|
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
|
|
|
|
Also taking into account a name in the return clause and in the
indices.
Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
|
|
|
|
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
ssreflect and coq code
|
|
|
|
a flag suspectingly renamed in a clearer way
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
|
|
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
|
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
|
|
This simplifies the API as before, inference of instances of type
classes was iff a type constraint was given.
We then export these both versions of interp_open_constr.
|
|
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
|
|
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
|
|
a goal with unresolved evars.
|
|
|
|
|
|
|
|
|
|
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
