The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

I was intending it more as pseudocode.
Looking at your actual makefile I would have this rule

tests/%.vo: tests/%.v

and after looking closer at coq_makefile's stuff I would use

tests/%.vo: tests/%.v real-all

does that work? It should allow running make for individual test files 
too. (real-all is a coq_makefile phony which depends on VOFILES and on 
the compiled plugin files)

Gaëtan Gilbert

On 27/04/2018 16:43, Beta Ziliani wrote:
> Thanks for the quick response.  But unfortunately it doesn't work :(
>
> It somehow realizes the dependencies, but doesn’t build anything.  The 
> same output is obtained without the $(VOFILES), BTW.
>
> |➜ Mtac2 git:(master) ✗ make test
> COQDEP theories/Mtac2.v make: Nothing to be done for 'test'. |
>
>
>
>
> ​
>
>
>
> On Thu, Apr 26, 2018 at 10:52 AM, Gaëtan Gilbert 
> <gaetan.gilbert AT skyskimmer.net <mailto:gaetan.gilbert AT skyskimmer.net>> 
> wrote:
>
>     something like
>
>     tests: $(VOFILES)
>
>     should work
>
>     Gaëtan Gilbert
>
>
>     On 26/04/2018 15:13, Beta Ziliani wrote:
>
>         Hi list,
>
>         In Mtac2 we have a tests folder with, ehm, the tests.  This
>         folder is not installed in the user's space.  To make tests, we
>         have an ad-hoc compilation rule in the Makefile.local file [1]. 
>         However, we don't know how to make it depend on the theories
>         folder, in order to re-compile the (relevant) tests when a file
>         in theories was changed.  An obvious dirty option is to move
>         tests inside theories, but I pretty much prefer to avoid doing that.
>
>         Any suggestions?
>
>         Many thanks,
>         Beta
>
>         [1]
>         
> https://github.com/Mtac2/Mtac2/blob/607689192296bc42d75bc933ab2229a6b347c73b/Makefile.local#L1
>         
> <https://github.com/Mtac2/Mtac2/blob/607689192296bc42d75bc933ab2229a6b347c73b/Makefile.local#L1>