Installation on MacOS with ZSH does not work
Opened this issue · 12 comments
I installed coqoune using
plug "guest0x0/coqoune" subset %{
coqoune.kak
}
which results in
Error: plug.kak: 'coqoune': keyword 'subset' is no longer supported.
Leaving it out and using
plug "guest0x0/coqoune"
results in
shell stderr: <<<
sh: line 1: -15: substring expression < 0
>>>
and
'source': /rc/syntax.kak: No such file or directory
Trying to source the file manually results in the same error.
It seems like echo ${kak_source:0:-15} does not work.
ZSH: 5.8
kak: v2021.08.28
For the subset keyword error, that seems to be an upstream change from plug.kak. It appears that simply removing the subset clause is fine.
For the second problem, I have changed the evil negative indexing to parametere expansion, hopefully it works.
BTW, there are some known bugs with the *result* parser. I would probably rewrite this plugin, using something other than shell once I've got time... I would like to have a little survey here. For a Coq user, which of python and OCaml sounds more "zero dependency"? I'll probably choose between one of the two for the rewrite.
The installation work, but using it still has a similar problem.
When I try to edit this file (test.v)
Definition foo := 1.
and run :coq-start, nothing seems to happen (there exists a goal and a result buffer, but they are not opened and they are empty).
running :coq-next results in
shell stderr <<<
coqoune.sh: line 3: (-11): substring expression < 0
coqoune.sh: line 47: /tmp/coqoune-test/in: No such file or directory
>>>
So it seems like more evil negative indexing exists.
Regarding Python vs. OCaml: IMO OCaml is more zero dependency, as you need it anyway to use Coq
For the first part, that's the expected behavior. When you enter a file without performing any coq-next or coq-to-cursor, the background Coq compiler is at a state of receiving no input.
For the second part, turns out it's in fact a careless mistake elsewhere. The shell scripts use some features not present in POSIX, so it actually choose one of zsh, bash and ksh to run. However somewhere in the rc file I forgot to invoke the interpreter and called a shell script directly. The new commit should fix this.
Still, nothing happens for me. Now there are no errors in the *debug* buffer, but :coq-next seems to do nothing. The *goal* and *result* buffers are still empty and the buffer with the code shows no sign of state-advancement.
This probably has something to do with shell compatibility, as I cannot reproduce this issue. So could you try the following:
- open a random Coq file
coq-start(if you haven's configured filetype hooks for it) thencoq-nextcoq-dump-log <log_file_name>
and paste the log file? That would help locate the issue I guess.
File: test.v
Definition foo := 1.
commands:
coq-start
coq-next
coq-dump test.log
File: test.log
cmd: init
to be sent: init
<call val="Init"><option val="none"/></call>
/Users/ds3/Opt/coqoune/event_loop.sh: line 428: (-2): substring expression < 0
cmd: user-input
cmd: add:1.21
cmd: goal
So it seems like yet another evil negative index exists
Weird. Zsh should support negative index. Could you do coq-start, then echo %opt{coqoune_shell} and paste the output? If it is not zsh, you can try set-option <scope> coqoushe_shell zsh explicitly. If that doesn't work, I'll dig into the zsh document to see what happens.
Oh, that's weird:
:echo %opt{coqoune_shell}
Outputs
bash
After setting
set-option global coqoune-shell zsh
Doing
coq-start
coq-next
seems to work (Definition foo := 1. is underlined).
But any subsequent command does nothing.
For example
Definition foo := 1.
Definition bar := 2.
and then
coq-start
coq-next
coq-next
Only underlines Definition foo := 1..
Also, the *goal* and *result* buffers are always empty.
If I have
Lemma foo : 1 = 1.
and do
set-option global coqoune-shell zsh
coq-start
coq-next
nothing happens.
Both buffers stay empty.
Should I open a new issue for these problems?
It seems, this one is fixed by setting coqoune-shell correctly
On first glance I see nothing weird in the log
cmd: init
to be sent: init
coqidetop: value: <state_id val="1"/>
cmd: value
command processed: init
get new state_id: 1
cmd: user-input
cmd: add:1.21
to be sent: add:1.21
Definition foo := 1.2<state_id val="%s"/>
coqidetop: value: <state_id val="2"/>
cmd: value
command processed: add:1.21
get new state_id: 2
cmd: goal
to be sent: goal
coqidetop: feedback: <state_id val="2"/><feedback_content val="processingin">master</feedback_content>
cmd: feedback
coqidetop: feedback: <state_id val="1"/><feedback_content val="processed"/>
cmd: feedback
coqidetop: feedback: <state_id val="2"/><feedback_content val="message"><message_level val="info"/><>foo is defined</></feedback_content>
coqidetop: feedback: <state_id val="2"/><feedback_content val="processed"/>
cmd: feedback
coqidetop: value:
I guess it has something to do with coqidetop outputting newline or not. I remember when I first developed this plugin I never observed coqidetop giving any newline, but in the log there are newlines. In the last line of log the script gets nothing for value. That may be caused by some bug in reading coqidetop's output. Anyway I'll update the code to make it robust against with/without newline.
The log is quite mysterious, in the sense that the outermost tags of the xml is gone. I don't have OS X devices available, so debugging this problem seems very difficult.
I would be quite busy this week. When I have more time next week I plan to start rewriting this plugin using OCaml. Hence this issue would probably not get fixed in the shell version... Really sorry about that. I'll try to finish the OCaml rewrite as soon as possible.
The new OCaml version is now available. It should avoid all the shell platform incompability problems altogether. Never gonna write anything serious using shell scrip anymore :(