Comply with coq8.5 #43
Conversation
swr1bm86
force-pushed
the
comply-with-coq8.5
branch
2 times, most recently
from
31c10a7 to
3bd21cb
Compare
swr1bm86
force-pushed
the
comply-with-coq8.5
branch
from
3bd21cb to
9946591
Compare
| .spyderproject | ||
|
|
||
| # Rope project settings | ||
| .ropeproject |
There was a problem hiding this comment.
I don't think you meant to commit this file.
At least not with this content.
There was a problem hiding this comment.
now only ignore the byte-compiled files.
| def ignore_sigint(): | ||
| signal.signal(signal.SIGINT, signal.SIG_IGN) | ||
|
|
||
| def escape(cmd): |
There was a problem hiding this comment.
Is that really useful necessary for a vim plugin?
There was a problem hiding this comment.
@trefis i think it is nothing to do with vim. 😅 we can not happily parse xml data using xml.etree.ElementTree without escaping these special chars.
| print "goals =>", gs | ||
| return r | ||
|
|
||
| if __name__ == '__main__': |
There was a problem hiding this comment.
The following lines look like testing. I don't think you meant to commit them.
There was a problem hiding this comment.
@trefis yes, exactly, they just some tests. 😅 so how about putting them into tests and then checking them using travis in this PR?
| @@ -2,7 +2,7 @@ let s:coq_running=0 | |||
| let s:current_dir=expand("<sfile>:p:h") | |||
|
|
|||
| if !exists('coquille_auto_move') | |||
| let g:coquille_auto_move="false" | |||
| let g:coquille_auto_move="true" | |||
There was a problem hiding this comment.
Please don't change things like this. Or at least propose them in another PR so they can be discussed independently.
There was a problem hiding this comment.
fair enought, i'll do that 😅
|
(Sorry for the delay btw) |
|
@trefis no worries, i'll take care of your comments first :)
|
swr1bm86
force-pushed
the
comply-with-coq8.5
branch
from
6890545 to
e6cdcb6
Compare
|
@trefis please review again :) |
| while True: | ||
| try: | ||
| data = os.read(fd, 0x4000) | ||
| acc += data |
There was a problem hiding this comment.
This accumulator doesn't seem to be used.
There was a problem hiding this comment.
Yeah, exactly, I'll remove it, THX!
There was a problem hiding this comment.
Isn't it possible that there is a longer input from coqtop (or, for example, the full output is not generated in time) ? I am not familiar with its behavior, but upon executing some local code, the execution of the plugin freezes here.
|
@trefis Bump, please! |
|
+1 |
|
I'll check out if it also works well on Coq8.6 which is released recently this weekend. |
|
Thanks @zjhmale, that would be fantastic. As a heads up - not sure the patch is exactly working with 8.5. I'm working through a learning text right now (Certified Programs Dependent Types) and it's throwing a different error now with a basic example ( After loading a
|
|
@civiclabsconsulting I'll check out that 😄 |
|
I finally tested this with 8.5 and it "works" (i.e. it seems to work, at least it's much better than not having anything). Some commits (like cleaning the "info" window before doing anything) did not seem so great to me, but I kept them anyway. Thanks a lot for the contribution! |
|
Btw, I just encountered the same kind of bug as @civiclabsconsulting (i.e. errors not being displayed properly, but a python backtrace being displayed in vim). |
Fixes #31 and #42.
now we can kindly play with Coq8.5 :)
@trefis please review.