How to resolve coq suffix import error (physical path bound to logical path)

Asked Feb 12 '17 at 08:19

Active Feb 12 '17 at 08:19

Viewed 3,054 times

Probably a coq newbie question, but I could not find a ready solution so I'll ask here for reference. The cocq version is 8.5pl2

I tried to build coqfj. The first make attempt has failed with some error in line 37 in src/FJ/ClassTable.v. This question is not about that error.

Taking a closer look, I opened ClassTable.v in emacs proofgeneral and pressed C-c C-n, or alternatively run coqc src/FJ/ClassTable.v. The result is an error in line 1:

File "./src/FJ/ClassTable.v", line 1, characters 15-23:
Error: Cannot find a physical path bound to logical path matching suffix FJ.

It seems the import require import FJ.Lists cannot be resolved (although FJ is used as a prefix, not suffix). I've noticed that make has already created a compiled file src/Lists.vo, that should be picked up by coqc.

How to tell coqc that it should resolve this "suffix" by looking at either the *.vo or *.v files in the src folder?

asked Feb 12 '17 at 08:19

Lars Bohl

1,001
16
20

5

`coqc -R src FJ src/FJ/ClassTable.v` should work. – Anton Trunov Feb 12 '17 at 08:57
1

good. how to make it stick in pg? – Lars Bohl Feb 12 '17 at 09:07
Hmmm, I tried opening `ClassTable.v` in Emacs and it just works (I mean the imports work)! I have Emacs 25.1 with the latest PG and [company-coq](https://github.com/cpitclaudel/company-coq) on top of it. – Anton Trunov Feb 12 '17 at 09:16
1

Do you have `_CoqProject` file in the project root directory with `-R src FJ` in its first line? It should be there if you didn't (accidentally) delete/modify it. My guess is that PG uses that file. – Anton Trunov Feb 12 '17 at 09:20
1

It works now after reinstalling PG from instructions here https://github.com/ProofGeneral/PG – Lars Bohl Feb 12 '17 at 09:32
1

did you manage to fix this? – Charlie Parker Nov 26 '18 at 01:20

How to resolve coq suffix import error (physical path bound to logical path)

0 Answers0