Newly-merged support for 8.5 often hangs - Githubissues

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.

ISC License

186 stars 68 forks source link

Newly-merged support for 8.5 often hangs #45

Closed pqwy closed 7 years ago

pqwy commented 7 years ago

Broadly, coquille causes vim to hang near the middle or towards the end of files in Software Foundations.

Repro:

Unpack the sources.
coqc Basics.v
vim Induction.v
Go to line 475 (beginning of plus_assoc'', the last theorem in the file).
:CoqToCursor; should run Coq over everything up to the theorem.
:CoqNext. At this point vim gets stuck.

Using Coq 8.5pl3 on OCaml 4.03.0. Happens both with vim (8.0) and neovim (0.1.7).

I'll see if I can dig out more details, but this repro seems reliable.

trefis commented 7 years ago

I fixed the hanging problem. But I think, though I might be wrong, that the current implementation of the protocol is broken in the sense that it doesn't seem to handle at all the asynchronous messages from Coq. i.e. it might be marking proof as checked while they haven't been processed by Coq yet, and then will ignore the messages confirming whether the proof is correct or not.

This is just speculation, I haven't read the code carefuly.