search

the-lambda-church / coquille

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

`:Coq Check nat.` hangs. #72

Open kindaro opened 6 years ago

kindaro commented 6 years ago

Hello.

I am new to Coq. My expectation is that :Coq Check nat. should write something along the lines of nat : Set to the Infos window. This is not the case: insofar as CoqLaunch was issued previously and, hence, there is a pair of coqtop processes attached to Vim, the following will be displayed, with Vim hanging:

[pid 1828] Unexpected XML message
[pid 1828] Expected XML node: pair
[pid 1828] XML tree received: <state_id val="1"/>

(Though with garbled indentation that I fixed manually for the purpose of clarity of presentation.)

Here 1828 is the process identifier of coqtop -ideslave -main-channel stdfds -async-proofs on.

If I resize terminal window, Vim will unstick, both coqtop processes will die, and the Goals and Infos buffers will get closed.

My operating system is ArchLinux.

Here is the version of Coq I use:

% coqtop --version
The Coq Proof Assistant, version 8.7.1 (December 2017)
compiled on Dec 16 2017 22:25:15 with OCaml 4.05.0

I have cloned coquille at commit df24600 which is the latest at the moment.

aferr commented 5 years ago

Is there a workaround for this? I have checked out the pathogen-bundle branches, not the master branch.