Prelude Not Loading On #509

[HazardousPeach]

Describe the bug Upon document creation, coq-lsp produces the following error, preventing further progress:

coq_serapy.coq_backend.CoqExn: Doc.create, internal error: Cannot find a physical path bound to logical path
                            Coq.Init.Prelude.

To Reproduce Steps to reproduce the behavior:

1. git clone git@github.com:ejgallego/coq-lsp.git
2. cd coq-lsp
3. git fetch -f origin pull/509/head:proper-interrupts
4. git checkout proper-interrupts
5. opam install .
6. opam install coq-serapi coq coq-stdlib
7. Send the following messages via stdin:

   
   Content-Length: 462

{"jsonrpc": "2.0", "id": 0, "method": "initialize", "params": {"processId": 1560110, "rootPath": "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16", "rootUri": "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16", "initializationOptions": {"verbosity": 1}, "capabilities": {}, "trace": "off", "workspaceFolders": [{"name": "coq-lsp", "uri":t "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16"}]}}

Content-Length: 57

{"jsonrpc": "2.0", "method": "initialized", "params": {}}

Content-Length: 220

{"jsonrpc": "2.0", "method": "textDocument/didOpen", "params": {"textDocument": {"uri": "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16/local1.v", "languageId": "Coq", "version": 1, "text": ""}}}

Content-Length: 248

{"jsonrpc": "2.0", "method": "textDocument/didChange", "params": {"textDocument": {"uri": "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16/local1.v", "version": 2}, "contentChanges": [{"text": "Unset Printing Notations."}]}}

Content-Length: 215

{"jsonrpc": "2.0", "id": 1, "method": "proof/goals", "params": {"textDocument": {"uri": "file:///work/pi_brun_umass_edu/asanchezster/proverbot9001/CompCert-8.16/local1.v"}, "position": {"line" : 0, "character": 25}}}

**Expected behavior**
The document is initialized and returns no error messages

**Desktop (please complete the following information):**
 - Arch Linux
 - coq-lsp c3eb4f59984eebd440f43c975175b5e01b4d143d

[Alizter]

Does running eval $(opam env) before launching code help?

[HazardousPeach]

No, it doesn't change anything (though I'm not actually using VSCode, I have my own python interface).

[ejgallego]

Hi @HazardousPeach , thanks for the report, we need to document how to do this better.

What does coqc -config say in your case?

As of today, the setup for Coq master is not very friendly to OPAM, likely the paths for Coq are misconfigured, due to the submodules.

So, when you checkout a branch, if you do:

$ make && dune exec -- bash

You get a shell where coqc and coq-lsp are setup properly in PATH (beware of OPAM auto-overriding PATH)

I agree that's a bit annoying for people that would like to integrate with opam, so I'll add a target that does install Coq and coq-lsp into an opam switch for further use.

[ejgallego]

I tried to reproduce, and indeed for me the problem was opam install . used the vendored Coq, which is wrong. This seems due to vendored_dirs.

The following sequence of commands seem to "work for me (TM)"

$ rm `dune` && git commit -m '[tmp] workaround'
$ opam install vendor/coq/coq{-core,-stdlib,}.opam
$ opam install vendor/coq-serapi
$ opam install .

Indeed, opam install . was pulling the submodules and not using the global coq even with -p present.

[ejgallego]

I understand now what is happening: dune build -p coq-lsp will actually use vendor/coq even with the -p option present. I did edit the previous message to remove misleading info.

I guess this could make sense for people vendoring stuff, but not for us.

There is a quick workaround, remove (vendored_dirs vendor) from the dune file. Thus, the above steps finally work for me.

I am not sure what the right fix for us is anymore, there are a few issues already open about this in the dune repos.

[ejgallego]

This is the corresponding Dune issue: https://github.com/ocaml/dune/issues/3911

After thinking a little bit, it seems to me that we can indeed just remove the vendor directory in the coq-lsp.opam file for main.

[ejgallego]

Related: #479 #488