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
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.
-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.
_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 04 2023 at 19:01 UTC