| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
| |
The default hook value is the one used by CoqIDE
|
| | |
|
| |
|
|
|
|
|
|
| |
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
| | |
|
| |
|
|
|
| |
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
|
| | |
|
| | |
|
| |
|
|
| |
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
|
| |
|
|
|
| |
PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
|
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Hugo Herbelin
Arnaud Spiwack