The Coq mailing list

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

s/have this rule/change this rule/

Gaëtan Gilbert

On 27/04/2018 16:49, Gaëtan Gilbert wrote:
> 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>