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
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?
coqtop does not speak XML, only coqidetop does. The options are accepted anyway, I'm afraid.
@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
if you happen to be using Python or can port to Python we also recommend PyCoq
@Karl Palmskog I have not considered alternatives, I will check those out, thank you!
@Enrico Tassi ah that explains it
Thomas Dziedzic has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC