Re: [PG-devel] PG and Coq ideslave mode

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

Re: [PG-devel] PG and Coq ideslave mode

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 >>

[PG-devel] Coq search blacklist

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

[PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

buffer after processing it. In general you 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

Re: [PG-devel] Using sockets instead of shell

k-process'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.

[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

[PG-devel] Proof tree code

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

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

Re: [PG-devel] Proof tree code

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

Re: [PG-devel] Using sockets instead of shell

should try to replace it by 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 <st...@stecksoft.com>: >> Per the earlier discussion here, I'm developing a branch

Re: [PG-devel] PG and Coq ideslave mode

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 associat

Re: [PG-devel] PG and Coq ideslave mode

nctions 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 >> and Pierre Courtieu, maybe others on this

Re: [PG-devel] PG and Coq ideslave mode

sentially). >> 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. >> >>

Re: [PG-devel] PG and Coq ideslave mode

e with this point; I argued in this direction on a recent >> coq-dev thread. >> >> On 2016-05-05 12:24, Paul A. Steckler wrote: >>> I'm not a fan of this idea. The IDE and the prover should be only >>> loosely-coupled, with a clearly-defined communication protocol

Re: [PG-devel] PG and Coq ideslave mode

. -- Paul On Fri, May 6, 2016 at 3:51 PM, David Aspinall <david.aspin...@ed.ac.uk> 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, P

[PG-devel] Status of PGIP?

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

Re: [PG-devel] Span (overlay) structure in PG

, Clément Pit--Claudel <clement@gmail.com> 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 appropriate

[PG-devel] State button for Coq, needed?

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

Re: [PG-devel] State button for Coq, needed?

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 <hendrik.t...@fireeye.com> wrote: > Hi,

[PG-devel] Span (overlay) structure in PG

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

[PG-devel] Setting to lock buffer?

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

[PG-devel] Trace, thms buffers

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

Re: [PG-devel] pg-set-span-helphighlights

) > > On 2017-02-24 12:02, Paul A. Steckler wrote: >> 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

Re: [PG-devel] pg-set-span-helphighlights

urt...@cnam.fr> wrote: > Did 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 <clement@gmail.com> > a écrit : >> >> O

Re: [PG-devel] pg-set-span-helphighlights

ties. -- Paul > > On 2017-02-23 17:14, Paul A. Steckler wrote: >> 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 &

Re: [PG-devel] Supported version of Emacs

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