> 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
> 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
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
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
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/ejgallego/coq-serapi I see:
(Query ((sid 3) (pp
> 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
