| Commit message (Collapse) | Author | Age |
|---|
| |
|
| |
Closes #3801.
|
| |
|
|
|
|
|
|
| |
If the async-proofs-always-delegate is passed, workers are killed
only when the proof they computed is obsolete. If one jumps back
to a state that was computed by the worker (and not the master) instead
of (re)computing such state in the master ask the worker to send it
back.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
| | |
|
| |
|
|
| |
Even indirectly, if it depends on another state that in turn failed.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
When async_proofs_always_delegate is on, park proof workers and
dispatch to them queries. This flips the current way of printing
goals in PIDE base UIs: it is not the worker that prints all goals
while coomputing the states (and the dies), it is the UI that asks
for them when they are under the eyes of the user.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Generalize the old model by letting one park a worker and
by letting the (parked) worker be picky about the tasks it
picks up.
The use of that is the following: a proof worker, while performing
its "main" task (building a proof term) computes all the intermediate
states but returns only its main result. One can ask the worker
to hang around, and react to special tasks, like printing the
goals of an intermediate state.
|
| |
|
|
|
|
|
| |
This lets me have a pool of active workers of a fixed size,
plus a parking area where workers that completed their job
can stay holding their state (and eventually one can ask them
to query such state afterwards).
|
| |
|
|
| |
E.g. let a worker pick up only jobs he is able to deal with.
|
| |
|
|
| |
The default hook value is the one used by CoqIDE
|
| | |
|
| | |
|
| |
|
|
| |
in tactic unification.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel
meant that the channel was closed, resulting in a crash when interrupting
an idle coqtop from CoqIDE.
To prevent this, we block SIGINTs when reading in ide_slave.
|
| |
|
|
|
|
|
| |
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
|
| |
|
|
| |
at least when f is an evaluable reference.
|
| | |
|
| |
|
|
|
| |
when the arguments of a constructor can be moved at the place of the
variable on which destruct or induction applies.
|
| |
|
|
|
|
| |
This bug was affecting the VM and the native compiler, but only in the pretyper
(not the kernel). Types of arguments of fixpoints were incorrectly normalized
due to a missing lift.
|
| |
|
|
| |
a UserError to ease debugging.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
- removed the encapsulation in a Tactic Failure (I don't see why
setoid_rewrite should specifically raise a Fail - do I miss something?)
- avoid having twice a "Unable to satisfy ... constraints" message.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
quantified hypothesis in functional induction. This has apparently no
visible effect, probably because functional schemes do not have
non-dependent hypothesis in their branches besides induction
hypotheses which are anyway introduced at the top of the context.
|
| | |
|
| |
|
|
| |
anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
|
| |
|
|
| |
Daniel Schepler.
|
| |
|
|
| |
of the function are dependent.
|
| | |
|
| | |
|
Arnaud Spiwack
Enrico Tassi
Hugo Herbelin
Pierre Letouzey
Pierre-Marie Pédrot
Xavier Clerc
Maxime Dénès
Matthieu Sozeau