Re: [PG-devel] Use cl-lib instead of cl

[Clément Pit-Claudel]

On 15/12/2018 20.06, Stefan Monnier wrote:
> Hopefully, the one below will go through better.

Indeed, this one applied smoothly. Thanks!



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Use cl-lib instead of cl

[Clément Pit-Claudel]

On 13/12/2018 22.58, Stefan Monnier wrote:
> Here's another,

`git am` doesn't like this one :'(

Applying: Fix remaining uses of CL; Make files more declarative
error: acl2/acl2.el: does not match index
error: coq/coq-autotest.el: does not match index
error: coq/coq-db.el: does not match index
error: coq/coq-par-compile.el: does not match index
error: coq/coq-par-test.el: does not match index
error: coq/coq-seq-compile.el: does not match index
error: coq/coq-syntax.el: does not match index
error: etc/testsuite/pg-test.el: does not match index
error: generic/pg-autotest.el: does not match index
error: generic/pg-movie.el: does not match index
error: generic/pg-user.el: does not match index
error: generic/proof-script.el: does not match index
error: generic/proof-splash.el: does not match index
error: generic/proof-syntax.el: does not match index
error: generic/proof-useropts.el: does not match index
error: generic/proof-utils.el: does not match index
error: generic/proof.el: does not match index
error: obsolete/plastic/plastic.el: does not match index
Patch failed at 0001 Fix remaining uses of CL; Make files more declarative
The copy of the patch that failed is found in: .git/rebase-apply/patch
When you have resolved this problem, run "git am --continue".
If you prefer to skip this patch, run "git am --skip" instead.
To restore the original branch and stop patching, run "git am --abort".

Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Use cl-lib instead of cl (was: Supported version of Emacs)

[Clément Pit-Claudel]

On 12/12/2018 15.27, Stefan Monnier wrote:
 I'm happy to push it for you. Would you mind sending a copy as a `git
 format-patch` attachment, so that the commit is properly attributed?
>>> Here it is,
>> Pushed, thanks. Looking forward to more neat patches :)
> 
> Here's the next one.

Pushed as well. Thanks!



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 11/12/2018 18.52, Stefan Monnier wrote:
>> I'm happy to push it for you. Would you mind sending a copy as a `git
>> format-patch` attachment, so that the commit is properly attributed?
> 
> Here it is,

Pushed, thanks. Looking forward to more neat patches :)



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 11/12/2018 16.26, Stefan Monnier wrote:
> Is there something else I need to do for this patch to be installed

I'm happy to push it for you. Would you mind sending a copy as a `git 
format-patch` attachment, so that the commit is properly attributed?

Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 03/12/2018 12.15, Emilio Jesús Gallego Arias wrote:
> Emilio Jesús Gallego Arias  writes:
> 
>> - Isabelle / PIDE understands complete projects;
>> - reliable async support and integration with external tools;
>> - better error reporting and handling.
> 
> Some more: on the fly checking, real completion, semantic folding; I'm
> sure experienced Isabelle users can come up with some more tricks.

Got it, thanks.

Plenty of nice stuff to look forward to in future versions of Coq!

We've had some success on the F* side with keeping the protocol stable while 
adding new features.  I think the trick is to be conservative in the design of 
the core protocol, attempting to future-proof it somewhat (for example, you and 
I agreed that returning a pair of regions to indicate which segments a change 
invalidates is a bad idea; instead, it's much better to return a list of all 
invalidated regions, so that a future version of Coq can be more precise about 
which regions a change invalidates). Then you very seldom have to change the 
core protocol; instead, most improvements are new queries or new options for 
existing queries.

Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 03/12/2018 11.57, Emilio Jesús Gallego Arias wrote:
> In the first case, my opinion (and the one of quite a few of my
> colleagues) is yes, clearly ahead.

But can you give concrete examples of extra features that they have?
And, re the coupling, are these worth being stuck with a single editor?



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Indentation tests

[Clément Pit-Claudel]

I'd go with any large file in the source distribution of Coq. In fact, a good 
test might be to clone the Coq repo, reindent the whole standard library, check 
these changes in, then reindent again with your changes and look at the git 
diff.  I expect the standard library + the Coq test suite to cover all or 
almost all of the syntax of Coq.

Clément.

On 01/12/2018 10.24, Stefan Monnier wrote:
> I have a few tentative changes to coq-smie.el.
> Does someone have some kind of test-suite somewhere against which I can
> run my new code to try and avoid regressions?
> 
> Ideally, it should be fully automated, including fixing my bugs and
> outputting a Coq proof that the result is correct, but I'll settle for
> a long file that I need to reindent manually.
> 
> So far I have the coq/indent.v but it doesn't seem to include some cases
> that are mentioned in coq-smie.el, so I'm hoping someone has something
> a bit more complete.
> 
> 
> Stefan
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 29/11/2018 14.11, Emilio Jesús Gallego Arias wrote:
> Clément Pit-Claudel  writes:
>>> Note even for the mainline, coqtop-based branch, many hacks in the code
>>> could be removed today if so we wished.
>>
>> I'm not sure I understand this part
> 
> See for example:
> 
> - https://github.com/coq/coq/issues/7591
> - https://github.com/ProofGeneral/PG/issues/212
> 
> Among others, that would allow to drop all the code manipulating `Set
> Silent`, having to parse documents, etc...

Ah, yes, of course; but removing that code requires dropping support for old 
versions of Coq.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Supported version of Emacs

[Clément Pit-Claudel]

On 29/11/2018 06.12, Erik Martin-Dorel wrote:
> Clément and Pierre, what do you think about this?

Sounds good to me



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Proof General's ability to interpret ANSI escape code from a proof assistant

[Clément Pit-Claudel]

No at all; the ansi-color module in Emacs can take care of that easily.

Clément.

On 2018-01-24 01:06, Jim Fehrle wrote:
> Hi,
> 
>  
> 
> How difficult would it be for Proof General to support ANSI escape codes 
> (used to set color, bold, underline, etc.) embedded in the output of a proof 
> assistant?
> 
>  
> 
> (I’m getting started on making a few enhancements to Coq.  It’s been a long 
> time since I used emacs.  I’ve not used Proof General at all.)
> 
>  
> 
> Thanks,
> 
>  
> 
> Jim
> 
> 
> 
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Great news :)

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 at 11:46 AM, Paul A. Steckler <st...@stecksoft.com> 
> wrote:
>> On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
>> <clement@gmail.com> wrote:
>>> A wild guess: the extra runtime is due to adding extra overlays.  This was 
>>> needed in the original PG since there may not have been another overlay 
>>> covering exactly that region (because the locked region was one large 
>>> overlay).  But since there now is one overlay per small processed region, 
>>> that overlay can be reused in pg-set-span-helphighlights.
>>>
>>> Is that correct?
>>
>> I think you're right that it's the span creation is what adds the most time.
>>
>> In the original PG, there was already a span for each script item with
>> the "type" property set to "vanilla". Those spans have links to the
>> helphighlight spans. The helphighlight spans basically cover the same
>> piece of text as the vanilla spans, except for any whitespace on the
>> ends.
>>
>> In PG/xml, I'm already trimming any whitespace at the start of the
>> vanilla spans, because those are the spans that get colors, otherwise
>> the coloring looks bad. It may be possible to reuse the vanilla spans
>> to contain the properties that were being set in the helphighlight
>> spans. There is one call that also sets a face for these spans, which
>> may clobber a face that's already been set.
>>
>> Making this change may simplify the code in other ways. Currently,
>> there are separate calls to delete the vanilla spans and to delete the
>> helphighlight spans. In one instance, there's a call to delete the
>> vanilla spans, but not the 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 added properties.
>>
>>
>> -- 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
>>>> `pg-set-span-helphighlights'.
>>>>
>>>> That procedure creates a daughter span with a context menu. In vanilla
>>>> PG, it looks like the context menu also contains the last response
>>>> from Coq. In PG/xml, that's not so useful, since the last response is
>>>> an XML blob.
>>>>
>>>> The context menu has a Show/Hide menu item. I suppose that can be
>>>> useful. There's also a Copy menu item, but of course you can use
>>>> ordinary Emacs commands for that.
>>>>
>>>> Do we know if this functionality is widely-used? How grievous would it
>>>> be if I removed it?
>>>>
>>>> -- 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
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

A wild guess: the extra runtime is due to adding extra overlays.  This was 
needed in the original PG since there may not have been another overlay 
covering exactly that region (because the locked region was one large overlay). 
 But since there now is one overlay per small processed region, that overlay 
can be reused in pg-set-span-helphighlights.

Is that correct?

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
> `pg-set-span-helphighlights'.
> 
> That procedure creates a daughter span with a context menu. In vanilla
> PG, it looks like the context menu also contains the last response
> from Coq. In PG/xml, that's not so useful, since the last response is
> an XML blob.
> 
> The context menu has a Show/Hide menu item. I suppose that can be
> useful. There's also a Copy menu item, but of course you can use
> ordinary Emacs commands for that.
> 
> Do we know if this functionality is widely-used? How grievous would it
> be if I removed it?
> 
> -- Paul
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

On 2017-02-23 17:14, Paul A. Steckler wrote:
> That procedure creates a daughter span with a context menu. In
> vanilla PG, it looks like the context menu also contains the last
> response from Coq.

I use it from time to time; I think that's also what PG-movie is based on, 
though I don't think anyone really uses that.

> In PG/xml, that's not so useful, since the last response is an XML
> blob.

True, but doesn't that XML usually contain what the old PG would have called 
the "last response"? It would be either a message or a goal.

Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] -quick

[Clément Pit--Claudel]

On 01/06/2017 09:46 AM, Ralf Jung wrote:
> (I don't know if my previous mail got through, as I didn't get the mail
> myself via the list -- and I cannot access the list subscriber options
> to check whether I enabled getting my own mails, because the website is
> not working properly either. I informed the list owner about this.)

Your email did get through (thanks for the thoughts!). I'll let Hendrik reply 
on the technical aspects :)



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Status of PGIP?

[Clément Pit--Claudel]

On 2016-07-27 05:24, David Aspinall wrote:
> I would be sad to see support for other provers being taken away though.
>  We put a lot of effort into making it easy to configure Proof General
> to use with CLI tools (even bash).  Maybe the script management code
> could be refactored into a standalone mode.  I still see people in
> conferences cutting and pasting text into command lines!

Hi David,

In the case of bash, do you have more in mind that what comint-mode already 
does?

In general, I think it'll be possible to reinstate support for REPLs after we 
make the transition.  We're transitioning PG to a more permissive protocol 
(instead of the current one-question-one prompt-one response), and it shouldn't 
be too hard to write a wrapper for REPLs further down the line.

Cheers,
Clément.



signature.asc
Description: OpenPGP digital signature
___
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]

On 2016-07-09 21:18, Paul A. Steckler wrote:
> Looking at CJ's notes, I see that you only get a pair of state id's
> when there's a new focus. Otherwise, you just get a single state_id,
> which is the new tip.
> 
> That will make it easy to determine when to use a pair of locked
> spans, or just one of them.

Yup, absolutely.

> 
> On Sat, Jul 9, 2016 at 2:30 AM, 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 appropriately. Yes?
>>
>> Indeed, SerCoq makes things simpler here. With EditAt you send an EditAt 
>> instead of Cancel, but it's essentially the same otherwise in terms of 
>> messages sent. The one difference is in the response: SerCoq sends me 
>> individual Cancelled messages, whereas EditAt send you a single message with 
>> two state IDs indicating a range:
>>
>>> Maybe it would be better to lock the individual spans for each
>>> sentence, as I think you've done in elcoq.
>>
>> Yes, I think that would be the simplest. With EditAt you'll get a pair of 
>> states to cancel, which stands for a "geographical" range. For examples if 
>> states IDs are
>>
>> 1
>> 8
>> 18
>> 6
>> 3
>> 9
>>
>> and you get (18,9), you should cancel 18,6,3,9. The function overlays-in 
>> should help for this.
>>
> 



signature.asc
Description: OpenPGP digital signature
___
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]

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?

Indeed, SerCoq makes things simpler here. With EditAt you send an EditAt 
instead of Cancel, but it's essentially the same otherwise in terms of messages 
sent. The one difference is in the response: SerCoq sends me individual 
Cancelled messages, whereas EditAt send you a single message with two state IDs 
indicating a range:

> Maybe it would be better to lock the individual spans for each
> sentence, as I think you've done in elcoq.

Yes, I think that would be the simplest. With EditAt you'll get a pair of 
states to cancel, which stands for a "geographical" range. For examples if 
states IDs are

1
8
18
6
3
9

and you get (18,9), you should cancel 18,6,3,9. The function overlays-in should 
help for this.



signature.asc
Description: OpenPGP digital signature
___
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]

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



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

Hi Alan,

We're hoping to get a pretty flexible codebase in the end, but more details on 
your use case would be useful :) What are the main difficulties that you ran 
into with the current codebase ?

Clément.

On 2016-06-16 03:27, Alan Schmitt wrote:
> Hello Clément,
> 
> Will this rewrite be monolithic, or will it be possible to use it to
> interact with Coq through elisp? I'm particularly interested in
> improving org-babel support for Coq (which works but is not very
> robust).
> 
> Thanks,
> 
> Alan
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:51, Makarius wrote:
> Concerning the "new" prover APIs of Coq and Isabelle in general: I was
> in contact with Enrico Tassi when he introduced this for Coq -- it was
> part of our Paral-ITP project at that time. My general impression is
> that the new Coq API is more conservative than the PIDE protocol of
> Isabelle: PIDE is quite demanding on the other side to process a lot of
> information in real-time.

Not sure whether this is what you had in mind, but there does exist a PIDE 
implementation built on top of the new Coq API 
(https://bitbucket.org/coqpide/pidetop). It's used by at least one Coq IDE 
(Coqoon ­— it's pretty cool, btw).



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:41, Stefan Monnier wrote:
>> There might be a tiny minority of Isabelle users who did not follow new
>> releases in the last 2 years and are still using Isabelle2014 with Proof
>> General.  I don't see a problem with that: they just won't be able to
>> upgrade Proof General and remain stable on both.
> 
> In an ideal world, the new PG Coq code should make it easier to support
> the "new" Isabelle API.  It would be good for someone somewhat familiar
> with the "new" Isabelle API to keep an eye on the new PG Coq code (or for
> those working on the new PG Coq code to take a look at the "new"
> Isabelle API).

Thanks Stefan :) 

I share that hope; I think the new code will be a good basis for such a 
development. I've looked at a few other protocols over the last year, including 
the Isabelle protocol/PIDE, Dafny's and F*'s protocols, and some of the stuff 
that David wrote about PGIP; extending the new code to support these things 
should be much easier than it would have been previously.

Cheers,
Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:31, Makarius wrote:
> One could formally ask on the isabelle-users mailing list, if anybody
> wants to join pg-devel for further discussion, although I wouldn't
> expect much from it.

Thanks! Feel free to post such an email there, but I wouldn't press much for 
it: I share you analysis that staying with the current release is a good option 
for these people.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

[PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

Hey PG-devel,

Paul is starting to work on porting PG to support new features introduced in 
Coq 8.5 (in particular a new async API). You can see a demo of the new API in 
action at https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9 (note in particular 
how the last proof completes before the other ones are processed; note also 
that this isn't PG, just a prototype that I made hosted at 
https://github.com/cpitclaudel/elcoq/).

We had long on and off-list discussions on how to best do this, wondering how 
much of the existing proof-shell code could be reused and shared. The answer 
was "not much", mostly because Coq's new async protocol isn't compatible with 
the one-prompt-one-response model that PG relies on. Based on this, there were 
essentially three ways to go:

1. Abandon the current Proof General, and start a new Emacs mode entirely, 
gradually merging-in bits and pieces of Proof General (indentation code, syntax 
highlighting, etc).

2. Refactor PG to delimit new interfaces, and somehow support both the old REPL 
mode and the new async mode.

3. Refactor PG to use the new async mode, dropping the REPL and support for old 
proof assistants on the way.

I personally don't like option 1 at all.

Option 2 was considered and partly attempted, but it does turn out to be very 
costly to implement cleanly, and it adds to the complexity without bringing 
much: support for most other provers is partly broken, and the refactoring 
would not fix them.

Option 3 is relatively easy and lets us return quickly to fully supporting Coq 
in PG, thereby hopefully allowing PG to remain the editor of choice for Coq. 
Unfortunately, it also means that the next release of Proof General will not be 
backwards compatible.  We'll mitigate this by tagging a last-good version 
before removing the REPL-management code, and editing the README to clarify how 
to use that version.

For these reasons, we settled on option 3.  It would be useful to hear from 
current users of PG for proof assistants other than Coq, to see if we could 
think of a transition plan for them (in particular, if there exists a newer, 
asynchronous protocol for that proof assistant, it would be good to hear more 
about it with the hope of supporting is as well once the Coq port is 
completed).  It would also be useful to hear from users of less-commonly-used 
features of PG, so that we can make sure that they remain compatible. Proof 
Tree is one; what are the others?

Cheers,
Clément.




signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

On 2016-06-11 15:29, Paul A. Steckler wrote:
> On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel 
> <clement@gmail.com> 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 generic aspects. It would
>> probably make your/our lives simpler, at no significant loss, I
>> think.
> 
> I'm with you, as long as none of the other provers mind that PG will 
> no longer be available to them.

Great. PG wouldn't stop being available; they would just use the 
latest-released tag. There hasn't been much progress on the generic side for a 
while.

>> If we can, I think it would be good to use it, actually :) What do
>> you mean by leaving CoqIDE in the cold?
> 
> 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 protocols.

Emilio's S-Expressions are built on top of Enrico's Stm, so it isn't really two 
separate parts. Additionally, Emilio's protocol comes as a plugin.

> Or are you suggesting that CoqIDE switch to using s-expressions,
> also?

Emilio is working on that, IIUC.

>> Also, if we have an S-expression to REPL shim, we can use it with
>> 8.5 as well, and only get fancy (parallelism and all that) in 8.6,
>> or whatever comes next.
> 
> Right, if someone wants to stick with 8.5 and have parallelism, they 
> have CoqIDE available for that purpose.
> 
>> Maybe we should discuss this at the meeting on Tuesday. In the
>> meantime, I can run a small experiment with Emilio's code, if you
>> want.
> 
> Sure. I think a shim should be written in OCaml, and it might be
> able to use some of the Coq code for printing that shows up in the
> REPL.
> 
> One decision here is whether to use coqtop's -emacs prompt, or the 
> vanilla prompt. If we could dump the -emacs prompt, that's another 
> desirable (if small) simplification.

Wouldn't that go away from PG anyway? Since PG would only support the XML or 
SEXP protocol.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hey Paul,

On 2016-06-11 15:02, Paul A. Steckler wrote:
> I don't think it would be too difficult (although I'm still confused
> about some of how the XML protocol works).  In some (Pickwickian)
> sense, we already have an implementation of that in coqtop itself.
>
> PG already detects the version of coqtop, so it could fire up a shim
> when needed.

Yup, I wrote that code :)

> Of course, this approach increases system complexity, and substitutes
> new code for code known to work adequately.
> 
> OTOH, such a project would allow us to remove the proof shell code
> specifically for Coq in PG. Then the question would become whether to
> keep any of the generic proof shell code around for other provers. I
> just looked into Lean, which appears to hijack emacs in its own way,
> so probably there isn't interest in using PG w/ Lean.
> 
> If the decision is to dump the proof shell entirely, PG becomes much simpler.

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 generic 
aspects. It would probably make your/our lives simpler, at no significant loss, 
I think.

> Then there's the question of how Emilio's new s-expression protocol
> fits in the picture. Embracing that would fit well with PG, and
> s-expressions are warmer/fuzzier than XML, but doing so might leave
> CoqIDE out in the cold, and also require an s-expression to XML shim
> for 8.5 and 8.6. So probably a non-starter.

If we can, I think it would be good to use it, actually :) What do you mean by 
leaving CoqIDE in the cold?
Also, if we have an S-expression to REPL shim, we can use it with 8.5 as well, 
and only get fancy (parallelism and all that) in 8.6, or whatever comes next.

Maybe we should discuss this at the meeting on Tuesday. In the meantime, I can 
run a small experiment with Emilio's code, if you want.

Clément.

> On Sat, Jun 11, 2016 at 12:48 PM, Clément Pit--Claudel
> <clement@gmail.com> wrote:
>> Hey Paul,
>>
>> I've been thinking about this. How hard do you think it would be to create 
>> an emulation layer that simulates the XML API on top of Coq 8.4?
>> Essentially, how hard would it be to have a program in the middle that 
>> translates uses of the 8.5 API to use Coq 8.4's REPL? It wouldn't have to 
>> replicate all of the functionality, of course; just a small subset of it 
>> would probably be fine.
>>
>> This could allow for a more radical paradigm shift inside of PG: instead of 
>> maintaining two code paths, 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 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 (politically incorrectly-named) mode in Coq, developed
>>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>>> from an IDE, without first offering a prompt.
>>>
>>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
>>> prompt regexp would have to look for both the closing tag, and the
>>> single-tag version, .
>>>
>>> Even with that, there's still a bootstrapping issue, because there's
>>> no prompt to s start with. I could probably modify PG to not look for
>>> that first prompt.
>>>
>>> Is there some good way to handle this?
>>>
>>> -- 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
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hey Paul,

I've been thinking about this. How hard do you think it would be to create an 
emulation layer that simulates the XML API on top of Coq 8.4?
Essentially, how hard would it be to have a program in the middle that 
translates uses of the 8.5 API to use Coq 8.4's REPL? It wouldn't have to 
replicate all of the functionality, of course; just a small subset of it would 
probably be fine.

This could allow for a more radical paradigm shift inside of PG: instead of 
maintaining two code paths, 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 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 (politically incorrectly-named) mode in Coq, developed
> for CoqIDE abandons that model. In that mode, Coq just waits for XML
> from an IDE, without first offering a prompt.
> 
> In ideslave mode, it seems that Coq sends back responses wrapped in
>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
> prompt regexp would have to look for both the closing tag, and the
> single-tag version, .
> 
> Even with that, there's still a bootstrapping issue, because there's
> no prompt to s start with. I could probably modify PG to not look for
> that first prompt.
> 
> Is there some good way to handle this?
> 
> -- Paul
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Coq search blacklist

[Clément Pit--Claudel]

yes: there's a user-facing option called coq-search-blacklist-string.
It's set to the same defaults as Coq, but if you change it these calls will 
look different.

On 2016-05-26 13:43, Paul A. Steckler wrote:
> 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 reset the
> search blacklist. But that call seems redundant, given the initial
> Add.
> 
> Is there a justification for this sequence of commands?
> 
> -- Paul
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Proof tree code

[Clément Pit--Claudel]

I think this would be the right strategy; Hendrik has been pretty good at 
keeping it up to until this point :)

On 2016-05-12 12:33, Pierre Courtieu wrote:
> I don't know. It is a nice peace of code. Maybe we can ask Hendrik to
> port it once you have something working.
> 
> P.
> 
> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler :
>> 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/proofgeneral-devel
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hey Paul,

I don't think it will make much of a difference, so you should feel free to go 
for sockets. They are very similar to processes in Emacs, so in practice you'll 
do essentially the same, namely accumulate the output that you get from Coq 
into a buffer until you have a full message. You can then. possibly based on 
the value of a debug flag, either remove or not that output from the 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 primitives for network reading and writing, so the actual
> Emacs mode where code runs can be anything.
> 
> Yes, I had meant to mention a logging facility. There could be a
> dedicated buffer showing the traffic, or a simplified version of it
> could be sent to *Messages*.
> 
> -- Paul
> 
> 
> On Wed, May 11, 2016 at 11:32 AM, Pierre Courtieu
>  wrote:
>> Hi Paul,
>>
>> AFAICT this seems a good way to go. Does scomint support the read and
>> write on sockets?
>>
>> The ability to "see" the coq session is very helpful for debugging and
>> maybe you 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 :
>>> 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 difference of opinion on that score in the Coq
>>> community.
>>>
>>> When operating using a REPL, communication with the prover uses an
>>> Emacs mode derived from PG's scomint mode, which is a simplified
>>> version of the Emacs-standard comint mode. The original comint mode
>>> was designed for interactive use, such as when running an interpreter.
>>> Having a similar mode for PG makes sense, because provers have
>>> historically worked in a similar way, taking input via stdin and
>>> printing output on stdout. When running Coq via PG, I can even open
>>> the *coq* buffer that uses its shell mode and interact directly with
>>> the prover.
>>>
>>> For the new server way of working, it's possible to do something
>>> similar for Coq, because coqtop can work with stdin and stdout using
>>> the -main-channels argument. But maybe that's not a great way to go.
>>> First, it's not likely that users will want to interact with the
>>> prover in a shell, because it's too hard to use the XML syntax
>>> manually. Second, the shell mode is fairly complex, in ways that maybe
>>> we can avoid.
>>>
>>> As an alternative, you can give coqtop's -main-channels argument port
>>> options, that allow it to communicate over sockets. On the PG side,
>>> instead of using a shell mode, we'd run Elisp code that would read and
>>> write over the sockets. After it's read something, the XML would be
>>> interpreted, calling other code when needed (writing out a response or
>>> goal, for example).  There would still need to be code that's
>>> currently done by the shell mode, such as firing up the prover, and
>>> maybe some of the non-prompt-related regexp matching.
>>>
>>> Does a socket-based approach make sense? What am I losing if I don't
>>> use a shell mode?
>>>
>>> -- 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
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

On 2016-05-07 14:37, Paul A. Steckler wrote:
> On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel <clement@gmail.com> 
> 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 obsolete provers
>> * Rename the "generic/" folder to "REPL/"
>> * Ensure that the separation between the "coq/" subfolder and the "generic/" 
>> subfolder is clean; that is, check which functions in "generic/" the "coq/" 
>> part calls (this is our "implicit API"), and ensure that nothing on the 
>> "coq/" side depends on the REPL model; anything that does is probably a 
>> mistake.
> 
> Yes, there is some code there that depends on the REPL model. See, for
> example, coq-last-prompt-info in coq/coq.el.

I see, thanks. Although for this particular example, it's mostly 
last-prompt-info not having an ideal name; in a sense, this is just a function 
that returns the current state of the proof (how many proofs are currently 
pending, etc).

>> It other words, my claim is that as part of a hypothetical fork we would 
>> already have to clean up the "coq/" subdirectory. Once this is done, it 
>> should be relatively easy to have support for both the REPL and the XML 
>> model in the same codebase. My hunch is that a very significant majority of 
>> the "coq/" subfolder does not depend on PG internals, since it uses clean 
>> interface functions to ask questions to the prover.
> 
> A lot of the code in there uses regexps to work out what the prover
> has sent, which is not so clean, IMHO. Just a thought, it might be
> better if that information was explicit in the XML, by using
> particular tags or attributes to flag items of interest. We could
> abstract over these approaches, and use regexp-matching for the REPL
> approach, and XML parsing in the other approach. That would give a
> clean, representation independent interface. The current XML
> essentially just wraps the textual output, and so we'd still use
> regexp-matching for now.

That would be great, and I think your last point is the key. We can just strip 
the XML code from responses for now.

> I think the approach you've outline is do-able, but again, I do have
> concerns about the complexity that it brings.

Anything that brings in complexity only for backwards compatibility we should 
avoid. However, if ensuring some level of backwards compatibility helps us 
reduce our technical debt, then that's good :) Ideally, we'd end up with 
multiple mostly-independent components: a tree-window display layer with text 
spans, a generic driver layer that implements basic UI functionality (moving 
around, etc), an implementation of the Coq API, and coq-specific package that 
implements syntax highlighting, indentation, and other Coq-only things. 
Concretely, this won't happen all at once, of course.

Cheers,
Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

On 2016-05-07 13:44, Paul A. Steckler wrote:
> OK, you'll need to explain the binding between plug-ins and PG to me.

I think this connects to my previous email. Company-coq uses PG as an interface 
to Coq (thus very little in it depends on how PG communicates with Coq, and I 
could fix anything that does: it only depends on the interface that PG 
exposes). In terms of functions, the only ones that it uses from PG itself are 
these:

  (fun proof-shell-invisible-command "ext:proof-shell.el" cmd)
  (fun proof-shell-available-p "ext:proof-shell.el")
  (fun proof-shell-live-buffer "ext:proof-shell.el")
  (fun proof-shell-ready-prover "ext:proof-shell.el")
  (fun proof-unprocessed-begin "ext:proof-script.el")
  (fun proof-goto-point "ext:pg-user.el")



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hi Paul,

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, we would be able to plug 
that library straight into proof general. Unfortunately, that isn't the case 
today. So, we'll have to modify PG. That's fine :)

One particular strong point of proof general is its ability to talk to multiple 
versions of Coq. 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:
> After hacking on PG all yesterday, and working out how to dispatch
> between two shell modes, I think a forked, Coq-only version is the
> better solution. Name suggestions? :-)
> 
> At the other end, I think that there should be a separate binary for
> the XML (or whatever it turns out to be) protocol, say `coqserver'.
> It's operating in a different way than coqtop-as-a-REPL. That would be
> simplify the codebase for coqtop. Although I haven't yet dealt with
> the extra channels that the toploop-coqide mode gives, I'm still
> liking the idea of using HTTP and a REST API as the basic
> communication mechanism.
> 
> -- 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, Paul A. Steckler wrote:
>>>
>>> The proof-shell mode comes with a lot of associated state, like
>>> regexps, buffers,  etc. Some bits of that state would be useful in the
>>> new mode I'm creating, others not.
>>>
>>> I'm thinking that I can share the same state variables for the new
>>> mode, because I'll never have an active proof shell mode and the new
>>> mode active at the same time. Yes?
>>> I'd hate to have to duplicate state.
>>>
>>> If I load two .v files in emacs, it seems I can only work on one at a
>>> time using Proof General, and there's only one proof-shell mode window
>>> active.
>>>
>>> -- Paul
>>>
>>>
>>> On Fri, May 6, 2016 at 3:15 PM, David Aspinall <david.aspin...@ed.ac.uk>
>>> wrote:
>>>>
>>>> I did something like this once to support PGIP, which was a sort of
>>>> pre-cursor of PIDE based on exchanging XML messages. You can find the
>>>> source in the CVS repo PG Kit repo (Kit/src/pgemacs).  But it probably
>>>> isn't useful: it's about 10 years 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 associated
>>>>> message filter. My thought now is to define an alternate-universe
>>>>> shell mode, proof-shell-noprompt and an associated message filter.
>>>>>
>>>>> -- Paul
>>>>>
>>>>>
>>>>>
>>>>> On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu
>>>>> <pierre.court...@cnam.fr> wrote:
>>>>>>
>>>>>> I am sorry to say that I already asked myself about everything you
>>>>>> asked here, and, despite you suggest more smart answers than I did
>>>>>> myself I don't see any good enough idea yet. About the prompt: a *lot*
>>>>>> of things (everything really) in pg depend on the fact that 1 command
>>>>>> = 1 prompt exactly.
>>>>>>
>>>>>> Once again, don't dismiss starting from scratch without thinking a
>>>>>> while about it. Actually large parts of pg could be reused.
>>>>>>
>>>>>> P.
>>>>>>
>>>>>>
>>>>>> 2016-05-05 19:59 GMT+02:00 Clément Pit--Claudel
>>>>>> <clement@gmail.com>:
>>>>>>>
>>>>>>> I entirely agree 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 prov

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

[Clément Pit--Claudel]

On 2016-05-06 09:34, Paul A. Steckler wrote:
> If I load two .v files in emacs, it seems I can only work on one at a
> time using Proof General, and there's only one proof-shell mode window
> active.

That's correct.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

I entirely agree 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 between
> them.
> 
> 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ément Pit--Claudel
> <clement@gmail.com> 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 on the coqtop side installed, what
>>> does Proof General see from its shell?
>>>
>>> -- Paul
>>>
>>> On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel
>>> <clement@gmail.com> wrote:
>>>> Hi Paul,
>>>>
>>>> Here's another approach that I forgot to mention: we could build a 
>>>> separate Emacs toploop as a plugin, which would inherit most of CoqIDE's 
>>>> toploop (you know that I have mixed feelings about that, but it may be the 
>>>> most pragmatic approach).
>>>>
>>>> Clément.
>>>>
>>>> On 2016-05-05 10:17, Clément Pit--Claudel wrote:
>>>>> Hi Paul,
>>>>>
>>>>> You could indeed modify PG to handle the first prompt differently, or 
>>>>> even Coq.
>>>>> In the long run, though, I don't think the approach is sustainable. PG is 
>>>>> very much hardcoded to expect one prompt for every query it sends: thus, 
>>>>> even though you may get something working pretty quickly by hacking 
>>>>> around this prompt thing, I think we'll see more breakages with every 
>>>>> evolution of the new protocol.
>>>>>
>>>>> Here's a slightly different idea. Right now, PG adds an abstraction layer 
>>>>> on top of a REPL model. What you could do is reimplement the same 
>>>>> abstraction, but on top of Coq's new asynchronous model. Concretely, my 
>>>>> suggestion is to make a separate library to talk to Coq's new API, which 
>>>>> would provide the same interface (proof-shell-invisible-command, 
>>>>> proof-shell-ready-prover, proof-shell-invisible-cmd-get-result, etc.).
>>>>>
>>>>> I think this would make your life easier. You would:
>>>>>
>>>>> 1. Identify a small (hopefully) collection of functions that 
>>>>> Coq-ProofGeneral actually depends on (some sort of semi-explicit 
>>>>> interface, 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.
>>>>>
>>>>> 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 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 (politically incorrectly-named) mode in Coq, developed
>>>>>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>>>>>> from an IDE, without first offering a prompt.
>>>>>>
>>>>>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>>>>>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
>>>>>> prompt regexp would have to look for both the closing tag, and the
>>>>>> single-tag version, .
>>>>>>
>>>>>> Even with that, there's still a bootstrapping issue, because there's
>>>>>> no prompt to s start with. I could probably modify PG to not look for
>>>>>> that first prompt.
>>>>>>
>>>>>> Is there some good way to handle this?
>>>>>>
>>>>>> -- 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
>>>>>
>>>>
>>>>
>>>> ___
>>>> ProofGeneral-devel mailing list
>>>> ProofGeneral-devel@inf.ed.ac.uk
>>>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>>>
>>
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

On 2016-05-05 10:36, Paul A. Steckler wrote:
> So you're suggesting that the abstractions in the generic layer could
> be re-implemented. 

Yup, essentially :)

> I wonder if this could done by providing a switch
> in the generic layer that says, "use prompts", or "use async
> messages", and then using the appropriate implementation. Maybe that's
> too optimistic. It might be that the abstractions in the generic layer
> just aren't a good fit for async messages, but I don't yet have a
> sense of that one way or the other.

I think most things should work fairly well (PG already has support for queries 
with callbacks). One issue may be that PG uses one large overlay covering the 
entire "processed" region of the buffer, so it may need adjustments to support 
having unprocessed regions mixed with processed regions.

Clément.

> On Thu, May 5, 2016 at 4:17 PM, Clément Pit--Claudel
> <clement@gmail.com> wrote:
>> Hi Paul,
>>
>> You could indeed modify PG to handle the first prompt differently, or even 
>> Coq.
>> In the long run, though, I don't think the approach is sustainable. PG is 
>> very much hardcoded to expect one prompt for every query it sends: thus, 
>> even though you may get something working pretty quickly by hacking around 
>> this prompt thing, I think we'll see more breakages with every evolution of 
>> the new protocol.
>>
>> Here's a slightly different idea. Right now, PG adds an abstraction layer on 
>> top of a REPL model. What you could do is reimplement the same abstraction, 
>> but on top of Coq's new asynchronous model. Concretely, my suggestion is to 
>> make a separate library to talk to Coq's new API, which would provide the 
>> same interface (proof-shell-invisible-command, proof-shell-ready-prover, 
>> proof-shell-invisible-cmd-get-result, etc.).
>>
>> I think this would make your life easier. You would:
>>
>> 1. Identify a small (hopefully) collection of functions that 
>> Coq-ProofGeneral actually depends on (some sort of semi-explicit interface, 
>> 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.
>>
>> 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 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 (politically incorrectly-named) mode in Coq, developed
>>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>>> from an IDE, without first offering a prompt.
>>>
>>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
>>> prompt regexp would have to look for both the closing tag, and the
>>> single-tag version, .
>>>
>>> Even with that, there's still a bootstrapping issue, because there's
>>> no prompt to s start with. I could probably modify PG to not look for
>>> that first prompt.
>>>
>>> Is there some good way to handle this?
>>>
>>> -- 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
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

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 on the coqtop side installed, what
> does Proof General see from its shell?
> 
> -- Paul
> 
> On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel
> <clement@gmail.com> wrote:
>> Hi Paul,
>>
>> Here's another approach that I forgot to mention: we could build a separate 
>> Emacs toploop as a plugin, which would inherit most of CoqIDE's toploop (you 
>> know that I have mixed feelings about that, but it may be the most pragmatic 
>> approach).
>>
>> Clément.
>>
>> On 2016-05-05 10:17, Clément Pit--Claudel wrote:
>>> Hi Paul,
>>>
>>> You could indeed modify PG to handle the first prompt differently, or even 
>>> Coq.
>>> In the long run, though, I don't think the approach is sustainable. PG is 
>>> very much hardcoded to expect one prompt for every query it sends: thus, 
>>> even though you may get something working pretty quickly by hacking around 
>>> this prompt thing, I think we'll see more breakages with every evolution of 
>>> the new protocol.
>>>
>>> Here's a slightly different idea. Right now, PG adds an abstraction layer 
>>> on top of a REPL model. What you could do is reimplement the same 
>>> abstraction, but on top of Coq's new asynchronous model. Concretely, my 
>>> suggestion is to make a separate library to talk to Coq's new API, which 
>>> would provide the same interface (proof-shell-invisible-command, 
>>> proof-shell-ready-prover, proof-shell-invisible-cmd-get-result, etc.).
>>>
>>> I think this would make your life easier. You would:
>>>
>>> 1. Identify a small (hopefully) collection of functions that 
>>> Coq-ProofGeneral actually depends on (some sort of semi-explicit interface, 
>>> 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.
>>>
>>> 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 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 (politically incorrectly-named) mode in Coq, developed
>>>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>>>> from an IDE, without first offering a prompt.
>>>>
>>>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>>>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
>>>> prompt regexp would have to look for both the closing tag, and the
>>>> single-tag version, .
>>>>
>>>> Even with that, there's still a bootstrapping issue, because there's
>>>> no prompt to s start with. I could probably modify PG to not look for
>>>> that first prompt.
>>>>
>>>> Is there some good way to handle this?
>>>>
>>>> -- 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
>>>
>>
>>
>> ___
>> ProofGeneral-devel mailing list
>> ProofGeneral-devel@inf.ed.ac.uk
>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hi Paul,

Here's another approach that I forgot to mention: we could build a separate 
Emacs toploop as a plugin, which would inherit most of CoqIDE's toploop (you 
know that I have mixed feelings about that, but it may be the most pragmatic 
approach).

Clément.

On 2016-05-05 10:17, Clément Pit--Claudel wrote:
> Hi Paul,
> 
> You could indeed modify PG to handle the first prompt differently, or even 
> Coq.
> In the long run, though, I don't think the approach is sustainable. PG is 
> very much hardcoded to expect one prompt for every query it sends: thus, even 
> though you may get something working pretty quickly by hacking around this 
> prompt thing, I think we'll see more breakages with every evolution of the 
> new protocol.
> 
> Here's a slightly different idea. Right now, PG adds an abstraction layer on 
> top of a REPL model. What you could do is reimplement the same abstraction, 
> but on top of Coq's new asynchronous model. Concretely, my suggestion is to 
> make a separate library to talk to Coq's new API, which would provide the 
> same interface (proof-shell-invisible-command, proof-shell-ready-prover, 
> proof-shell-invisible-cmd-get-result, etc.).
> 
> I think this would make your life easier. You would:
> 
> 1. Identify a small (hopefully) collection of functions that Coq-ProofGeneral 
> actually depends on (some sort of semi-explicit interface, 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.
> 
> 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 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 (politically incorrectly-named) mode in Coq, developed
>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>> from an IDE, without first offering a prompt.
>>
>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
>> prompt regexp would have to look for both the closing tag, and the
>> single-tag version, .
>>
>> Even with that, there's still a bootstrapping issue, because there's
>> no prompt to s start with. I could probably modify PG to not look for
>> that first prompt.
>>
>> Is there some good way to handle this?
>>
>> -- 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
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

[Clément Pit--Claudel]

Hi Paul,

You could indeed modify PG to handle the first prompt differently, or even Coq.
In the long run, though, I don't think the approach is sustainable. PG is very 
much hardcoded to expect one prompt for every query it sends: thus, even though 
you may get something working pretty quickly by hacking around this prompt 
thing, I think we'll see more breakages with every evolution of the new 
protocol.

Here's a slightly different idea. Right now, PG adds an abstraction layer on 
top of a REPL model. What you could do is reimplement the same abstraction, but 
on top of Coq's new asynchronous model. Concretely, my suggestion is to make a 
separate library to talk to Coq's new API, which would provide the same 
interface (proof-shell-invisible-command, proof-shell-ready-prover, 
proof-shell-invisible-cmd-get-result, etc.).

I think this would make your life easier. You would:

1. Identify a small (hopefully) collection of functions that Coq-ProofGeneral 
actually depends on (some sort of semi-explicit interface, 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.

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 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 (politically incorrectly-named) mode in Coq, developed
> for CoqIDE abandons that model. In that mode, Coq just waits for XML
> from an IDE, without first offering a prompt.
> 
> In ideslave mode, it seems that Coq sends back responses wrapped in
>  tags, so you can use that as a pseudo-prompt. Hmm, I think the
> prompt regexp would have to look for both the closing tag, and the
> single-tag version, .
> 
> Even with that, there's still a bootstrapping issue, because there's
> no prompt to s start with. I could probably modify PG to not look for
> that first prompt.
> 
> Is there some good way to handle this?
> 
> -- Paul
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

[PG-devel] Moving to ELPA!

[Clément Pit--Claudel]

Hi pg-devel folks,

TL;DR: Please get in touch with me if you've made significant contributions to 
the PG source code (> 10 lines total); we need an FSF copyright assignment from 
you to include PG in Emacs.

Pierre and I, and Stefan, are looking for ways to make Proof General easier to 
install for our users, and to relieve David of some of the maintenance burden. 
Moving to Github was a good step, but it's not the whole story; in particular, 
we're still dependent on David to maintain the website, and release packages 
for various Linux distributions.

One significant change since PG was launched is how Emacs packages are 
typically distributed: it used to be the case that packages would be either 
installed from a source code repository, or shared as tarballs, or through the 
package managers of Linux distributions; but Emacs now has (and has had for a 
while) it's own package manager. Migrating to this would make a lot of things 
simpler for us:

* No need for per-distribution packages
* No need to manage a complex release process
* No need for complex installation instructions
* We could depend on other packages: for example we could depend on the latest 
mmm-mode instead of vendoring it, or we could use the seq library, etc. (this 
has been a pain point for me while working on PG patches: I can't use features 
of external libraries at all)
 
The move to Github went pretty smoothly, so I think now is a good time to go 
one step further and move to ELPA. ELPA is the Emacs Lisp Package Archive, the 
main FSF-maintained package repository for Emacs. Choosing this package archive 
will have the additional advantage that we will be part of the official Emacs 
ecosystem: it'll be easier for us to ask for help, for example.

Two things need to be done for this:

* A general cleanup to be a good citizen of the package eco-system; Stefan will 
do it :)
* Copyright assignments: hosting packages in the GNU Emacs package archive 
requires them; see https://www.gnu.org/licenses/why-assign.html for more info. 
The broad idea is that as we transfer PG into Emacs, it becomes covered by FSF; 
that doesn't make a big difference in the end, since it stays GPL.

Please do let me know if you already have the forms on file, too.

Cheers and thanks for your help in making PG easier to install for our users, 
and to hack on for everyone,
Clément.



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Migrating Proof-General to Git

[Clément Pit--Claudel]

Hi David et al,

I'll do the migration of the CVS repo this week-end, then. Hopefully I don't 
run into trouble.

Cheers,
Clément.

On 09/18/2015 05:54 AM, David Aspinall wrote:
> Hi Pierre/all,
> 
> Sorry for delay replying, I was away then returned but now very busy
> with start of term...
> 
> Have made a new Admin team now with you and Clément as members.
> 
> BTW, a mapping of names->emails is in the Makefile somewhere, although
> it may be incomplete  (try "make ChangeLog").
> 
> If we're going to switch to Github properly I'd like to switch off the
> cvs server and then update the webpages, would you be able to help with
> the web page updates too?  There is another repo that I can add to GitHub.
> 
>  - David
> 
> 
> On 14/09/2015 17:00, Pierre Courtieu wrote:
>> Hi pg dev!
>>
>> Trying to wake up this thread 5 months later.
>>
>> Coq-8.5 is not yet released but its beta version is already quite
>> spread and used. IMHO it is the right time for a release of PG.
>>
>> I suggest that Clément performs the migration to github now and that
>> we make a release quickly from git. The best would be an elpa (or
>> melpa) package release + a tarball.
>>
>> David is it ok for you?
>>
>> Best regards,
>> Pierre
>>
>>
>>
>>
>>
>>
>>
>> 2015-04-28 14:36 GMT+02:00 Clément Pit--Claudel <clement@gmail.com>:
>>> On 04/28/2015 04:53 AM, David Aspinall wrote:
>>>> Hello Clément,
>>>>
>>>> Sorry I haven't looked in detail yet, hope soon.  Thanks for sending the
>>>> tips of what you did.  I want to try again to get the names right and
>>>> maybe some other minor surgery (looking at reposurgeon for that but
>>>> haven't tried it yet).
>>>
>>> No problem, thanks for the quick response!
>>> cvs2git has a mapping of cvs usernames to git usernames, so it should just 
>>> be a matter of finding the names and emails of each PG developer.
>>>
>>>> I think your suggestion for Trac is sensible.  We might leave it up but
>>>> make it read only, perhaps.
>>>
>>> That sounds great.
>>>
>>>> I've made a team for PG developers on GitHub, Clément you are invited,
>>>> anyone else please let me know your GitHub username.
>>>
>>> Great, thanks!
>>>
>>>>  - David
>>>>
>>>> On 26/04/2015 02:01, Clément Pit--Claudel wrote:
>>>>> Hi David & list,
>>>>>
>>>>> David: Have you had time to look at my attempt to migrate to git? My 
>>>>> username on github is cpitclaudel.
>>>>>
>>>>> List: I had a quick look at options to migrate trac tickets to GitHub. 
>>>>> There seems to exist solutions, but nothing too robust. There hasn't been 
>>>>> loads of activity on trac in the last few years though, so I'm not sure 
>>>>> if such a migration is really needed. And (as opposed to CVS) there is no 
>>>>> need to retire Trac immediately after the migration.
>>>>>
>>>>> Clément.
>>>>>
>>>>> On 04/20/2015 03:49 PM, David Aspinall wrote:
>>>>>> Hello Clément, all,
>>>>>>
>>>>>> This is a very timely message!  I have indeed started to think of making 
>>>>>> this migration again.  Although I don't have a lot of time to work on 
>>>>>> it, I would like to see it done.  There is an old attempt here:
>>>>>>
>>>>>>  https://github.com/DavidAspinall/ProofGeneral
>>>>>>
>>>>>> but it didn't get updated and indeed we could do a better job with the 
>>>>>> user names.  I'll take a look at your attempt soon (which tool did you 
>>>>>> use?).
>>>>>>
>>>>>> I agree that we probably need to set a cut-off date and disconnect the 
>>>>>> old CVS repo, the sync options don't look robust.  What I could most do 
>>>>>> with help is converting the packaging/publishing tools to use the github 
>>>>>> repo.  (The web pages also badly need replacing but I'm not sure if 
>>>>>> anyone would have the stomach to do that?)
>>>>>>
>>>>>> I'm slightly wary of needing to manage merge requests so I thought of 
>>>>>> using a GitHub organisation for this to share the job and to host a 
>>>>>> central repo.  Hence:
>>>>>&

[PG-devel] Closing outdated tickets

[Clément Pit--Claudel]

Hi pg-devel,

What's the policy regarding closing tickets on the tracker? If I come across an 
outdated ticket, do I close it with an explanation message? Or do only 
committers close tickets?

Clément. 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Migrating Proof-General to Git

[Clément Pit--Claudel]

Hi David  list,

David: Have you had time to look at my attempt to migrate to git? My username 
on github is cpitclaudel.

List: I had a quick look at options to migrate trac tickets to GitHub. There 
seems to exist solutions, but nothing too robust. There hasn't been loads of 
activity on trac in the last few years though, so I'm not sure if such a 
migration is really needed. And (as opposed to CVS) there is no need to retire 
Trac immediately after the migration.

Clément.

On 04/20/2015 03:49 PM, David Aspinall wrote:
 Hello Clément, all,
 
 This is a very timely message!  I have indeed started to think of making this 
 migration again.  Although I don't have a lot of time to work on it, I would 
 like to see it done.  There is an old attempt here:
 
  https://github.com/DavidAspinall/ProofGeneral
 
 but it didn't get updated and indeed we could do a better job with the user 
 names.  I'll take a look at your attempt soon (which tool did you use?).
 
 I agree that we probably need to set a cut-off date and disconnect the old 
 CVS repo, the sync options don't look robust.  What I could most do with help 
 is converting the packaging/publishing tools to use the github repo.  (The 
 web pages also badly need replacing but I'm not sure if anyone would have the 
 stomach to do that?)
 
 I'm slightly wary of needing to manage merge requests so I thought of using a 
 GitHub organisation for this to share the job and to host a central repo.  
 Hence:
 
  https://github.com/ProofGeneral
 
 If anyone on this list would like to join, please tell me your GitHub user 
 name.
 
  - David
 
 On 20/04/2015 19:29, Clément Pit--Claudel wrote:
 Hi Pierre and David (and proofgeneral-devel),

 There were talks a while ago on the mailing list about a migration to git. I 
 think this would be really cool. I experimented with various export options, 
 and came up with the repo at https://github.com/cpitclaudel/proof-general/ . 
 The problem with the process that I used is that it makes it hard to 
 incrementally track changes (we would need to migrate once and for all).

 Most of the history seems to have been preserved just fine, but it would be 
 nice to map CVS usernames to proper names and emails; the authors in the CVS 
 tree seem to be [assia, crr, cxl, da, djs, fionam, gklein, hhg, joheras, 
 lego, makarius, mark, markus, monnier, patrl, pier, proofgen, pxc, sberghof, 
 tews, tms, weber]. Is there a list of names and emails somewhere matching 
 these usernames?

 It would be great to get feedback on the history as recorded in 
 https://github.com/cpitclaudel/proof-general/ ; also, if a migration was 
 eventually decided, I could help with the process. One reason for migrating 
 to Git and hosting on Github would be lowering the barrier of entry to new 
 contributors: many of the changes that I made in my company-coq plugin could 
 in fact be ported to proof-general. It could also allow for simplified 
 distribution of extensions and updated versions, via emacs' package system.

 Clément.

 
 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Migrating Proof-General to Git

[Clément Pit--Claudel]

One more advantage of moving to MELPA as our distribution system is that we can 
register mmm as a dependency, instead of packaging it ourselves.

On 04/20/2015 03:49 PM, David Aspinall wrote:
 Hello Clément, all,
 
 This is a very timely message!  I have indeed started to think of making this 
 migration again.  Although I don't have a lot of time to work on it, I would 
 like to see it done.  There is an old attempt here:
 
  https://github.com/DavidAspinall/ProofGeneral
 
 but it didn't get updated and indeed we could do a better job with the user 
 names.  I'll take a look at your attempt soon (which tool did you use?).
 
 I agree that we probably need to set a cut-off date and disconnect the old 
 CVS repo, the sync options don't look robust.  What I could most do with help 
 is converting the packaging/publishing tools to use the github repo.  (The 
 web pages also badly need replacing but I'm not sure if anyone would have the 
 stomach to do that?)
 
 I'm slightly wary of needing to manage merge requests so I thought of using a 
 GitHub organisation for this to share the job and to host a central repo.  
 Hence:
 
  https://github.com/ProofGeneral
 
 If anyone on this list would like to join, please tell me your GitHub user 
 name.
 
  - David
 
 On 20/04/2015 19:29, Clément Pit--Claudel wrote:
 Hi Pierre and David (and proofgeneral-devel),

 There were talks a while ago on the mailing list about a migration to git. I 
 think this would be really cool. I experimented with various export options, 
 and came up with the repo at https://github.com/cpitclaudel/proof-general/ . 
 The problem with the process that I used is that it makes it hard to 
 incrementally track changes (we would need to migrate once and for all).

 Most of the history seems to have been preserved just fine, but it would be 
 nice to map CVS usernames to proper names and emails; the authors in the CVS 
 tree seem to be [assia, crr, cxl, da, djs, fionam, gklein, hhg, joheras, 
 lego, makarius, mark, markus, monnier, patrl, pier, proofgen, pxc, sberghof, 
 tews, tms, weber]. Is there a list of names and emails somewhere matching 
 these usernames?

 It would be great to get feedback on the history as recorded in 
 https://github.com/cpitclaudel/proof-general/ ; also, if a migration was 
 eventually decided, I could help with the process. One reason for migrating 
 to Git and hosting on Github would be lowering the barrier of entry to new 
 contributors: many of the changes that I made in my company-coq plugin could 
 in fact be ported to proof-general. It could also allow for simplified 
 distribution of extensions and updated versions, via emacs' package system.

 Clément.

 
 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel