the-lambda-church / coquille Goto Github PK

The plugin doesnt work anymore in coq 8.5, is there intention to work on this?

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.

Some very useful commands like "Set Printing All" cannot be written in a script when coqtop is called in ideslave mode. The error message says "Use CoqIDE display menu instead", however Coquille doesn't provide such a menu. It would be nice to have a way to access these commands. I tried ":Coq Set Printing All." but it seems to have no effect.

When a comment is followed by a bullet, any tactic following the bullet seems to be ignored. After processing the following script:

Goal True.
(* foo *)
+ exact I.

the goal is not solved.

It would be nice if CoqToCursor could encapsulate the functionality of CoqToCursor and CoqUndoToCursor. Is there a way to have it decide if the definitions under the cursor are already loaded?

While sending chunks to coqtop, vim thread is frozen because pipe reads are blocking. They should probably be made non-blocking instead, in particular when a script takes a vast amount of time to be processed, that would allow the user to further edit the file without having to wait.

I'm getting the following when executing the simple command :Coq Check (and True False):

Error detected while processing function coquille#RawQuery:
line    1:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/Users/jeffwu/Dropbox/dotfiles/vim/bundle/coquille/autoload/coquille.py", line 192, in coq_raw_query
    send_cmd(xml, encoding)
  File "/Users/jeffwu/Dropbox/dotfiles/vim/bundle/coquille/autoload/coquille.py", line 407, in send_cmd
    coqtop.stdin.write(serialized)
IOError: [Errno 32] Broken pipe

I thought it was because i was using coq 8.5 (seeing the other issue), but after uninstalling and re-installing, it still happens.

# coqtop --version                                                                                                                                                [12:35:16 AM]
The Coq Proof Assistant, version 8.3pl5 (March 2015)
compiled on Mar 24 2015 12:04:04 with OCaml 3.12.1

In the spirit of merlin, and other interactive theorem provers, it would be nice to map \leader<letter> to some useful commands. For instance, when the cursor is on a symbol, \leader p could call :Coq Print <symbol> to print the value, and \leader t could call :Coq Check <symbol>.

A shortcut for SearchAbout would be awesome, too. And syntax coloring in Infos/Goals windows!

It seems that the boundaries of commands are not correctly detected when there are non ascii symbols in them. Here is a minimal non-working example:

Require Import Utf8.

Check nat → nat.

Coq — through coquille — answers: “Syntax error: '.' expected after [vernac:check_command](in [proof_mode:subgoal_command]).” whereas coqc says: “nat → nat : Set”

Minimal example:

Theorem plus_swap : forall n m p : nat, 
  n + (m + p) = m + (n + p). 
Proof. 
  Admitted.

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

Silly workaround without digging into it:

--- autoload/coquille.py        2017-02-24 19:18:16.172890241 -0500
+++ /tmp/coquille.py    2017-02-24 19:22:42.111095494 -0500
@@ -239,7 +239,7 @@
 
     del buff[:]
     if info_msg is not None:
-        lst = info_msg.split('\n')
+        lst = str(info_msg).split('\n')
         buff.append(map(lambda s: s.encode('utf-8'), lst))
 
 def clear_info():

I'm getting this error:

"Logic.v" 346L, 7797C
Error detected while processing /home/omer/rcbackup/.vim/bundle/coquille/autoload/coquille.vim:
line    5:
E117: Unknown function: vimbufsync#init
line   10:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/omer/rcbackup/.vim/bundle/coquille/autoload/coquille.py", line 11, in <module>
    import vimbufsync
ImportError: No module named vimbufsync

I googled for that module but couldn't find anything.

line18 in coquille.py

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

Hey,
I get the following error when I try to open vim with coquille in my .vim/bundle.
I don't immediately know what's wrong with it. Could someone help me?

Traceback (most recent call last): File "<string>", line 1, in <module> File "~/.vim/bundle/coquille/autoload/coquille.py", line 5, in <module> import coqtop as CT File "~/.vim/bundle/coquille/autoload/coqtop.py", line 3, in <module> import subprocess File "/usr/local/Cellar/python@2/2.7.15_2/Frameworks/Python.framework/Versions/2.7/lib/python2.7/subprocess.py", line 72, in <module> import select ImportError: dlopen(/usr/local/Cellar/python@2/2.7.15_2/Frameworks/Python.framework/Versions/2.7/lib/python2.7/lib-dynload/select.so, 0x0002): code signature in (/usr/local/Cellar/python@2/2.7.15_2/Framew orks/Python.framework/Versions/2.7/lib/python2.7/lib-dynload/select.so) not valid for use in process: mapped file has no cdhash, completely unsigned? Code has to be at least ad-hoc signed

On my laptop, when coquille is waiting for coqtop to process several lines, the SentToCoq zone cannot be seen and the CheckedByCoq zone is materialized only after everything has been processed. The problem is solved by adding the following line in coquille.py, line 308 (right after reset_color()) :

vim.command('redraw')

I am using Coq8.4pl2 under linux. It may be the case that other versions or architectures do not require to redraw explicitely.

Ubuntu hasn't shipped Vim with +python since 16.04. It'd be nice to have +python3 support in coquille.

I made a naive repeat decide equal call and paid the price, having to kill Coq manually. This resulted in Vim not only hanging but consuming 100% CPU. To be fair, I recall similar situations when using Proof General, though I don't recall if I needed to kill emacs in the end.

Perhaps there could be two changes to address this situation:

1. A vim command to kill Coq that can be executed concurrently with a Coq command.
2. Clean recovery from the death of a Coq process.

I use Plug for plugin management, which assumes that master is the default branch of a project. It appears that the default branch for this repo is pathogen-bundle. As a result, when installing with Plug, I got an old version of the code. Worse, I fixed this issue in the code I had checked out (in the master branch), but cannot merge this back into the pathogen-bundle branch, because the two branches share no branch history. Would it be possible to replace the contents of the master branch with the contents of pathogen-bundle, to avoid breaking alternative plugin managers and befuddling potential contributors?

My _CoqProject file contains arguments (such as -R . Namespace) that need to be passd to coqtop. Other IDEs do this, and I can do it manually by passing it to :CoqLaunch. It would be nice if I did not have to do this manually, though.

For example it is not possible with one key press to process all commands in

Theorem true : True.
Proof.
auto.
Qed./EOF

Hello.

I am new to Coq. My expectation is that :Coq Check nat. should write something along the lines of nat : Set to the Infos window. This is not the case: insofar as CoqLaunch was issued previously and, hence, there is a pair of coqtop processes attached to Vim, the following will be displayed, with Vim hanging:

[pid 1828] Unexpected XML message
[pid 1828] Expected XML node: pair
[pid 1828] XML tree received: <state_id val="1"/>

(Though with garbled indentation that I fixed manually for the purpose of clarity of presentation.)

Here 1828 is the process identifier of coqtop -ideslave -main-channel stdfds -async-proofs on.

If I resize terminal window, Vim will unstick, both coqtop processes will die, and the Goals and Infos buffers will get closed.

My operating system is ArchLinux.

Here is the version of Coq I use:

% coqtop --version
The Coq Proof Assistant, version 8.7.1 (December 2017)
compiled on Dec 16 2017 22:25:15 with OCaml 4.05.0

I have cloned coquille at commit df24600 which is the latest at the moment.

Accidentally re-running CoqLaunch adds the splits in the current buffer again, is there a way to detect that it's already been run, or treat this as CoqKill; CoqLaunch?

It seems that coquille can't parse UTF8 characters (or maybe non-ascii characters?); when trying to use a file with spanish accented characters I get the following error:

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/dixego/.vim/bundle/coquille/autoload/coquille.py", line 129, in coq_next
    send_until_fail()
  File "/home/dixego/.vim/bundle/coquille/autoload/coquille.py", line 321, in send_until_fail
    response = CT.advance(message, encoding)
  File "/home/dixego/.vim/bundle/coquille/autoload/coqtop.py", line 247, in advance
    r = call('Add', ((cmd, -1), (cur_state(), True)), encoding)
  File "/home/dixego/.vim/bundle/coquille/autoload/coqtop.py", line 195, in call
    msg = ET.tostring(xml, encoding)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 1126, in tostring
    ElementTree(element).write(file, encoding, method=method)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 820, in write
    serialize(write, self._root, encoding, qnames, namespaces)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 939, in _serialize_xml
    _serialize_xml(write, e, encoding, qnames, None)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 939, in _serialize_xml
    _serialize_xml(write, e, encoding, qnames, None)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 939, in _serialize_xml
    _serialize_xml(write, e, encoding, qnames, None)
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 937, in _serialize_xml
    write(_escape_cdata(text, encoding))
  File "/usr/lib/python2.7/xml/etree/ElementTree.py", line 1073, in _escape_cdata
    return text.encode(encoding, "xmlcharrefreplace")
UnicodeDecodeError: 'ascii' codec can't decode byte 0xc3 in position 7: ordinal not in range(128)

however if I remove all accented characters there's no problem anymore. I should note that all accented characters were within comments, not as part of the code.

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.

First of all, thanks for this great work.

I want to have some old coq ide vim plugin features in coquille,

