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
> 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,
Stefan
>From 1cd25fa20ccac27835b1609cfc089615aade2575 Mon Sep 17 00:00:00 2001
From: Stefan Monnier
Date: Tue, 11 Dec 2018 18:48:51
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
> Find below a first patch.
Is there something else I need to do for this patch to be installed, or
should I just wait a bit more (I have other patches in the pipeline
after this one).
Stefan
> 2018-11-28 Stefan Monnier
>
> Move `defvar`s used to silence warnings outside of eval
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
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 ca
Clément Pit-Claudel writes:
> 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?
I will mention three that already
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?
Clément Pit-Claudel writes:
> 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?
Do you mean th
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
Hi Pierre,
Pierre Courtieu writes:
> Of cours evolution is equally important. Please correct "stable" by
> "backward compatible". The changes should not make valid commands
> become invalid, or at least before having it tagged "obsolete" for
> several years. Actually coq has a very good policy a
Le lun. 3 déc. 2018 à 13:11, Emilio Jesús Gallego Arias a écrit
:
>
> I feel like this may be the moment to make it a bit more "stable".
Good news!
> However, I would expect adding PG support to SerAPI to require at least
> one or two Coq releases where it would be marked "experimental" and th
Pierre Courtieu writes:
> I took a quick look at serapi's github. It looks very nice but is
> serapi still in "alpha" and "subject to change"?
I feel like this may be the moment to make it a bit more "stable".
However, I would expect adding PG support to SerAPI to require at least
one or two Co
I took a quick look at serapi's github. It looks very nice but is
serapi still in "alpha" and "subject to change"?
This is important. I don't want to switch to a protocol that will not
be backward compatible for a long time. By long time I mean >= 10
years.
Consider that coq old REPL stayed stabl
Pierre Courtieu writes:
> Does serapi avoids being based on a notion of document model? Last I
> checked about stm it was based on an implicit DAG roughly representing the
> lemmas of the file. Don't we need something like that to use serapi
> correctly?
It aims to have a simpler notion of docum
Le dim. 2 déc. 2018 à 02:50, Emilio Jesús Gallego Arias a
écrit :
> Pierre Courtieu writes:
>
> > I think the most important is that your documentation should contain or
> > point to a documentation of coq stm.
>
> Why? I'd rather document SerAPI by itself, why to expose the low-level
> document
Pierre Courtieu writes:
> I agree. One more argument: opam has problems and having Coq delivered only
> by opam is risky these days. So having a reliable fallback is good. Even if
> it is a bit outdated.
The main problem is that Coq 8.6 is unsupported upstream, and it seems
de-facto orphaned in
Pierre Courtieu writes:
> I think the most important is that your documentation should contain or
> point to a documentation of coq stm.
Why? I'd rather document SerAPI by itself, why to expose the low-level
document manager?
Note that the README is not accurate anymore, as SerAPI is not tied t
I think the most important is that your documentation should contain or
point to a documentation of coq stm.
Cheers
Pierre
Le sam. 1 déc. 2018 à 01:46, Emilio Jesús Gallego Arias a
écrit :
> Pierre Courtieu writes:
>
> > I am all for it, where can I find the serapi documentation please?
>
> Th
I agree. One more argument: opam has problems and having Coq delivered only
by opam is risky these days. So having a reliable fallback is good. Even if
it is a bit outdated.
P
Le sam. 1 déc. 2018 à 03:53, Stefan Monnier a
écrit :
> > Now that you have mentioned it, we consider this pretty unopti
> Now that you have mentioned it, we consider this pretty unoptimal and we
> agreed on removing Coq from Debian due to the perils of shipping an
> outdated version :( :(
I find it perfectly adequate for my needs, FWIW.
And I'd be annoyed to have to install Coq manually.
2 years old sounds like a r
Stefan Monnier writes:
> FWIW, Debian stable has Coq-8.6 (which is only about 2 years old),
> so that's what I use on some of my machines.
Now that you have mentioned it, we consider this pretty unoptimal and we
agreed on removing Coq from Debian due to the perils of shipping an
outdated version
Pierre Courtieu writes:
> I am all for it, where can I find the serapi documentation please?
That's a good point, the documentation is fairly sketchy as we didn't
see the need to make the API stable yet.
In fact one of the problems Paul has pointed out was lack of
specification of the XML proto
> I guess at some point it would make sense to tie PG to an specific Coq
> range; I think the required changes could be made in the range of Coq >=
> 8.8.
FWIW, Debian stable has Coq-8.6 (which is only about 2 years old),
so that's what I use on some of my machines.
Stefan
__
I am all for it, where can I find the serapi documentation please?
Cheers,
Le ven. 30 nov. 2018 à 03:15, Emilio Jesús Gallego Arias a écrit
:
>
> [ccing Maxime as he is working on the core Coq document platform these days]
>
> Clément Pit-Claudel writes:
>
> > This. At least from my short expe
[ccing Maxime as he is working on the core Coq document platform these days]
Clément Pit-Claudel writes:
> This. At least from my short experience, the protocol offered by
> SerAPI (well, the one that was offered a year ago ^^ I don't know if
> it changed) is much more robust than the XML-based
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
"Paul A. Steckler" writes:
>> > That helps a bit for some issues, but I think most of the bugs in the
>> > async branch mostly relate to maintaining unstated or unknown
>> > invariants in the implementation.
>>
>> Umm, I'm not sure I share that view, I'd dare to say that for a start the
>> new pr
> > That helps a bit for some issues, but I think most of the bugs in the
> > async branch mostly relate to maintaining unstated or unknown
> > invariants in the implementation.
>
> Umm, I'm not sure I share that view, I'd dare to say that for a start the
> new protocol would allow to drop 90% of t
"Paul A. Steckler" writes:
> That helps a bit for some issues, but I think most of the bugs in the
> async branch mostly relate to maintaining unstated or unknown
> invariants in the implementation.
Umm, I'm not sure I share that view, I'd dare to say that for a start the
new protocol would allo
Clément Pit-Claudel writes:
> Ah, yes, of course; but removing that code requires dropping support
> for old versions of Coq.
I guess at some point it would make sense to tie PG to an specific Coq
range; I think the required changes could be made in the range of Coq >=
8.8.
Of course it would d
On Thu, Nov 29, 2018 at 11:16 AM Emilio Jesús Gallego Arias
wrote:
> As of today, you have coq-serapi[1], which was specifically designed to
> make interaction with Emacs easy.
That helps a bit for some issues, but I think most of the bugs in the
async branch mostly relate to maintaining
unstate
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
Stefan Monnier writes:
>> In my opinion, it seems very likely that the branch will never reach a
>> working state; mainly because it would be hard to justify putting time
>> to fix it when you have other alternatives that allow a much lightweight
>> and robust implementation.
>
> I'm not up to sp
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
Am
> In my opinion, it seems very likely that the branch will never reach a
> working state; mainly because it would be hard to justify putting time
> to fix it when you have other alternatives that allow a much lightweight
> and robust implementation.
I'm not up to speed on those alternatives. What
On Thu, Nov 29, 2018 at 9:35 AM Emilio Jesús Gallego Arias wrote:
> In my opinion, it seems very likely that the branch will never reach a
> working state; mainly because it would be hard to justify putting time
> to fix it when you have other alternatives that allow a much lightweight
> and robus
On 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 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
_
Pierre Courtieu writes:
> I am very worried about the async branch. Its state is not usable at
> this moment (lots of bugs) imho and we have nobody to maintain and fix
> it currently.
In my opinion, it seems very likely that the branch will never reach a
working state; mainly because it would be
Hi Pierre,
Le jeudi 29 novembre 2018 à 17:48 +0100, Pierre Courtieu a écrit :
> Is a student having a 6 year old linux distrib really worth worrying?
> (just kidding).
For Ubuntu 14.04 I guess you just mean 4 years old (or 4.5)… as we’re
still in 2018 ;)
Actually what might be interesting when d
Le jeu. 29 nov. 2018 à 12:12, Erik Martin-Dorel
a écrit :
>
> Hi Pierre,
>
> Le jeudi 29 novembre 2018 à 10:35 +0100, Pierre Courtieu a écrit :
> > Do we really want to be compatible with ubuntu 14.04? I mean there are
> > 18.04 and now 20.04 out there...
>
> Indeed it may seem quite an old releas
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
Hi Pierre,
Le jeudi 29 novembre 2018 à 10:35 +0100, Pierre Courtieu a écrit :
> Do we really want to be compatible with ubuntu 14.04? I mean there are
> 18.04 and now 20.04 out there...
Indeed it may seem quite an old release… but the EOL of Ubuntu 14.04
will just take place in April 2019 (and I’
Thanks a lot Stefan,
I am very worried about the async branch. Its state is not usable at
this moment (lots of bugs) imho and we have nobody to maintain and fix
it currently.
Do we really want to be compatible with ubuntu 14.04? I mean there are
18.04 and now 20.04 out there...
P.
Le jeu. 29 nov.
> Yes, exactly. `master` is still the mainline branch to integrate new PRs
> while the nextgen implementation available in `async` is still in alpha phase.
OK, good.
> We'd specifically want to keep support of Emacs 24.3 for the moment
> because this is still the version of the emacs24 package di
I'm consider sending patches that change the code to take advantage of
features from newer Emacsen (such as lexical-binding) but am wondering
what's the "target" supported version.
In the `master` branch (PG-4.5), it is claimed that it should work under
Emacs-24.3 whereas in the `async` branch (PG
47 matches
Mail list logo
