2016-05-12 15:44 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>:
> As I'm developing a separate server mode for PG, I'm noticing a tight
> coupling between the queue of items for processing and proof shells,
> which seems undesirable.
In PG these are in bijection indeed, except for queries that can be
sent to the prover only when the queue is empty. Yet another strong
invariant on which pg holds.
Ideally we should tend to have no queue of items at all, but a pool of
them and coq dealing with its dag structure. Once again as a first
step we can keep the queue structure but we should also remember that
the async mode frees us of that.
> To wit, the procedures `proof-extend-queue` and `proof-add-to-queue`
> are both found in generic/proof-shell.el. Probably there should be
> some way to extend the queue, independent of the proof shell (and
> server), then some way to process the queue that involves the proof
> shell or server.
> Does that make sense?
This is already the case AFAIK, in pg the queue is processed one
element at a time (waiting for a prompt between each), so in fact
there is a process that reads the queue and process it. No?
More generally can you take a few minutes explaining exactly where you
want to go. The thing that I don't get in your approach is the
If I understood well you still want to have a "locked region" as pg
has currently, right? Then I don't understand why the current
mechanism should change, especially if you manage to get a
pseudoprompt after each command.
> -- Paul
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list