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.


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

Reply via email to