| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
longer use camlp4.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
VernacDefinition
|
| | |/
|/| |
|
| | | |
|
| |/ |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Fixes #6490.
`prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`,
and adjusted to work with econstr.
This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where
`has_nodep_prod_after` counts both products and let-ins, but was only
being passed `mib.mind_nparams`, which does not count let-ins.
Replaced with (Context.Rel.length mib.mind_params_ctxt).
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| | | | |
|
| |\ \ \
| |_|/
|/| | |
|
| | |/
|/|
| |
| |
| | |
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |/ /
| |
| |
| |
| |
| | |
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| | |
| |
| |
| | |
It was the identity.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Extraction Language command
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
This is useful as it allows to reflect program_mode behavior as an attribute.
|
| | |/ / / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
|
| | |_|_|_|_|/ / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | | | | | |/ /
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
|
| | |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
(fix #6106)
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
same right-hand side.
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | |/ / /
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
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.
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
| | | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This is to have a better symmetry between CCases and GCases.
|
Jim Fehrle
Maxime Dénès
Gaëtan Gilbert
Vincent Laporte
Paul Steckler
Jasper Hugunin
Théo Zimmermann
Enrico Tassi
Emilio Jesus Gallego Arias
Jason Gross
Hugo Herbelin