Skip to content

:Coq Check nat. hangs. #72

@kindaro

Description

@kindaro

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions