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 t
ttps://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 whi
ve 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 th
re 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
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
___
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émen
ut
> 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:
>> H
b 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 :
>
gt;> 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 GM
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 f
e 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.
>
>
lly).
> 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 wrot
May 5, 2016 at 4:34 PM, Clément Pit--Claudel
> 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
hink 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
>
> 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
> wrote:
>>
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
__
t;>>>>
>>>>> On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu
>>>>> wrote:
>>>>>>
>>>>>> I am sorry to say that I already asked myself about everything you
>>>>>> asked here, and, despite you suggest more smart ans
Additionally, it would be nice to remain compatible with plugins :)
On 2016-05-07 09:33, Clément Pit--Claudel wrote:
> 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:
On 2016-05-07 13:44, Paul A. Steckler wrote:
> Well, we're asking Proof General to work in a fundamentally
> different way than it has so far. Adding support for the XML mode
> significantly increases the complexity of the software, and that mode
> would not be used by other provers. Imagine that w
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 th
On 2016-05-07 14:37, Paul A. Steckler wrote:
> On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel
> wrote:
>> I'm all for a cleanup of the PG codebase, of course. But I think we can do
>> it slightly differently: starting with the current code, we can:
>>
>&
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 c
I think you just want two (well four, with the control channel)
`make-network-process'es, actually :)
You can `cl-define-struct' a pair of network process (and possibly wrap
relevant function to work on pairs of half-channels) for convenience, too.
Interestingly, you probably don't need a filte
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:
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
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.
>
>
n 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.
> O
On 2016-06-11 15:29, Paul A. Steckler wrote:
> On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel
> wrote:
>> My proposal was to dump the entire proof-shell part, indeed. I
>> agree with you that it would make everything much easier, and I
>> think that would be
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-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 ana
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 rem
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 t
On 2016-06-15 19:10, Makarius wrote:
> Yes, that is by Carst Tankink -- I was working with him over 6 months,
> before I left France. Later the Coqoon guys also joined the move,
> because I encouraged them to do that, but it never became first-class
> for Coq.
Well, it was demoed to an audience of
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 mon
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,
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
air of locked
> spans, or just one of them.
Yup, absolutely.
>
> On Sat, Jul 9, 2016 at 2:30 AM, Clément Pit--Claudel
> wrote:
>> On 2016-07-08 19:06, Paul A. Steckler wrote:
>>> So when you edit in a buffer, you send an StmCancel messages, you
>>&g
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 standalo
On 2016-08-08 11:31, Paul A. Steckler wrote:
> I've made some fair headway in getting Proof General working with the
> coqtop XMLish protocol. So now I'm working on some of the less-central
> bits for that port.
>
> There's a PG button, State, which in the REPL version of PG, sends
> "Show." to c
Very nice!
On 2016-11-16 06:06, Hendrik Tews wrote:
> Hi,
>
> I opend a PR for comments with a first version of -quick support,
> see the quick branch on g...@github.com:hendriktews/PG.git. The
> solution has advantages over using make because the quick options
> accept an up-to-date .vo file for
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 info
On 01/06/2017 05:45 PM, Ralf Jung wrote:
> I only today learned about "make -k" from your changes, that will be
> very useful indeed and may already be enough -- it will tell me which
> other files need fixing.
Yesh, that's what I was going to suggest from your post :) It's the default if
you run
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 an
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
l A. Steckler
> wrote:
>> On Fri, Feb 24, 2017 at 11:12 AM, Clément Pit--Claudel
>> 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
>>>
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
> ass
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.i
On 29/11/2018 12.20, Erik Martin-Dorel wrote:
> But AFAIK this info is not provided by the MELPA repository.
It could be, at least partly: a while ago I submitted a patch to Emacs that
makes it send its version number to MELPA.
signature.asc
Description: OpenPGP digital signature
_
On 29/11/2018 12.32, Emilio Jesús Gallego Arias wrote:
> 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
signature.asc
Description: OpenPGP digital signature
___
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
>
>
On 29/11/2018 14.52, Emilio Jesús Gallego Arias wrote:
> Note that SerAPI does indeed try to workaround a few quirks of the STM
> so clients don't have to care; and it can do so with moderate success
> as it lives in the OCaml work.
This. At least from my short experience, the protocol offered by
> This said, I don't see any hand parsing or pre/post processing tricks
> when reading SerAPI's sexps: I only see the prin1-to-sexp hack which
> works around the nil-vs-() difference. So maybe the syntax is closer to
> that of Elisp than shown in the README.md.
Indeed; in practice it works OK.
Th
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 c
On 03/12/2018 10.33, Emilio Jesús Gallego Arias wrote:
> I do believe users are much better served by the second approach. Let's
> face it, Isabelle IDE is years ahead of Coq on terms of features, the
> coupling approach was a key point.
Is it?
> I won't commit to an unachievable / unrealistic po
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?
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 co
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: OpenP
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
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.
Pus
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
err
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
Master branche please :)
On December 18, 2018 5:32:58 PM EST, Pierre Courtieu
wrote:
> Your "I think it is ok" is enough for me :-)
> P.
>
> Le mar. 18 déc. 2018 à 20:19, Stefan Monnier
> a écrit :
> >
> > > Cool! Should we think about putting this in a dev branch or do you
> > > feel confiden
On 2019-04-29 19:50, Emilio Jesús Gallego Arias wrote:
> - updates are in the form of diffs sent to the server,
Hi Emilio,
Can you say more about this part? Is the UI expected to compute diffs between
two updates, or can it just send the whole document and leave update
computation to SerAPI?
O
On 2019-04-30 12:00, Emilio Jesús Gallego Arias wrote:
> [Barring the problem that Coq itself has terrible internal support for
> completion as of today]
That's indeed a problem. In F* we used a fancy trie structure that gets
updated every time an identifier is added to the context, and rolled
On 2019-04-30 13:34, Emilio Jesús Gallego Arias wrote:
> Clément Pit-Claudel writes:
>
>> That's indeed a problem. In F* we used a fancy trie structure that
>> gets updated every time an identifier is added to the context, and
>> rolled back when reverting a segmen
On 2019-04-30 17:28, Emilio Jesús Gallego Arias wrote:
> I guess that for Coq we will try to allow to plug custom indexers to the
> namespace operations so they can use their indexing method of choice.
Yup, that's roughly how it works in F*-land: the IDE backend plugs in two
functions, and popula
66 matches
Mail list logo