• in old plugin it was possible to send comment blocks to coq separately, but now when I send next block it consumes all comments and sends up to next definition. I don't want this.
• in old plugin, cursor was moving to last evaluated block automatically. I want to have that feature.

unfortunately I don't know enough vimscript. Is it possible to have that features with some flag or option or do I need to find relevant code and replace?

Thanks,

When the minibufexpl plugin is installed, coquille can initialize and :CoqLaunch seems so succeed, but doesn't make any command (CoqNext, CoqToCursor,...) available.

Not sure if this is a big issue, but it should at least be mentioned in the readme (took me some time to realize the source of the problem). Especially because minibufexpl is part of the standard vim plugins package in some linux distributions (like arch).

I'm getting a 404 from https://camo.githubusercontent.com/1353f36d9dde1d89936984603b3fdcd22ffc5c91/687474703a2f2f3139352e3135342e3138382e33332f2537457472656669732f636f7175696c6c652e706e67

I've got Coq installed and I keep getting this error even after calling :CoqLaunch

Trying to process any command, Coq responds: "Incorrect query". I have Coq 8.4pl13 on Linux.

Sorry, this is a bit of a brain dump.

Hi, the plugin is hanging when I try and use it with the coq from HoTT.
I'm working hard to debug it myself, but was wondering if you had tried to tackle that yourself? Do you know how to debug these kind of issues?

Once I changed it to hoqtop instead of coqtop, it was crashing.
There's a few places where it sends var="info" instead of "good" or "bad", but I fixed those, along with <message> <message_level val="info" /> <string> Warning...</string></message> responses. But coqtop sends those too.

I'm passing the -debug flag to coqtop, and redirecting stderr to a tmp file, but it seems like coqtop is not crashing, and thinks it sent a message to vim.

If I take a closer look at what happens when I send Check 4. to coqtop or hoqtop, I get this reply:

<message><message_level val="warning"/><string>Query commands should not be inserted in scripts</string></message>
<message><message_level val="notice"/><string>4
     : nat</string></message><value val="good"><string></string></value>

That's more that one root node.

Oh, hey, if I set the number of bytes read each time to 1, it fixes the hangs. It might be running into problems with more than one root node sneaking in, like the string <node>1</node><node>2</node>, which'll cause a parse error forever.
It's still running into some problems parsing the goals, and I'm not sure why, since the response I'm retrieving in python/vim is different from the one it's sending?! At least according to the bit of extra debugging code in compiled into hoqtop.
So, I guess there's a extra call to flush or something in coqtop, which is preventing the pairs of nodes to sneak by in one system call to write.

Have there been any reports of infinite loop hangs for regular coqtop?

When running command CoqNext or CoqToCursor, python just crashed and told me an error. By the way, I'm using coq 8.5pl3, python 2.7.13 and vim 8.0.142.

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/Users/kraks/.vim/bundle/coquille/autoload/coquille.py", line 129, in coq_next
    send_until_fail()
  File "/Users/kraks/.vim/bundle/coquille/autoload/coquille.py", line 321, in send_until_fail
    response = CT.advance(message, encoding)
  File "/Users/kraks/.vim/bundle/coquille/autoload/coqtop.py", line 250, in advance
    r = call('Add', ((cmd, -1), (cur_state(), True)), encoding)
  File "/Users/kraks/.vim/bundle/coquille/autoload/coqtop.py", line 200, in call
    response = get_answer()
  File "/Users/kraks/.vim/bundle/coquille/autoload/coqtop.py", line 181, in get_answer
    messageNode = parse_value(c[2])
  File "/usr/local/Cellar/python/2.7.13/Frameworks/Python.framework/Versions/2.7/lib/python2.7/xml/etree/ElementTree.py", line 266, in __getitem__
    return self._children[index]
IndexError: list index out of range

If I make a mistake (such as "cannot unify") in a proof and :CoqToCursor to a later line, the error message doesn't display anywhere. Is there a way to show errors, like the "Errors" tab in CoqIDE?
A workaround is to step through line-by-line in order to see them, but I think there's probably a better way.

And thank you so much for this tool, it's joy to use Coq in Vim.

the minimal pathogen setup

execute pathogen#infect()
syntax on
filetype plugin indent on

does not work with coquille; specifically, :CoqLaunch does not work (vim 7.4.52 on Ubuntu 14.04). What it should expand to, i.e. :call coquille#Launch(), does do something, but any attempt to type in the interaction window results in:

 Error detected while processing InsertEnter Auto commands for "<buffer=1>":
 Traceback (most recent call last):

In the old Coq ide plugin, when I remove a character, if that character was already sent to Coq interpreter, Coq ide was undoing until last non-changed expression that is on left part of cursor. In Coquille, I have to undo changed parts manually and this is worse than old behavior.

