Python error on coq error

[sdemos]

If an error in a proof is introduced (such as a reflexivity where the subgoal can't be solved with it), the python wrapper spits back an error that says the following -

err: <value loc_e="11" loc_s="0" val="fail"><state_id val="359" />
Error: In environment
H : false &amp;&amp; false = true
Unable to unify "true" with "false".</value>
Error detected while processing function provider#python#Call:
line   18:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/demos/.genconfig/vim/bundle/coquille/autoload/coquille.py", line 113, in coq_to_cursor
    send_until_fail()
  File "/home/demos/.genconfig/vim/bundle/coquille/autoload/coquille.py", line 352, in send_until_fail
    refresh()
  File "/home/demos/.genconfig/vim/bundle/coquille/autoload/coquille.py", line 180, in refresh
    show_goal()
  File "/home/demos/.genconfig/vim/bundle/coquille/autoload/coquille.py", line 201, in show_goal
    if response.msg is not None:
AttributeError: 'Err' object has no attribute 'msg'

This is instead of printing this information in the third pane, like it did in previous versions.

Also, it was pretty stable up until I started trying to reproduce the error, and now it just makes vim hang when I try to get back to where I was, the same as #45. This happens in both neovim 0.1.7 and vim 8.0 using coq 8.5pl3.

[Deleted user]

bump

[alexeicolin]

Silly workaround without digging into it:

--- /home/acolin/.vim/bundle/coquille/autoload/coquille.py      2017-02-24 19:29:37.688292892 -0500
+++ /tmp/coquille.py    2017-02-24 19:29:14.128451735 -0500
@@ -198,7 +198,7 @@
         print('ERROR: the Coq process died')
         return
 
-    if response.msg is not None:
+    if hasattr(response, "msg") and response.msg is not None:
         info_msg = response.msg
 
     if response.val.val is None:

[dwarfmaster]

I am working on a fix here. There still are some issues, but it should fix the most of these errors. Would you mind testing it ?

[felixbauckholt]

@lucas8, I ran into the same error; I've been using your fix and I haven't noticed any issues so far.

Thanks a lot! Do you know how to speed up the acceptance of your pull request?

[dwarfmaster]

@felixbauckholt The best you can do is to comment my pull request, and hope @trefis will see it.

To prevent this kind of problems, I asked a Coq developer if there was any documentation for the protocol, and there isn't. Futhermore it seems to be mostly experimental and prone to change, so I guess we're stuck with having these problems for every new version.

[JaredCorduan]

Thank you @lucas8 for making that branch! I'm using it now and it is working great for me.

[williamsonrichard]

@lucas8: Which pull request were you referring to? I too would like to see this merged.

[dwarfmaster]

@williamsonrichard I was speaking of #55, which has already been merged. I just noticed I didn't included in the pull request my last two commits. I just made a pull request for that : #67