Stream: coq-lsp

Topic: setup help


view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:17):

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.

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:18):

Has anyone run into this, or has any idea as to what's causing it or how to fix it?

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 23:28):

That's a Coq plugin, where else should coq-lsp be looking for things?

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 23:30):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:32):

[I hope the doc is not too buggy]

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:33):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:33):

As you can see for now we just send the goals as strings, but that's easy to fix, open an issue please.

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:33):

Re the rest, give me one sec

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:34):

@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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 24 2023 at 23:38):

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.

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 23:46):

sorry for the wrong suggestions, I striked them out

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:49):

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.

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:53):

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

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:56):

didOpen goes through fine now, didChange reports this:

view this post on Zulip Alex Sanchez-Stern (Jan 24 2023 at 23:56):

$/logTrace {'message': '[process_queue]: Anomaly "Uncaught exception Not_found."\nPlease report at http://coq.inria.fr/bugs/.'}

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 00:01):

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?

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 00:37):

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.

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 00:49):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:08):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:09):

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)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:10):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:11):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:12):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:13):

They go in the initializationOptions field, and they are documented both in OCaml and json format

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 01:14):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:15):

I'd be surprised if that's the Coq code and not some problem with the JSON but let's indeed see, thanks!

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 01:18):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:19):

Thanks to you! I see no problem with that request, this is what I send:

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:19):

[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"
        }
    ]
}

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:21):

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.

view this post on Zulip Alex Sanchez-Stern (Jan 25 2023 at 01:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 01:25):

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.

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:23):

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?

view this post on Zulip Ali Caglayan (Feb 06 2023 at 21:38):

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

view this post on Zulip Ali Caglayan (Feb 06 2023 at 21:38):

It is in editor/ btw

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:40):

Hi @Alex Sanchez-Stern , server should never crash, do you have a log of the crash?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:41):

In particular it should still be possible not to send the init options

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:41):

But we did some changes to serialization so I'd be not suprised if we broke it.

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:43):

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

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:45):

Now that I understand the issue I can pass "." as the rootPath and it works fine

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:48):

Ah yes, thanks for the report Alex

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:49):

Indeed this is a bug on coq-lsp side

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:49):

rootPath is optional

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:49):

I read the spec wrong

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:52):

Ah okay great! I can file an issue if you like

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:52):

https://github.com/ejgallego/coq-lsp/issues/294

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 21:52):

I just did, sorry for the bug

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:57):

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?

view this post on Zulip Alex Sanchez-Stern (Feb 06 2023 at 21:59):

Also ":" is invalid as of that commit in a uri

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:04):

Oh that's quite a good point

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:05):

Indeed I think that Coq doesn't support - and : in file names

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:05):

do you need that?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:06):

This is because Coq uses the filename and the usual -Q/-R bindings to map file name to module name

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:07):

So for that, I def suggest @Alex Sanchez-Stern you open an issue with the URIs that should be valid

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:07):

see also https://github.com/ejgallego/coq-lsp/issues/187

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 22:07):

lots to improve w.r.t. uris

view this post on Zulip Alex Sanchez-Stern (Feb 07 2023 at 01:29):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2023 at 01:37):

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,

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2023 at 01:37):

But I'm happy to support non-file URIs too

view this post on Zulip Alex Sanchez-Stern (Feb 07 2023 at 01:38):

Sounds like a reasonable restriction for the filenames.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2023 at 01:42):

If we get a non-file URI, I will just disable saving to a .vo file, but other than that, it should work.

view this post on Zulip Jim Portegies (Feb 08 2023 at 07:06):

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)"

view this post on Zulip Jim Portegies (Feb 08 2023 at 07:06):

The above error messages only appear on linux

view this post on Zulip Jim Portegies (Feb 08 2023 at 07:24):

I'm sorry, I missed the chat in the General Chat, I think I am having the same problem

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2023 at 18:23):

Yes @Jim Portegies , this is a bug on how we interpreted the spec, you need to pass rootPath

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2023 at 18:23):

that's already fixed, I hope I get a bit of time and make json parsing better

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2023 at 18:24):

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