Is there a recommended way to have some test files with coq_makefile? ie I have my main files in
theories/foo.v and I want a makefile target
test which compiles some .v files in
If I put
-Q tests Test in my _CoqProject coq_makefile will think they are part of the main build and will get confused with my
-Q theories Whatever
maybe just have a Makefile.local like https://github.com/arthuraa/deriving/blob/master/CoqMakefile.local ?
I'd recommend using
Makefile.coq.local for this, so the test stuff doesn't get installed, etc.
Last updated: Jan 28 2023 at 05:02 UTC