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 following: 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. P. > -- Paul > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
