Stream: Coq users

Topic: How do nested _CoqProjects and Makefiles work?


view this post on Zulip Paul Snively (Jan 02 2023 at 14:34):

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!

view this post on Zulip Gaëtan Gilbert (Jan 02 2023 at 14:42):

looks like you have -R . Top in the submodule coqproject

view this post on Zulip Karl Palmskog (Jan 02 2023 at 14:43):

right, you can't compile a project with one name like Top, and then use those compiled files under another name like Zoo elsewhere

view this post on Zulip Paul Snively (Jan 03 2023 at 00:47):

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.

view this post on Zulip Paolo Giarrusso (Jan 03 2023 at 02:27):

Adding -arg -w -arg -overriding-logical-loadpath in your _CoqProject should disable the warning

view this post on Zulip Paolo Giarrusso (Jan 03 2023 at 02:28):

(and yes, "X is underdocumented in Coq" _is_ often true)

view this post on Zulip Paolo Giarrusso (Jan 03 2023 at 02:31):

_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

view this post on Zulip Paul Snively (Jan 03 2023 at 13:45):

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: Jun 15 2024 at 05:01 UTC