I've already mentioned the issue described below to Clément Pit-Claudel
and Pierre Courtieu, maybe others on this list have thoughts on it.
Proof General is welded to a model of receiving prompts from a prover.
After it's received a prompt, PG can send something back to the
prover.
The ideslave (
he current implementation to call these functions or the legacy
> ones depending on the version of Coq.
>
> What do you think?
> Clément.
>
> On 2016-05-05 09:48, Paul A. Steckler wrote:
>> I've already mentioned the issue described below to Clément Pit-Claudel
>
>> essentially).
>> 2. Implement support for these functions using Coq's new API model
>> 3. Modify the current implementation to call these functions or the legacy
>> ones depending on the version of Coq.
>>
>> What do you think?
>> Clément.
>&g
till seems undesirable to me.
-- Paul
On Thu, May 5, 2016 at 4:58 PM, Clément Pit--Claudel
wrote:
> Not entirely clear to me :) I think there'd be some amount of design work
> there as well.
>
> On 2016-05-05 10:39, Paul A. Steckler wrote:
>> With that toploop plugin installed o
gt;>> A plugin introduces a tight coupling between these components. Yes,
>>> it's only a plugin, so the scope of the coupling is limited. But it
>>> still seems undesirable to me.
>>>
>>> -- Paul
>>>
>>> On Thu, May 5, 2016 at 4:58 PM, Clém
old and the case we wanted to allow
> was input coming voluntarily from the prover to PG (think
> progress/annotations etc), rather than the other way around. - David
>
> On 06/05/2016 11:48, Paul A. Steckler wrote:
>> Proof General defines a shell mode, proof-shell, and an assoc
munication mechanism.
-- Paul
On Fri, May 6, 2016 at 3:51 PM, David Aspinall wrote:
> That sounds right (but could lead to confusion!). What I did was to fork a
> version of PG and cut it down to something fairly minimal. - D.
>
>
> On 06/05/2016 14:34, Paul A. Steckler wrote:
>
On Sat, May 7, 2016 at 3:33 PM, Clément Pit--Claudel
wrote:
> I don't think we should give it a different name yet; I think it would create
> a lot of confusion.
>
> We can phrase this differently: what you are currently writing is a library
> that implements the protocol spoken by Coq. Ideally,
A full fork would be problematic, because it would
>> loose this ability.
>>
>> Regarding the other part (coqserver), I think a coqdev thread would be more
>> appropriate.
>>
>> Clément.
>>
>> On 2016-05-07 02:48, Paul A. Steckler wrote:
>>>
On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel
wrote:
> I'm all for a cleanup of the PG codebase, of course. But I think we can do it
> slightly differently: starting with the current code, we can:
>
> * Tag a last-known good version (the current HEAD) for obsolete provers
> * Remove obsole
Per the earlier discussion here, I'm developing a branch (not fork) of
PG that operates in two ways, either the old REPL way where the prover
offers a prompt, and a new server way, where PG and the prover
exchange messages. I'm being coy about whether PG or the prover is the
server, due to differen
something else. Like a Logging
> buffer where xml noise is removed as much as possible. I don't know.
>
> P.
>
>
> 2016-05-11 11:11 GMT+02:00 Paul A. Steckler :
>> Per the earlier discussion here, I'm developing a branch (not fork) of
>> PG that operates in two w
You mean here the pipes that are created when running Elisp's start-process?
It looks like you'd setup a filter function for the Coq process to get
its output, and use process-send-string to send input to Coq.
I guess that's as easy as, or easier than sending data over sockets.
Yes, I'd like to
u want to remove it, since
>> otherwise lots of text will be accumulated, but in debug mode you can keep
>> it, à la comint-mode.
>>
>> Clément.
>>
>> On 2016-05-11 05:42, Paul A. Steckler wrote:
>>> Elisp has primitives for network reading and writing,
You're comparing make-network-process, then, with start-process?
When using sockets, coqtop works in a funny way, using two half-duplex
sockets. So if you used make-network-process, I think you'd get just
one of those sockets, and have to use Elisp's other network facilities
to manage the other so
#x27;es, actually :)
>
> You can `cl-define-struct' a pair of network process (and possibly wrap
> relevant function to work on pairs of half-channels) for convenience, too.
>
> Interestingly, you probably don't need a filter function on the two Emacs->
> Coq ones.
>
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 b
The code in generic/proof-tree appears to rely on proof shell modes.
Is the `prooftree' tool in common use among Coq users?
-- Paul
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgener
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 procedur
Just to note, I'm adding a configuration option to force the use of the
existing Emacs mode, so Prooftree will always be available.
-- Paul
On May 13, 2016 11:08, "Pierre Courtieu" wrote:
> 2016-05-13 9:49 GMT+02:00 Hendrik Tews :
> > For 2 and 5 I insert additional print commands into the queue
When Proof General starts coqtop, it issues this sequence of commands:
--
Add Search Blacklist "Private_" "_subproof".
Set Printing Depth 50 .
Remove Search Blacklist "Private_" "_subproof".
Add Search Blacklist "Private_" "_subproof".
--
The Remove/Add are issued from a single PG-internal call to
one with and one without support for 8.5, we'd
> have just one, with an extra compatibility layer inserted between PG and Coq
> when using 8.4.
>
> Cheers,
> Clément.
>
> On 2016-05-05 09:48, Paul A. Steckler wrote:
>> I've already mentioned the issu
On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel
wrote:
> My proposal was to dump the entire proof-shell part, indeed. I agree with you
> that it would make everything much easier, and I think that would be nice.
> We'd write a semi-working shim to not leave out 8.4 entirely, and drop the
On Sat, Jun 11, 2016 at 3:59 PM, Clément Pit--Claudel
wrote:
>> If coqtop works with s-expressions, is the ability to use XML
>> maintained? If so, then CoqIDE can still work as it does. If not,
>> then CoqIDE is orphaned, yes? Maybe not a great idea to have coqtop
>> support two separate protocol
I'm the one who'll be doing the programming on this project.
As a long-time consumer of OCaml Weekly News, I'm happy to reciprocate
by exposing what APIs are needed. :-)
The coqtop XML API concludes each response with a tag. We can
probably offer something to indicate when that's happened.
-- P
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
bly 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 :
>> Hi all,
>>
>> I&#
On Fri, Jul 8, 2016 at 5:35 AM, Enrico Tassi wrote:
> On Fri, Jul 08, 2016 at 10:10:49AM +0200, Pierre Courtieu wrote:
>> 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.
>
> As far as I k
each sentence, as I think you've done
in elcoq.
-- Paul
On Fri, Jul 8, 2016 at 12:23 PM, Clément Pit--Claudel
wrote:
> I think I got that working fine in elcoq. Did you have a look?
>
> Clément.
>
> On 2016-07-07 16:07, Paul A. Steckler wrote:
>> It looks like there are is
2016 at 2:30 AM, Clément Pit--Claudel
wrote:
> On 2016-07-08 19:06, Paul A. Steckler wrote:
>> So when you edit in a buffer, you send an StmCancel messages, you
>> get messages for each cancelled state, so you can just mark the
>> corresponding overlays appropriately. Yes?
>
>
itt
wrote:
> On 2016-06-16 15:44, "Paul A. Steckler" writes:
>
>> I'm the one who'll be doing the programming on this project.
>>
>> As a long-time consumer of OCaml Weekly News, I'm happy to reciprocate
>> by exposing what APIs are needed. :-)
What is the status of the PGIP code in Proof General?
Are there any provers that use the protocol?
-- Paul
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
I've made some fair headway in getting Proof General working with the
coqtop XMLish protocol. So now I'm working on some of the less-central
bits for that port.
There's a PG button, State, which in the REPL version of PG, sends
"Show." to coqtop to request the current goal.
I'm thinking this but
less-used buttons. After the new PG has had some use,
we could assess whether the State button can be scrapped.
-- Paul
On Mon, Aug 8, 2016 at 12:14 PM, Clément Pit--Claudel
wrote:
> On 2016-08-08 11:31, Paul A. Steckler wrote:
>> I've made some fair headway in getting Proof Gener
OK, I've left the State button in, and it's working with the XML
protocol. I moved it over a few positions, so that the new Check
button is always visible.
Thanks for all the feedback.
-- Paul
On Tue, Aug 9, 2016 at 3:58 AM, Hendrik Tews wrote:
> Hi,
>
> "Paul A. Stec
I'm doing some code cleanup on my PG/xml branch.
Are the trace and thms buffers used at all for Coq? The thms buffer is
not even mentioned in the PG manual.
-- Paul
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.
I'm trying to solve an issue with PG/xml:
https://github.com/psteckler/ProofGeneral/issues/75
I'm unable to reproduce the issue, I'm supposing because there's a
setting I'm missing.
Is there a setting in PG that locks a buffer and colors it red?
-- Paul
___
In my PG/xml fork, the Elisp profiler indicates the most expensive
procedure is `proof-done-advancing-other' (about 12% of the CPU
cycles). Most of the time in that procedure is allotted to
`pg-set-span-helphighlights'.
That procedure creates a daughter span with a context menu. In vanilla
PG, it
you try to unplug it to see if the speed up is significant?
> I guess it is useful only when going back and forth in a script is slow.
> P
>
> Le ven. 24 févr. 2017 à 01:19, Clément Pit--Claudel
> a écrit :
>>
>> On 2017-02-23 17:14, Paul A. Steckler wrote:
>> >
e helphighlight spans (in
`proof-script-clear-queue-spans-on-error'); I don't understand why
you'd delete just the vanilla spans.
The helphighlight spans have modification hooks that delete them. If
we reused the vanilla spans, we could add a modification hook that
just removes the
And I can confirm it's the span-making that takes the time.
If I set the properties on the existing vanilla span, the time is
about the same as just returning nil.
On Fri, Feb 24, 2017 at 11:46 AM, Paul A. Steckler wrote:
> On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
>
re are helphighlight
spans for proofs and sections, so you can hide them. I suppose I'll
have to work to restore this functionality. Of course, adding these
spans again will take additional run time.
-- Paul
On Fri, Feb 24, 2017 at 1:28 PM, Clément Pit--Claudel
wrote:
> Great news :)
>
I claim) of functionality.
-- Paul
On Fri, Feb 24, 2017 at 2:36 PM, Paul A. Steckler wrote:
> I just ran the experiment of setting the properties used in the
> helphighlight spans in the vanilla spans.
>
> All works well, until you try to hide a span. Indeed, the span gets
> h
On Thu, Nov 29, 2018 at 9:35 AM Emilio Jesús Gallego Arias wrote:
> In my opinion, it seems very likely that the branch will never reach a
> working state; mainly because it would be hard to justify putting time
> to fix it when you have other alternatives that allow a much lightweight
> and robus
On Thu, Nov 29, 2018 at 11:16 AM Emilio Jesús Gallego Arias
wrote:
> As of today, you have coq-serapi[1], which was specifically designed to
> make interaction with Emacs easy.
That helps a bit for some issues, but I think most of the bugs in the
async branch mostly relate to maintaining
unstate
> > That helps a bit for some issues, but I think most of the bugs in the
> > async branch mostly relate to maintaining unstated or unknown
> > invariants in the implementation.
>
> Umm, I'm not sure I share that view, I'd dare to say that for a start the
> new protocol would allow to drop 90% of t
46 matches
Mail list logo
