Clément Pit-Claudel writes:
> Yup, that's roughly how it works in F*-land: the IDE backend plugs in
> two functions, and populates its own view of the completion
> candidates.
Ah cool! I'll have a look again for sure to see how the API is; I recall
looking at the trie itself, but not at the plug
Clément Pit-Claudel writes:
> The completion data structures in F* allow for prefix matching across
> each '.' in the qualified name, so Aaa.Bbb.Ccc can be found using
> A.B.Cc or B.Ccc or C.
Thanks Clément; I think that Coq's Nametab can do this kind of stuff
already, I didn't look too closely
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 segment. Maybe that would work for Coq
> too?
You told me about this but I forgot, what kind of m
Emilio Jesús Gallego Arias writes:
> We may experiment with speculative checking in the future, but with the
> current architecture it will likely be too heavy.
>
> The design allows for it
To be more concrete: "the current design does allow for speculative
checking if the u
Clément Pit-Claudel writes:
> 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?
Indeed you can send the whole document if you want; diffs are an
optimization. Here we follo
Hi folks,
I thought I'd give an update on what has been going on w.r.t. SerAPI and
its successor.
First, we added a bit of documentation, it is not a wonder, and
moreover, it will change, but here it is:
http://ejgallego.github.io/coq-serapi/priv-serapi/Serapi_protocol/
The main change is that S
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
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 wi
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 poin
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
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
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
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
> This little detail will likely end up forcing the Elisp side to either
> re-implement a sexp-reader by hand (in Elisp, which will be slowish),
> or require ugly hacks to try and pre-process the answer before passing
> it to the sexp reader (or post-process the sexp), which will likely
> always
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
Hi Stefan!
Stefan Monnier writes:
> Looking at SerAPI, I'm wondering about the choice of "sexp". I know it
> may sound odd to want something else than sexps when working in Elisp,
> but in reality sexps only work well if they use *exactly* the same
> syntax. E.g. in https://github.com/ejgalleg
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
[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
"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
"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
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
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 Jim,
"Jim Fehrle" writes:
> 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?
Sorry for the late reply, let me add a few brief comments.
Much in the line of what Pierre said, i
26 matches
Mail list logo
