search

the-lambda-church / coquille

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

Fix python error message when using `Save.` or `Qed.` #52

Closed TWal closed 7 years ago

TWal commented 7 years ago

I had the following error message when going through a Save. or Qed.:

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/twal/.vim/bundle/coquille/autoload/coquille.py", line 129, in coq_next
    send_until_fail()
  File "/home/twal/.vim/bundle/coquille/autoload/coquille.py", line 354, in send_until_fail
    refresh()
  File "/home/twal/.vim/bundle/coquille/autoload/coquille.py", line 181, in refresh
    show_info()
  File "/home/twal/.vim/bundle/coquille/autoload/coquille.py", line 244, in show_info
    lst = info_msg.split('\n')
AttributeError: 'Option' object has no attribute 'split'

Indeed, info_msg was an Option(val=None) It came from coquille.py, line 202, in show_goal coqtop.py, line 269, in goals coqtop.py, line 197, in call coqtop.py, line 185, in get_answer coqtop.py, line 57, in parse_value

Since this line of parse_value returns Option(val=None), the fix is to add a .val in the line 185 of get_answer

Here is my coqtop --version, if it is useful:

The Coq Proof Assistant, version 8.6 (February 2017)
compiled on Feb 22 2017 19:37:17 with OCaml 4.04.0

It comes from the repositories of Archlinux