Eric Mark Martin (Dec 07 2021 at 01:28): 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
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?]
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
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?
Quinn (Jan 24 2022 at 00:19):emacs, coqide? the solution will depend.
Li-yao (Jan 24 2022 at 00:19):@Raymond Baker have you compiled the library already?
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.
Li-yao (Jan 24 2022 at 00:21):They all do the same
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
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.
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".
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"
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...
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.
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: Oct 05 2023 at 02:01 UTC