Stream: Coq users

Topic: coq_makefile and tests

view this post on Zulip Gaëtan Gilbert (Jun 15 2022 at 12:47):

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 tests/
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

view this post on Zulip Gaëtan Gilbert (Jun 15 2022 at 12:48):

maybe just have a Makefile.local like https://github.com/arthuraa/deriving/blob/master/CoqMakefile.local ?

view this post on Zulip Karl Palmskog (Jun 15 2022 at 14:13):

I'd recommend using Makefile.coq.local for this, so the test stuff doesn't get installed, etc.

Last updated: Oct 03 2023 at 02:34 UTC