[PG-devel] Coupling of items queue and proof shell
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. 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? -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Coupling of items queue and proof shell
2016-05-12 15:44 GMT+02:00 Paul A. Steckler : > 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
Re: [PG-devel] Coupling of items queue and proof shell
On Thu, May 12, 2016 at 6:28 PM, Pierre Courtieu wrote: > 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? In generic/proof-shell.el, there is procedure labeled "MAIN LOOP" that I believe pulls items off the queue. The procedures that add items to the queue are in the same file. All I'm suggesting is that the procedures that add items be moved out of this file, and the queue itself, so that my server code as well as the proof shell code can use the queue. > 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. The basic mechanism of queue handling won't change, just the code organization. It's an issue of software engineering, rather than an algorithmic issue. -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Coupling of items queue and proof shell
OK, that makes sense to me. P. 2016-05-12 19:25 GMT+02:00 Paul A. Steckler : > On Thu, May 12, 2016 at 6:28 PM, Pierre Courtieu > wrote: >> 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? > > In generic/proof-shell.el, there is procedure labeled "MAIN LOOP" that > I believe pulls items off the queue. > The procedures that add items to the queue are in the same file. > > All I'm suggesting is that the procedures that add items be moved out > of this file, and the queue itself, so that my server code as well as > the proof shell code can use the queue. > >> 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. > > The basic mechanism of queue handling won't change, just the code > organization. It's an issue of software engineering, rather than an > algorithmic issue. > > -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
