Hi everyone! I've started a new project at https://github.com/paul-snively/verse, trying to use _CoqProject and coq_makefile with a submodule that has its own _CoqProject and Makefile. I build the submodule with make -C submodules/strategies
and try to depend on it in my _CoqProject with -R submodules/strategies/main Zoo
, but when I From Zoo Require Import Preliminaries
, for example, in my source, coqc
complains that the library "Top.main.Preliminaries" is found rather than "Zoo.Preliminaries". Any advice would be most welcome!
looks like you have -R . Top
in the submodule coqproject
right, you can't compile a project with one name like Top
, and then use those compiled files under another name like Zoo
elsewhere
OK, I at least got overriding the logical path to work. But now I get:
Warning: /home/psnively/verse/submodules/strategies/main was previously bound
to Top.main; it is remapped to Zoo [overriding-logical-loadpath,loadpath]
Even though I have:
COQFLAGS = '-q -w -overriding-logical-loadpath'
in my coq_makefile invocation for the "strategies" submodule. In general, it seems like disabling warnings in Coq is badly underdocumented.
Adding -arg -w -arg -overriding-logical-loadpath
in your _CoqProject
should disable the warning
(and yes, "X is underdocumented in Coq" _is_ often true)
_however_, rather than disabling this warning (didn't even know you could), I'd consider just ignoring make -C submodules/strategies
.
If your _CoqProject
only has
-Q src Verse
-R submodules/strategies/main Zoo
and you use e.g. coq_makefile -f _CoqProject -o Makefile.coq $(find . -name '*.v')
to generate Makefile.coq
, your life might well become simpler
It may come to that. But I'd really rather continue to build submodules "on their own terms," so to speak. Thanks for the tip!
Last updated: Oct 13 2024 at 01:02 UTC