Hey coq-lsp folks,
I'm playing around with building a python interface to coq-lsp with a high-level api. I initially just installed coq-lsp from opam, but it seems that version is quite old (0.01), and doesn't return much goal information (no background, shelved, or given up goals), so I decided to try a newer one. I can build the main branch from source fine, and send an initialize
and initialized
message fine, but when I run didOpen
, I get:
'[process_queue]: Serving Request: textDocument/didOpen'
message in $/logTrace, and then this message in window/logMessage:
{'type': 1, 'message': 'Fleche.Doc.create, internal error: Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\\"/home/alexss/.opam/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlLocusops__10\\")")'}
This error seems to prevent future requests like didChange
from working.
From the error message, it seems like while I'm using the coq-lsp binary from my from-source build, it is still trying to link against ocaml code from my opam switch, which has different versions of things and thus fails. But I can't figure out why it is looking for these libraries in my opam switch. I tried setting my PATH, OPAM_SWITCH_PREFIX, and CAML_LD_LIBRARY_PATH environment variables to point to the appropriate place in the coq-lsp build directory, but it didn't change anything.
Has anyone run into this, or has any idea as to what's causing it or how to fix it?
That's a Coq plugin, where else should coq-lsp be looking for things?
for lowest friction, I'd avoid the _necessity_ to mess with those settings (because there are more) — and just install everything but coq-lsp
via opam
Hi @Alex Sanchez-Stern , indeed you get that dynlink error because you need to run coq-lsp
when built from source with the right OCAMLPATH
, for example make && dune exec -- coq-lsp
will set that up.
Note that the version in opam has a bug in the display of the version number, likely yours is 0.1.3. But I much recommend master
now that you have built it.
To show the goals you need to send a $/coq/goals
request, that's outside of the protocol. See https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md
[I hope the doc is not too buggy]
Re where should coq-lsp be looking for things: Well when I build coq-lsp from source, it builds its own version of that plugin, located at $COQ_LSP_DIR/_build/install/default/lib/coq-core/plugins
, that is what I wanted to point it at.
As you can see for now we just send the goals as strings, but that's easy to fix, open an issue please.
Re the rest, give me one sec
@Alex Sanchez-Stern Coq locates its plugins using ocamlfind, so it doesn't matter how Coq was built, the OCAMLPATH
variable has to point to the directory you just wrote, or indeed Coq will wrongly locate the plugins in the opam switch. That's a PITA.
so export OCAMLPATH=$COQ_LSP_DIR/_build/install/default/lib/coq-core/plugins
will fix your woes. We are hoping to have a better build setup anyways soon.
sorry for the wrong suggestions, I striked them out
Huh, adding that export OCAMLPATH
command did something, but now the server quits immediately before I can call "initialize". I'll see if cd to the appropriate directory and using dune exec
helps things.
Ah wait, the exiting immediately thing seemed to be due to one of the other environment variables I set, when I just open a fresh shell and do eval $(opam env)
, then use dune exec -- coq-lsp
in the appropriate directory, it gets farther
didOpen goes through fine now, didChange reports this:
$/logTrace {'message': '[process_queue]: Anomaly "Uncaught exception Not_found."\nPlease report at http://coq.inria.fr/bugs/.'}
If I don't do any didChange though, and just do a didOpen with the contents of the file, and then run a proof/goals
message, I get a reasonable goals object. However, if I split into two goals and then focus the first one, I don't see the background goal anywhere in the goal response. With coq-serapi, there was a bg_goals field that had the unfocused goals, but I don't see anything corresponding here. Maybe that's what the "stack" field in GoalConfig is supposed to be? But that's still coming back as "None" for me when I have background goals. Is this a known limitation of the current version, or is there somewhere else I should be looking for background/unfocused goals?
Oh, is there anything in particular I need to be passing as capabilities during registration? I've been passing an empty capabilities object since that didn't seem to break anything and none of the capabilities here seemed relevant.
If it's relevant, the didChange I'm doing is the one that replaces the entire document with a new one. Not sure why it's giving me the uncaught exception Anomaly, I've seen it before sometimes deep in proofs when doing search, but never on such a simple proof/change.
Indeed @Alex Sanchez-Stern the stack
object is not filled in yet, I've been still experimenting with how to organize the protocol, see https://github.com/ejgallego/coq-lsp/pull/237 for a fix.
It would be helpful if you could post the input that created problems, the server is not yet very hardened, tho I'm confident it will soon be. didChange
is tricky, be aware that we only support method 1 for sync (as advertised)
We can do better of course, I'd recommend using the trace windows with verbose
in VS Studio if you have any doubt about what's on the wirte.
Alex Sanchez-Stern said:
If it's relevant, the didChange I'm doing is the one that replaces the entire document with a new one. Not sure why it's giving me the uncaught exception Anomaly, I've seen it before sometimes deep in proofs when doing search, but never on such a simple proof/change.
That's likely some kind of parsing error, if you enable backtraces (in fleche/debug.ml, soon as an option) we can see what the problem is
Alex Sanchez-Stern said:
Oh, is there anything in particular I need to be passing as capabilities during registration? I've been passing an empty capabilities object since that didn't seem to break anything and none of the capabilities here seemed relevant.
The main important field in initialization is the server options, see package.json
They go in the initializationOptions
field, and they are documented both in OCaml and json format
Emilio Jesús Gallego Arias said:
It would be helpful if you could post the input that created problems, the server is not yet very hardened, tho I'm confident it will soon be.
didChange
is tricky, be aware that we only support method 1 for sync (as advertised)
You mean the Coq code input? Right now I'm sending:
Theorem nat_refl: forall n: nat, n = n.
Proof.
induction n.
on didOpen, and then sending:
Theorem nat_refl: forall n: nat, n = n.
Proof.
induction n.
{
on didChange
I'd be surprised if that's the Coq code and not some problem with the JSON but let's indeed see, thanks!
Thanks Emilio! Thanks for being patient with me and answering all my questions. I'll keep pushing on this when I have time and try to get all the issues surfaced.
Thanks to you! I see no problem with that request, this is what I send:
[Trace - 2:19:00] Sending notification 'textDocument/didChange'.
Params: {
"textDocument": {
"uri": "file:///home/egallego/research/coq-lsp/examples/pbroken.v",
"version": 15
},
"contentChanges": [
{
"text": "Theorem nat_refl: forall n: nat, n = n.\nProof.\ninduction n.\n{\n"
}
]
}
Gonna go to bed, but last useful pointer, you can use the hover request to ask for info about the document processing status.
It is not very refined in terms of structured data, but it should take a few mins to make that better.
Great thanks! It looks like I wasn't passing the "version", when I do the error changes, so that was probably the problem. Seems like a weird error message for that mistake, but obviously nice error messages are a later-in-the-process kind of thing
Good to hear it was that, indeed the less refined part is the json input / output as you can see, you hit two problem (goals, and didChanges) just starting. I'll put a bit more effort on that layer, so far it wasn't my worry.
Reviving this thread, but @Emilio Jesús Gallego Arias mentioed something before about initialization options for the LSP server that are in some sort of package.json
. I didn't look to deeply into it at the time because my coq-lsp install worked without any initialization options, but more recent versions have been crashing, so I wanted to look into what these options are. But I can't find a package.json
in the github repo, is it somewhere else? And the protocol documentation says what capabilities are supported by the server, but nothing about what capabilities need to be advertised by the client. Does anyone know where I can find the package.json
?
When you are in Github viewing a repository, if you press t
it brings up the "file filter" mode. This will let you find package.json
It is in editor/ btw
Hi @Alex Sanchez-Stern , server should never crash, do you have a log of the crash?
In particular it should still be possible not to send the init options
But we did some changes to serialization so I'd be not suprised if we broke it.
Sorry not really a crash per-say, it's sending an error message that my code doesn't recognize and so the handling code fails. The error message is "Yojson.Safe.Util.Type_error("Expected string, got null", 870828711)", problem was introduced in this commit https://github.com/ejgallego/coq-lsp/commit/0ad23394027675bd3f6c848ebe2639a7bb62ac01 because it assumes a rootPath was passed
Now that I understand the issue I can pass "." as the rootPath and it works fine
Ah yes, thanks for the report Alex
Indeed this is a bug on coq-lsp side
rootPath is optional
I read the spec wrong
Ah okay great! I can file an issue if you like
https://github.com/ejgallego/coq-lsp/issues/294
I just did, sorry for the bug
No problem! Another thing I noticed was that this commit: https://github.com/ejgallego/coq-lsp/commit/d704cb47017030326c6d622c03346c2edb6f07be made it invalid to have a "-" in a document URI, was that intentional?
Also ":" is invalid as of that commit in a uri
Oh that's quite a good point
Indeed I think that Coq doesn't support -
and :
in file names
do you need that?
This is because Coq uses the filename and the usual -Q/-R
bindings to map file name to module name
We can indeed have coq-lsp be more liberal, but we'd need to translate that to some particular Coq module name that is valid
So for that, I def suggest @Alex Sanchez-Stern you open an issue with the URIs that should be valid
see also https://github.com/ejgallego/coq-lsp/issues/187
lots to improve w.r.t. uris
Oh no problem, I don't actually need those URI's. I just noticed that something had changed, and it didn't seem to be documented anywhere. Since it didn't actually correspond to any file on my end, I wasn't thinking about using something which was a valid filename, before i was just using the string "local:1". It looks like it also needs to end with the right extension too, so now local.v
is what I use that seems to work.
Oh I see, sorry for the trouble, I have added some documentation and tweaked the changelog.
It is not clear to me what kind of URI the LSP server protocol expects, so for now coq-lsp requires a valid file, as indeed saving the .vo
file of a buffer in progress is supported (that requires to resolve the uri to a valid Coq library name)
Extension checking is indeed now more strict, as for example .mv
files are interpreted as markdown files, and we will likely support other formats,
But I'm happy to support non-file URIs too
Sounds like a reasonable restriction for the filenames.
If we get a non-file URI, I will just disable saving to a .vo file, but other than that, it should work.
Hi all, I'm trying to get coq-lsp to work with vscode on any platform, but failing so far. I use version 0.1.4+v8.16. As far as I can see the server starts but then soon after crashes. Error messages are : [CoqLspOption.of_yojson error: ] JFleche.Config.Unicode_completion.t
and [fatal error]: Yojson.Safe.Util.Type_error("Expected string, got null"), 870828711)
[fatal_error [coq iprint]]: Anomaly "Uncaught exception Yojson.Safe.Util.Type_error("Expected string, got null", 870828711)"
The above error messages only appear on linux
I'm sorry, I missed the chat in the General Chat, I think I am having the same problem
Yes @Jim Portegies , this is a bug on how we interpreted the spec, you need to pass rootPath
that's already fixed, I hope I get a bit of time and make json parsing better
Actually in the main code json parsing fails better, but indeed the init routine is not so robust :/
Last updated: Mar 29 2024 at 08:39 UTC