Stream: Coq users

Topic: ✔ coqtop xml protocol example

Thomas Dziedzic (Jan 22 2022 at 13:56):

Hey all, I'm trying to develop a system that communicates with coqtop over the xml protocol and I can't seem to get a simple example working. I have the following ruby file which sets up a read and a write channel that listens on local ports: test.rb (run this with ruby test.rb) and after I start coqtop with the following command coqtop -main-channel 127.0.0.1:2000:2001 -async-proofs on I see the following on my server:

connected on main channel read
connected on main channel write
writing <call val="Init"><option val="none"/></call>
44

Note the 44 is the number of bytes it wrote over the write channel, but it seems like I don't receive anything over the read channel. It's been hard trying to find examples of how to write an xml client for coqtop on the internet so hoping someone here could provide some insight into what I could try. Also if you don't want to touch ruby but you have a simple coqtop client example, I could also work with that instead.

I'm also using coq 8.15.0

Thomas Dziedzic (Jan 22 2022 at 14:59):

ok, so I managed to get it to work using coqidetop.opt -main-channel 127.0.0.1:2000:2001 -async-proofs on I guess I don't know why coqtop doesn't work but coqidetop.opt does work, any ideas?

Enrico Tassi (Jan 22 2022 at 15:50):

coqtop does not speak XML, only coqidetop does. The options are accepted anyway, I'm afraid.

Karl Palmskog (Jan 22 2022 at 15:53):

@Thomas Dziedzic have you considered using an alternative to XML such as sexps or JSON via SerAPI to communicate with Coq? I believe the XML protocol is considered a legacy component of Coq at this point

Karl Palmskog (Jan 22 2022 at 15:59):

if you happen to be using Python or can port to Python we also recommend PyCoq

Thomas Dziedzic (Jan 22 2022 at 17:13):

@Karl Palmskog I have not considered alternatives, I will check those out, thank you!

Thomas Dziedzic (Jan 22 2022 at 17:13):

@Enrico Tassi ah that explains it

Notification Bot (Jan 23 2022 at 13:31):

Thomas Dziedzic has marked this topic as resolved.

Last updated: Sep 30 2023 at 07:01 UTC