search

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

Coq-HoTT #21

Open tbelaire opened 10 years ago

tbelaire commented 10 years ago

Sorry, this is a bit of a brain dump.

Hi, the plugin is hanging when I try and use it with the coq from HoTT. I'm working hard to debug it myself, but was wondering if you had tried to tackle that yourself? Do you know how to debug these kind of issues?

Once I changed it to hoqtop instead of coqtop, it was crashing. There's a few places where it sends var="info" instead of "good" or "bad", but I fixed those, along with <message> <message_level val="info" /> <string> Warning...</string></message> responses. But coqtop sends those too.

I'm passing the -debug flag to coqtop, and redirecting stderr to a tmp file, but it seems like coqtop is not crashing, and thinks it sent a message to vim.

If I take a closer look at what happens when I send Check 4. to coqtop or hoqtop, I get this reply:

<message><message_level val="warning"/><string>Query commands should not be inserted in scripts</string></message>
<message><message_level val="notice"/><string>4
     : nat</string></message><value val="good"><string></string></value>

That's more that one root node.

Oh, hey, if I set the number of bytes read each time to 1, it fixes the hangs. It might be running into problems with more than one root node sneaking in, like the string <node>1</node><node>2</node>, which'll cause a parse error forever. It's still running into some problems parsing the goals, and I'm not sure why, since the response I'm retrieving in python/vim is different from the one it's sending?! At least according to the bit of extra debugging code in compiled into hoqtop. So, I guess there's a extra call to flush or something in coqtop, which is preventing the pairs of nodes to sneak by in one system call to write.

Have there been any reports of infinite loop hangs for regular coqtop?

tbelaire commented 10 years ago

Ha, I got it https://github.com/tbelaire/coquille/tree/hoqtop

I'll clean up all the debugging stuff soon, but what was happening was more than one message was getting sent at once to vim. Now I loop over all the messages each time I get it.

Also, sorry about the colour change in that commit, but it's unreadable otherwise. Maybe that should be a variable I can set in the vimrc. Same with the coqtop name.