Bug 2777 - Document ideslave (coqide) interchange format
: Document ideslave (coqide) interchange format
Status: NEW
Product: Coq
Classification: Unclassified
Component: Doc
: 8.4
: All All
: P5 enhancement
: ---
Assigned To: nobody
Depends on:
  Show dependency treegraph
Reported: 2012-05-11 05:50 CEST by Edward Z. Yang
Modified: 2012-10-26 23:55 CEST (History)
2 users (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
Description Edward Z. Yang 2012-05-11 05:50:59 CEST
This is related to Bug 2705; but possibly more so, given the comments of Makarius Wenzel.

coqtop -ideslave currently uses an XML exchange format that is not documented. It would be great if it were; this would allow for cross-language interop between Coq and other frontends, without requiring us to use the Ide_slave/Ide_intf modules and tie our frontend to Coq.

Downsides would be that if you wanted to make any sort of major refactoring it'd be easy to break external users; but I suppose anyone this closely in bed with Coq wouldn't mind keeping their software up to date.
Comment 1 Pierre-Marie Pédrot 2012-05-11 20:00:33 CEST
Yes, this should indeed be done. The interface is not that stable yet, so you should not expect to something totally done.

If you really have a urgent crave for discussing with Coqtop in XML, the trunk file lib/serialize.ml is quite self-explanatory.

Otherwise, I will try to do that quickly.