| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
|
|
|
This change fixes performance problems in PIDE based user interfaces
|
|
|
|
Only tactics are taken into account.
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
Probably a regression introduced in some code refactoring.
Affects only PIDE based code.
|
|
coqtop mode.
|
|
|
|
|
|
Here nonsensical means a Qed/Defined without a Lemma.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Before this commit the worker was sending back a proof term
as built by tactics. The master receives the proof terms and
eventually (when one clicks on the gears in CoqIDE) check it
with the kernel. This meant that errors like the ones produced
by the "fix" tactics were discovered very late.
Now a worker checks with its kernel the proof term before sending it
back. The term is also checked by the master, eventually, but the
error is signaled early.
|
|
|
|
|
|
|
|
|
|
removing the need of thread creation in the interface.
|
|
|
|
|
|
|
|
|
|
This commits makes the concept of delegated and async more orthogonal.
A proof can be async but not delegated to a worker (if it is known
to be very small it is too much overhead to delegate to a worker).
A proof that is not async cannot be delegated to a worker.
An async proof that contains an error does not prevent Coq from continuing
the execution (interactive mode) and can be fixed without invalidating
the whole document (CoqIDE knows how to do that) even if it is processed
locally. It used to be the case only for delegated proofs, now it worker
for all the proofs that can be in principle delegated (doing it or not
is an implementation detail, an optimization).
|
|
|
|
|
|
Thanks the the previous patchset a worker can be asked to send
back "light" version of the system states. This is reasonably
efficient hence the idea of letting a worker hang around just to
hold system states for retrieval on demand is dropped.
|
|
|
|
|
|
|
|
|
|
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
|
|
the non-verbose mode which I guess one wants to obey whatever
interface is used, and restoring a policy ok for coqtop - maybe would
need a change if obeying the local verbose flag is not ok for PG or
Jedit).
|
|
|
|
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.
|
|
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.
|
