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
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
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.
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:
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:
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
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
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
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
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
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
>
ul 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 sinc
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
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
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
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
gt; 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
>>&g
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
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,
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
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
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
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
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
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
>
e 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,
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 welde
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
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
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
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 c
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
gt;>>>> 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
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
> 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&g
uld 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.
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
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 i
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
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
lease 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--Cl
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
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
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
44 matches
Mail list logo
