search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
135 stars 31 forks source link

Serlib warning #800

Open MRandl opened 1 week ago

MRandl commented 1 week ago

Describe the bug On my machine, coq-lsp gives the following warning:

Serlib plugin: coq-serapi.serlib.btauto is not available.
Incremental checking for commands in this plugin will be impacted.

It happens when attempting to browse files from github.com/MRandl/verith It does not seem to have an impact on my workflow

To Reproduce Steps to reproduce the behavior: This warning was not emitted on my other machine, so it must be environment-dependent

  1. clone verith as above
  2. make
  3. browse Cmod.v The first import displays the warning

Expected behavior No warning, as on the other machine

Screenshots If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

MRandl commented 1 week ago

I'll gladly add more info on my environment if you need it !

ejgallego commented 1 week ago

Thanks @MRandl for tying out LSP and taking the time to submit this issue!

This is mostly a developer warning, and for this plugin totally harmless.

I think time has come to disable it in the 0.2.x. series , tho this particular one is already fixed in master (merging serlib into coq-lsp fixed this , cc #698 )

MRandl commented 1 week ago

All good then ! Thanks