| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
|
| | |
|
| | |
|
| |
|
|
|
| |
When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.
Fixes test-suite/success/apply.v
|
| |
|
| |
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.
|
| | |
|
Pierre-Marie Pédrot
Enrico Tassi
Arnaud Spiwack
Hugo Herbelin
Pierre Letouzey
Xavier Clerc
Maxime Dénès
Matthieu Sozeau