coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] tests in plugins

From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] tests in plugins
Date: Fri, 27 Apr 2018 11:43:09 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=PermError smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT agni.famaf.unc.edu.ar
Ironport-phdr: 9a23:JtC/IxWSvfUliE2a8OMgJsX8YmbV8LGtZVwlr6E/grcLSJyIuqrYbBeFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAIy8YYsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4Et8TrnvUsM/6P7oRXuC0yKnIzC/Mb/VX2Tzg74XHaREgofCIXbJxa8XRz0gvGhjLjlqKrIzqJT2V2v4Qs2id8+VsT/yghHM6qw1ruDev3N4hh4/UjYwbzVDE8D92wIczJdCgR057YMKkEJtNty6BLYd5XsQiQ2RutS0nybMGoYa2cDYWxJg73RLTdv2Kf5KV7h/hTuqdPCt0iXJ9dL6hmxq/9VKsx+78W8WuzlpGsCRInsPRun0P2BHe7NWMROFn8Ue7wzmP0hje6uFaLkAwkqrWM4QuwrE2lpoSq0jDEDX5mEDsg6+YbEkk5+6o5Pj9brr4u5CcKpV4hRvkMqg2m8y/B/o3MhQWUmSF5eiwyKfv8VD4TblQk/E7kLPVvI3GKckbvqK5BhVa0ocn6xaxFTem19EYkGEcI1NEeRKHi4npNEvIIPD5Fvq/jU6jkDJxyPDIJLHhH5PNIWTZnLj/YLl99lRQxxApzdxH/ZJbFqkBIO7vWk/2rNHXEhg5MxWtz+n7DNV9y5gRVHmUAq6ZNaPSqUWH6vguI+mKfo8VuSzyJ+Ir5/703jcFngo2erDh9p8KYjjsFfN/Zk6dfHDEg9EbEG5MsBBoH8Lwj1jXezNPbj6AXqY97zc6QNasH4bHR4mrgZSP1SKyENtLYGsAB1yRV37yIdbXE8wQYT6fd5cy2gcPUqKsHsp4jUn35V3KjoF/J++RwRU28Jfq1dx7/erWzEFg+zVxBsrbzmeGCWx4gyUBXW1ohfwtkQlG0l6GlJNArblAD9UKt6FHWwIzO9jByec8BtzvHAvbLI/QFQSWB+6+CDR0deofht8DZ0EnQIergRbCmSSjBrYb0aGND9o5/r+a1mKjf8s=

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

[Coq-Club] tests in plugins, Beta Ziliani, 04/26/2018
- Re: [Coq-Club] tests in plugins, Gaëtan Gilbert, 04/26/2018
  - Re: [Coq-Club] tests in plugins, Beta Ziliani, 04/27/2018
    - Re: [Coq-Club] tests in plugins, Gaëtan Gilbert, 04/27/2018
      - Re: [Coq-Club] tests in plugins, Gaëtan Gilbert, 04/27/2018
        
        Re: [Coq-Club] tests in plugins, Beta Ziliani, 04/27/2018