coquille issueshttps://framagit.org/tyreunom/coquille/-/issues2020-04-30T23:13:48Zhttps://framagit.org/tyreunom/coquille/-/issues/32Hang when stepping quickly over comments2020-04-30T23:13:48ZJames D. PollardHang when stepping quickly over commentsEnvironment
===========
* Coq version (run `coqtop -v` if unsure):
```
The Coq Proof Assistant, version 8.10.2 (April 2020)
compiled on Apr 10 2020 23:02:08 with OCaml 4.09.1
```
* Neovim version (run `nvim -v` if unsure):
```
NVIM...Environment
===========
* Coq version (run `coqtop -v` if unsure):
```
The Coq Proof Assistant, version 8.10.2 (April 2020)
compiled on Apr 10 2020 23:02:08 with OCaml 4.09.1
```
* Neovim version (run `nvim -v` if unsure):
```
NVIM v0.4.3
Build type: Release
LuaJIT 2.0.5
Compilation: /usr/bin/cc -march=x86-64 -mtune=generic -O2 -pipe -fno-plt -O2 -DNDEBUG -DMIN_LOG_LEVEL=3 -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -Wmissing-prototypes -Wimplicit-fallthrough -Wvla -fstack-protector-strong -fdiagnostics-color=always -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FROM -I/build/neovim/src/build/config -I/build/neovim/src/neovim-0.4.3/src -I/usr/include -I/build/neovim/src/build/src/nvim/auto -I/build/neovim/src/build/include
Compiled by builduser
Features: +acl +iconv +tui
See ":help feature-compile"
system vimrc file: "$VIM/sysinit.vim"
fall-back for $VIM: "/usr/share/nvim"
Run :checkhealth for more info
```
* Coquille commit (run `git log -1` in coquille's directory if unsure):
` 81cea3080eb781216c4f3ab14dc7a1673d6688f6 `
Description
===========
If I quickly step over multiple lines of comments, e.g.:
```
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
.
.
.
```
Then Coquille is prone to hang after a few lines. Alternatively, jumping to the very end of the block also has the same effect most of the time.
Steps to Reproduce
==================
```
echo "\
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)
(* XXXXXXXXXXXXXXXXXXXXXXXXXX *)\
" > test.v
nvim test.v
```
Then `:call CoqLaunch()` and try stepping down quickly, or jumping to the end of the file.
Debug Output (Optional)
=======================
Not possible: CoqDebug hangs also (seems the Messenger locks up entirely).https://framagit.org/tyreunom/coquille/-/issues/31Issue #17 "Undoing quickly can cause assertion to fail" still persists2020-04-27T16:12:14ZKanashimiaIssue #17 "Undoing quickly can cause assertion to fail" still persistsBasically, when you hold onto undo it undoes itself: ^)
Video: https://www.youtube.com/watch?v=6XSgrMsqBdkBasically, when you hold onto undo it undoes itself: ^)
Video: https://www.youtube.com/watch?v=6XSgrMsqBdkhttps://framagit.org/tyreunom/coquille/-/issues/30Scroll + CoqToCursor kills+hangs Coquille if previous head is offscreen2020-04-09T17:07:33ZCache CacheScroll + CoqToCursor kills+hangs Coquille if previous head is offscreenEnvironment
===========
* Coq version: 8.10.2
* Neovim version: `v0.5.0-nightly-355-g4139678f9` (edit: also repros with the default v0.4.3 build from Homebrew)
* Coquille commit (run `git log -1` in coquille's directory if unsure): `81c...Environment
===========
* Coq version: 8.10.2
* Neovim version: `v0.5.0-nightly-355-g4139678f9` (edit: also repros with the default v0.4.3 build from Homebrew)
* Coquille commit (run `git log -1` in coquille's directory if unsure): `81cea3080`
* I have run `:UpdateRemotePlugins` in neovim but it didn't help: yep
Description
===========
If you go bit by bit through a file, comment by comment, proof by proof, then you can check all of it. However, you generally want to do large swaths at a time, to catch up. Coquille cannot do this at the moment. It can't do large leaps; it silently fails, stops accepting commands, and then hangs on exit.
Steps to Reproduce
==================
1. Find a long .v file. nahas_tutorial.v works for this. Observe you can check a few lines at a time.
2. Scroll down. Takes about a screenful and a half for me.
3. CoqToCursor
4. Nothing happens
5. Go back to the end of the checked part to try a smaller region
6. Observe that you can no longer interact with Coquille at all
7. Attempt to start fresh: `call CoqStop()` hangs. So does exiting the buffer, due to the autocommand.
8. Kill the neovim process externally, because it is no longer accepting input.
((8) shouldn't really ever be a problem with a python plugin -- pynvim has perfectly good facilities for asynchronous functions that don't block the entire editor even if the downstream program is blocking, which coqtop appears to be doing a lot recently.)
Debug Output (Optional)
=======================
Unable to get CoqDebug output because it also hangs.https://framagit.org/tyreunom/coquille/-/issues/23`:call CoqLaunch()` gives error2019-10-17T13:19:46ZSally Brack`:call CoqLaunch()` gives errorEnvironment
===========
* `coqtop -v`:
```
The Coq Proof Assistant, version 8.9.1 (August 2019)
compiled on Aug 17 2019 16:43:13 with OCaml 4.02.3
```
* `nvim -v`:
```
NVIM v0.4.0-1730-ge2ccf47b5
Build type: Debug
LuaJIT 2.0.5
Compilati...Environment
===========
* `coqtop -v`:
```
The Coq Proof Assistant, version 8.9.1 (August 2019)
compiled on Aug 17 2019 16:43:13 with OCaml 4.02.3
```
* `nvim -v`:
```
NVIM v0.4.0-1730-ge2ccf47b5
Build type: Debug
LuaJIT 2.0.5
Compilation: /usr/bin/cc -g -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -Wmissing-prototypes -Wvla -fstack-protector-strong -fdiagnostics-color=always -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FROM -I/home/username/Downloads/neovim/build/config -I/home/username/Downloads/neovim/src -I/home/username/Downloads/neovim/.deps/usr/include -I/usr/include -I/home/username/Downloads/neovim/build/src/nvim/auto -I/home/username/Downloads/neovim/build/include
Compiled by username@machinename
Features: +acl +iconv +tui
See ":help feature-compile"
system vimrc file: "$VIM/sysinit.vim"
fall-back for $VIM: "/home/username/local/neovim/share/nvim"
Run :checkhealth for more info
```
* `git log -1`:
```
commit f9ceda022cd639ae1304f2654be334036445f7d2
Author: LEPILLER Julien <julien.lepiller@irisa.fr>
Date: Fri Jun 28 15:44:00 2019 +0200
```
* I have run `:UpdateRemotePlugins` in neovim but it didn't help:
Yes, does not help.
Description
===========
Calling `:call CoqLaunch()` gives the following error:
```
line 1:
error caught in request handler '/home/username/.local/share/nvim/site/pack/plugin/start/coquille/rplugin/python3/pycoqtop:function:CoqLaunch [[]]':
Traceback (most recent call last):
File "/home/username/.local/share/nvim/site/pack/plugin/start/coquille/rplugin/python3/pycoqtop/__init__.py", line 68, in launch
self.vim.call('coquille#ShowPanels')
File "/home/username/.local/lib/python3.5/site-packages/pynvim/api/nvim.py", line 299, in call
return self.request('nvim_call_function', name, args, **kwargs)
File "/home/username/.local/lib/python3.5/site-packages/pynvim/api/nvim.py", line 182, in request
res = self._session.request(name, *args, **kwargs)
File "/home/username/.local/lib/python3.5/site-packages/pynvim/msgpack_rpc/session.py", line 102, in request
raise self.error_wrapper(err)
pynvim.api.nvim.NvimError: b'Vim(file):E172: Only one file name allowed: file Goals b17ba966-7291-411e-9e02-13e0932912da'
```
```https://framagit.org/tyreunom/coquille/-/issues/20document interactions with coqtop2019-06-28T13:48:47ZJulien Lepillerdocument interactions with coqtopinteractions with coqtop are complex and lead to some annoying bugs (sometimes).
coqtop is run in parallel to coquille. A user interaction can lead to more than one action sent to coqtop, and actions are queued before being sent to coqt...interactions with coqtop are complex and lead to some annoying bugs (sometimes).
coqtop is run in parallel to coquille. A user interaction can lead to more than one action sent to coqtop, and actions are queued before being sent to coqtop for evaluation. Some actions will act on that queue, require coqtop to be in a specific state, etc.
de-synchronisation happens too often, so something must be done.
I need to understand better what coqtop expects from the plugin, what is allowed and what is not. This should lead to a better implementation and testable assumptions!
Scenarios:
* The command ends successfully
* The command ends with an error
* The command doesn't end
On every scenario, what happens if we let them be, and what happens if we send an interrupt in the middle (check for every position an interrupt can be sent; especially before and after answers from coqtop).https://framagit.org/tyreunom/coquille/-/issues/16Autocompile feature2019-10-24T15:57:35ZJulien LepillerAutocompile featureThe idea is to automatically try to (re-)compile a .v file when an import fails. This option would (at least at first) be disabled by default. Users should be able to either enable it globally or per-project/session. Ideally, it would re...The idea is to automatically try to (re-)compile a .v file when an import fails. This option would (at least at first) be disabled by default. Users should be able to either enable it globally or per-project/session. Ideally, it would recursively compile files.Julien LepillerJulien Lepiller