Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Organization of Coq enhancement requests from UI developers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Organization of Coq enhancement requests from UI developers


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Organization of Coq enhancement requests from UI developers
  • Date: Sat, 30 Jan 2016 11:56:13 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
  • Ironport-phdr: 9a23:eGoodh3Hfl8KHOWesmDT+DRfVm0co7zxezQtwd8ZsegVLfad9pjvdHbS+e9qxAeQG96LtLQc26GP4+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZznnLnis7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCaJ/HoXVS0qmwFTAkCR4RfgX5z29DfzrfF88CicJ8z/C74uD2fxp5x3QQPl3X9UfwUy93va35R9
On Fri, Jan 29, 2016 at 07:08:40PM -0500, CJ Bell wrote:
> Speaking of the CoqIDE XML protocol, I've partially documented it here:
> https://github.com/siegebell/vscoq/blob/master/CoqProtocol.md

Very nice. A simple remark: your description mixes the encoding of
remote function calls with the encoding of their payloads. It may help
to separate the two things. You may also want to link

https://github.com/coq/coq/blob/trunk/ide/interface.mli#L222

For the records, there is also a related document by Emilio. It focuses
on the API the XML protocol is based upon, it is somewhat complementary.

https://github.com/ejgallego/jscoq/blob/master/notes/coq-notes.md

Best,
--
Enrico Tassi

Archive powered by MHonArc 2.6.18.

Top of Page