Since coquille isn't compatible with Coq 8.4pl3, it could be nice to add to the readme the version required of coqtop & vim (+python).

Using gvim triggers an error message when loading coquille.vim: cannot allocate color 60 (modulo translation). Editing line 99 of coquille.vim to use a standard color name for guibg solves the problem.

When issuing :CoqLaunch under Coq 8.9.0, vim freezes with the message

Don't know what to do with -ideslave
See -help for the list of supported options

vim does not respond to ^c or ^z after this point, and must be killed.

When stepping through the following file (using Linux and Coq version 8.6), the string "<W> Grammar extension: in [constr:operconstr] some rule has been masked" appears on the screen at an unpredictable location:

Inductive natprod : Type :=
| pair : nat -> nat -> natprod.
Notation "( x , y )" := (pair x y).

This string doesn't move when scrolling through this file, so it doesn't seem like Vim is aware of its existence.

The appearing string doesn't seem to be in the coquille files, it looks like it's the output of Coqtop (see for example some of the output here: http://www.lix.polytechnique.fr/coq/pylons/logs/view/QuicksortComplexity/5528711275707690290).

Furthermore, this doesn't happen when I add stderr = subprocess.PIPE to the coqtop = subprocess.Popen(...) call in coqtop.py. So I think this message is from the stderr output of Coqtop.

I'll make a pull request to suppress this message shortly; any suggestions on how to use this message in a helpful way are welcome!

I can see https://framagit.org/tyreunom/coquille which supports NeoVim and asynchronous, which is obviously better. Maybe it makes sense to archive this one and provide a link?

Steps to reproduce :

1. open a new empty file.
2. invoke :CoqLaunch
3. Write some coq code in the buffer.
4. Use CoqNext to eval the added code.

coquille fails with the following error :

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/joris/.vim/bundle/coquille/autoload/coquille.py", line 163, in coq_next
    send_until_fail()
  File "/home/joris/.vim/bundle/coquille/autoload/coquille.py", line 353, in send_until_fail
    xml_template.text = message.decode(encoding)
LookupError: unknown encoding: 

If the buffer already contains any text content before invoking :CoqLaunch, everything works as expected.

It looks like the master and pathogen-bundle branch are currently being updated to support Coq 8.5. However this causes vim to crash for people using Coq 8.4, like me. Since Coq 8.4pl4 is currently the version shipped with Debian stable I think it's worthwhile to have it supported. I saw the tag '8.4' pointing to commit '30a8f16' which did not work on my machine. The merge commit '3bd17ca' however worked great.

If we want to support different Coq version I propose using a branch for each minor version (8.4, 8.5, 8.6) and feature branching. We can then remove the pathogen-bundle branch and let the master branch contain all non-version specific code. What do you think?

Thanks for the project by the way, it's great!

The syntax highlighting doesn't properly handle the case of

Lemma foo: 1 = 1.
Proof.
    Lemma L : 2 = 2.
        auto.
    Qed.
    auto.
Qed.

As the second auto. is marked in red as an error.

2013-04-21 03:06:05 rks_ pis l'intérêt seirl
2013-04-21 03:06:17 rks_ c'est que là mon truc, il marche dans tmux, en ssh
2013-04-21 03:06:43 rks_ ('fin, c'est pas l'intérêt, mais c'est un bonus)
2013-04-21 03:06:49 seirl mouais ok
2013-04-21 03:06:55 seirl sinon tu dev un autre IDE en console
2013-04-21 03:07:01 seirl que t'appelles coquille
2013-04-21 03:07:20 rks_ hum seirl, le nom est pris déjà ?
2013-04-21 03:07:33 rks_ c'est une marque déposée ?
2013-04-21 03:07:43 rks_ parce que si non, je prends carrément ce nom pour mon plugin
2013-04-21 03:08:02 seirl je pense pas que tu puisses déposer une marque pour un nom français
2013-04-21 03:08:08 seirl par contre bonne chance pour le référencement
2013-04-21 03:08:25 def-lkb seirl: tu peux déposer une marque pour allo quoi
2013-04-21 03:09:00 rks_ seirl: boah, l'idée c'est de faire un truc qui marche, et d'être listé là http://coq.inria.fr/related-tools
2013-04-21 03:10:36 seirl bah coquille !
2013-04-21 03:11:23 rks_ %%

Initial goals of coquille were:
[x] to work
[ ] to be listed on http://coq.inria.fr/related-tools

Please fix.

When an error is received the "info" pane is immediately cleared when in insert mode. For example:

Define Food = .

Will only give you a brief flash of:

Syntax error: '.' or '...' expected after [...]

when in insert mode.