Stream: Coq users

Topic: Coqc path resolution in Require [Import]


view this post on Zulip Mario Carneiro (Dec 10 2023 at 08:55):

How does coqc figure out where to look when seeing [From Bar] Require [Import] Foo? And if it fails what are the usual techniques for debugging this?

More concretely, I'm trying to compile https://github.com/MetaCoq/metacoq/ and running make from the root is able to compile some of the project but it fails at

COQC theories/Primitive.v
File "./theories/Primitive.v", line 4, characters 0-54:
Error: Cannot find a physical path bound to logical path
bytestring with prefix MetaCoq.Utils.

despite apparently completing an earlier COQC theories/bytestring.v step. (Line 4 is:

From MetaCoq.Utils Require Import bytestring MCString.

.)

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:00):

did you do ./configure.sh local before your build?

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:00):

I did ./configure.sh

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:02):

that does seem to be the difference, although I'm hoping to be able to get past the voodoo stage of coqc building at some point

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:03):

both for 8.16 and 8.18, the local makes a difference, e.g., https://github.com/MetaCoq/metacoq/blob/coq-8.18/Makefile#L6

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:06):

if all you want to do is install MetaCoq, we highly recommend using the versioned opam packages here: https://github.com/coq/opam/tree/master/released/packages/coq-metacoq

Building from source requires careful choice of branch, Coq version, Equations version, build command.

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:06):

I want to browse the sources (in vscoq if it matters)

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:06):

so I think that means building from source

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:11):

depending on the branch, the CI configuration might be helpful then: https://github.com/MetaCoq/metacoq/blob/coq-8.18/.github/workflows/build.yml

Otherwise I'd try to follow very carefully https://github.com/MetaCoq/metacoq/blob/coq-8.18/INSTALL.md#getting-the-sources

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:30):

My question remains though. How in general does coqc find things? How do I replicate by hand Coq's lookup mechanism?

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:35):

by default coqc looks in a user-contrib directory which is installed when Coq is installed (Ltac2 is there). Then you can pass other directories to look in via the -Qand -R options. Typically, opam install coq-X just creates a directory user-contrib/X

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:36):

is the user-contribs located relative to the coqc binary in some way or is it in an env var?

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:37):

user-contrib is I believe hardcoded into the binary. Run coqc -where to see its base path

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:37):

And I suppose that local paths for building a project are always done via -Q and -R and that's what the makefile is about

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:37):

ls `coqc -where`/user-contrib

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:38):

that's part of what the Makefile does, sure. But MetaCoq is a mix of Coq and OCaml (that extends Coq via its OCaml API), so it's more complicated

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:44):

another possible approach to build MetaCoq (which will typically take care of all path resolution) is to use Nix and specifically the Coq Nix Toolbox

view this post on Zulip Mario Carneiro (Dec 10 2023 at 09:46):

I was able to compile everything after the ./configure.sh local hint. Now to figure out which combination of things I have to futz with to get vscoq to work... (Seems metacoq is built for coq 8.16 and vscoq wants 8.18+)

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:50):

yes, if you want to use regular VsCoq, as opposed to VsCoq legacy, you will have to use the coq-8.18 branch of MetaCoq.

view this post on Zulip Karl Palmskog (Dec 10 2023 at 09:50):

and if you want regular VsCoq, you also have to install the VsCoq language server, e.g., opam install vscoq-language-server

view this post on Zulip Yann Leray (Dec 10 2023 at 18:54):

To use VSCoq or coq-lsp on the 8.18 branch, cherry-pick commit aec0e80 which edits the VSCode workspace config file

view this post on Zulip Mario Carneiro (Dec 11 2023 at 05:04):

@Yann Leray I don't have a _opam/bin, vscoqtop is located at ~/.opam/coq.8.18/bin instead. Should I edit this, or is there something that is supposed to create an _opam folder in the project directory?

view this post on Zulip Mario Carneiro (Dec 11 2023 at 05:11):

setting "vscoq.path": "~/.opam/coq.8.18/bin/vscoqtop", also didn't work but eliminating it entirely (and using the rest of the metacoq.code-workspace file) seems to work with VsCoq 2 + the 8.18 branch of metacoq

view this post on Zulip Yann Leray (Dec 11 2023 at 10:41):

_opam/bin is the directory where executables go when you install a local opam switch, but you don't need one. I don't exactly know why setting the path as you did din't work, maybe it doesn't recognize "~" and you need the full path but, either way, if it works without it, the most important part is the args field so VSCoq/coq-lsp know where stuff is


Last updated: Jun 22 2024 at 16:02 UTC