I think it is available. But I a mnot sure we should reflect async proof yet. Let us have PG work as before, then we make the async proof queue working.
P. 2016-07-07 22:07 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>: > It looks like there are is a span representing the locked region of > the entire script, and then one span apiece for individual sentences. > When the end of a proof is reached, the sentence spans are glued > together. > > I've gotten rid of the gluing step, and now undo will work with the > steps of a completed proof. > > But I think the async mode will require something more complex, > because there can be multiple parts of the script that have been > processed, interleaved with unprocessed parts. > > It looks like the Stm machinery gives the dependencies between parts > of the script, and it may be the key to structuring spans. Do we know > if that's available through the XML interface? > > -- Paul > > > On Fri, Jul 1, 2016 at 4:43 AM, Pierre Courtieu <pierre.court...@cnam.fr> > wrote: >> I cc Enrico for this one. >> >> In pg/coq there should be one span at a time (but emacs uses overlays >> for other purposes). When a proof is finished (Qed or Save) the spans >> of the proof are glued together in a single span on the whole lemma. >> Coq's backtracking mechanism used to be unable to backtrack inside a >> proof and I never implemented a "replay" feature to workaround it. >> >> There is probably a way to avoid the glueing. >> >> But with the Stm machinery (do you use it Paul?) it should be much >> simpler to deal with spans. Enrico can you say a word on this? >> >> P. >> >> >> >> 2016-06-30 17:40 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>: >>> Hi all, >>> >>> I'm making decent progress on getting PG to work with the Coq >>> XML(ish) protocol. >>> >>> The main stumbling block I'm having is making sure the spans have >>> the correct structure. Those are implemented by Emacs overlays. >>> >>> Can someone explain what the structure of the spans should be, and >>> what metadata they should contain? Are there invariants that should >>> hold as a user steps through a proof? >>> >>> I'm told that CoqIDE has a similar notion, but there's just one span >>> per sentence in a script. I'm noticing multiple, overlapping spans in >>> PG. >>> >>> Currently, PG has machinery to know where a proof begins. If you >>> undo just past a finished proof, the entire proof is retracted. I'm >>> told that since 8.5, you can backtrack to the middle of a proof, so >>> that machinery is unneeded. >>> >>> -- 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
