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:
> 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:
> 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
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
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
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
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
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
> 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
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
> 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
"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
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:
>
> -
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
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
> 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.
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
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
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
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
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
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
> 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
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
25 matches
Mail list logo
