coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Beta Ziliani <beta AT mpi-sws.org>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] tests in plugins
- Date: Fri, 27 Apr 2018 11:59:19 -0300
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
- Ironport-phdr: 9a23:LLZKJx9Bssjbq/9uRHKM819IXTAuvvDOBiVQ1KB42u8cTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsYSmpPXshfWS9PDJ6iYYQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33vk/HgHaxgMrAtEBsHXQrNX0LqgSV+G1x7TPwDrYcfxWxS3y5ZPNchA5oPGARKlwcMTKyUU1EAPFlFqQpJXjMjiI2OoNtG2b4PBhVeKpk2Mnrh9+oiK1yscqlIbJmpoZyl/F9SVlwIY1OMa3RFRnbt6jFZtdsTyROYhuQs46Xm1ltiI3xqcbtZO/ZiQHy5UqywTQZvCba4SE/A7vWeKLLTp7hH9pYqyziwu9/ES6xeDwS8+520tQoCVfiNnDrHUN2gTT6seZTvt9+V+s2TSS1wDV7eFIO0U0lbLaK5I4wb4wkoETvl/ZEi/zgEX2g7WaeVg69eSw6uTnZKvppoOEOoNphAzzNr4iltG7DOgiMQUDXnKX9Oug2LH7+E32WrRKjvk4kqnDt5DaINwWqbWnDA9JyIku8BO/Dy+n0NgBhnkGIklFdAiAj4jzNFHCOOr4Auung1SwjDdrwOjLMaHmApXUN3TMjLPhfatm5ENH0woyzdVf54pOBb0bIfLzXFXxtN3CARMjPQy02bWvNNIo/YQHEUmLH6XRZKjVqBqD4v8lC+iKfo4c/jjnfasL/fnr2FU0hVZVT6it3JIRaTjsFPl6Km2ceXupmcgaV2AQsVxtH6TRlFSeXGsLND6JVKUm62R+Udr+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFC6zJYCcWrIXdznUJdVuwGVdCeqRDrQ53BTrjzfUjqJ9J7OPqCgAtNf4y8Mz4Pfcx0lrqG5ESv+F2mTIdFla22MFQzhshvJ9vEp6jFKb0O17h+dSU9lL6LVFX1ViOA==
\o/
Many many thanks Gaëtan!What it isn't doing is selecting just the tests that depends on particular (modified) .v file in theories, so it just recompiles everything, even tests without requiring said theory file. But it is good enough for me as is.
On Fri, Apr 27, 2018 at 11:50 AM, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:
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>
- [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.