coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- 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
- Re: [Coq-Club] tests in plugins, Gaëtan Gilbert, 04/26/2018
Archive powered by MHonArc 2.6.18.