Coq responds "Incorrect query"
Closed this issue · 10 comments
Trying to process any command, Coq responds: "Incorrect query". I have Coq 8.4pl13 on Linux.
This sounds bad .. apparently there are some protocol changes and this means my favorite Coq Vim plugin(http://www.vim.org/scripts/script.php?script_id=4388) will also be broken once I update my Coq installation ...
Yes there indeed have been some protocol changes.
I haven't had time to update coquille to this new protocol yet though, I'll try to see what I can do in the next few weeks.
I'll keep you posted.
I think it's time for me to finally learn vimscript and help plugin development ... :)
No vimscript required here, just a bit of python and knowledge of the
protocol (=> xml).
Your help is of course very welcomed :)
Is there a quick reference for the protocol? I'd be happy to contribute some time :)
There is a simple fix for CoqIDE: https://github.com/tauli/CoqIDE/commit/2e5578c8078c7aa60aee491d037cc6eed1ab3a8c
Perhaps the fix for Coquille is easy as well?
@anderslundstedt thanks for fixing CoqIDE! I'll use your changes once I update my Coq setup ...
See this thread https://sympa.inria.fr/sympa/arc/coqdev/2013-11/msg00051.html for the changes in the protocol, the last message of Enrico address these specifically ; @elliottt it also mentions coqtop --help-XML-protocol which might interest you (it's been introduced recently I believe, I didn't know about it before this mail at least).
I'll try and update coquille soon, it should be done before the end of next week. Sorry for the latency.
@osa1 it was not my fix, I merely discovered the pull request. Also I would advise you to not upgrade Coq yet, since there seems to be problems remaining. For example, I discovered that the following produces a lemma that is not available: http://pastebin.com/4vKk1pa9
Ok so, quick update : I tried to work on this. But I only have an "old" version of coq on my system, and --help-XML-protocol seems to exist only on trunk which I failed to compile.
I'll try again sometime soon (I'll start using Coq regularly again in april, so Coquille is gonna be more lively soon!).