Stream: Coq users

Topic: Cannot find a phyical path bound to logical path


view this post on Zulip Eric Mark Martin (Dec 07 2021 at 01:28):

I'm getting the error "Cannot find a physical path bound to logical path matching suffix
<> and prefix Coq." I've seen some discussions of this issue but never for prefix Coq. What might be going on here? I have coq installed via a local opam switch, version 8.14.1

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 03:34):

Either the prefix for configure for Coq is wrong, or the lib/coq/theories dir somehow got empty [stdlib not built?]

view this post on Zulip Eric Mark Martin (Dec 19 2021 at 21:33):

It seems I was able to fix this by installing Coq through linuxbrew rather than apt

view this post on Zulip Raymond Baker (Jan 24 2022 at 00:17):

Hey y'all, I've seen this problem a few places but have found no solutions which fixed it. I am trying to get the UniMath library to work and, whenever I try to load a file in the UniMath directory, I get the error "cannot find physical path matching suffix". This seems to happen for every file within the UniMath directory. It seems like a wholesale problem on how I set up UniMath but I can't figure out what went wrong. Anyone have some ideas?

view this post on Zulip Quinn (Jan 24 2022 at 00:19):

emacs, coqide? the solution will depend.

view this post on Zulip Li-yao (Jan 24 2022 at 00:19):

@Raymond Baker have you compiled the library already?

view this post on Zulip Quinn (Jan 24 2022 at 00:19):

proof general (emacs) is looking for something called a _CoqProject file to resolve this. I haven't the slightest what coqide does.

view this post on Zulip Li-yao (Jan 24 2022 at 00:21):

They all do the same

view this post on Zulip Li-yao (Jan 24 2022 at 00:29):

Ah no, actually proof general can also be configured via .dir-locals.el, and that's how UniMath does it. So if you're using coqide you'll need to set a bunch of options yourself. https://github.com/UniMath/UniMath/blob/master/INSTALL_COQIDE.md

view this post on Zulip Raymond Baker (Jan 24 2022 at 01:15):

Hey, sorry for the delayed response. @Quinn I'm working in coqide 8.13.2 on fedora 35.

view this post on Zulip Raymond Baker (Jan 24 2022 at 01:17):

@Li-yao I ran "make" in the top level of the UniMath directory. "make" returned some errors but I thought it still succeded. The errors were things like "Error: The file /usr/lib64/ocaml/str.cmxa is not a compilation unit description".

view this post on Zulip Raymond Baker (Jan 24 2022 at 01:19):

Though, there was more than one of these errors. They were of the same type, just with different files
There was also an error near the end that read "Error: Unbound module Mltop
make[2]: *** [Makefile.build:422: bin/coqtop.opt] Error 2
make[2]: Leaving directory '/home/rymndbkr/UniMath/sub/coq'
make[1]: *** [Makefile.make:178: submake] Error 2
make[1]: Leaving directory '/home/rymndbkr/UniMath/sub/coq'
Makefile:76: .coq_makefile_output.conf: No such file or directory
make: *** [Makefile:247: sub/coq/bin/coq_makefile] Error 2"

view this post on Zulip Raymond Baker (Jan 24 2022 at 01:19):

the more I look at it the more I think this is whats causing the problem. Maybe I was naive to think "make" succeeded...

view this post on Zulip Raymond Baker (Jan 24 2022 at 01:31):

I think one of the problems is with ocaml. All the files where I get the "is not a compilation unit description" error have to do with ocaml. Not sure whats causing this though.

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 07:53):

Do those cmxa files exist on your system? Maybe you're missing OCaml or its dev packages?


Last updated: Feb 04 2023 at 21:02 UTC