Error detected wile processing function provider#python#Call

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.

ISC License

186 stars 68 forks source link

Error detected wile processing function provider#python#Call #50

Open adityavkk opened 7 years ago

adityavkk commented 7 years ago

line18 in coquille.py

AttributeError: 'Option' object has no attribute 'split'

vuongDang commented 7 years ago

Hey! Same error but line 242: coquille.py

lst = info_msg.split('\n')
AttributeError: 'Option' object has no attribute 'split'

rbowden91 commented 7 years ago

The issue seems to be that "info_msg" might not just be None, but might be Option(val=None), which is something that coqtop.py constructs. Not sure how all this comes together, but my fix was changing the condition on line 241 of coquille.py to:

if info_msg is not None and (not isinstance(info_msg, CT.Option) or info_msg.val is not None):

vuongDang commented 7 years ago

Actually it was my bad, I'm using coq 8.6 which is not currently supported by coquille. After looking into the issue it seems the API of coqtop has been modified quite a bit. Does anyone know where I can find some documentation about it? I've seen nothing on the offical website and neither in the coq project doc.