coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] tests in plugins

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] tests in plugins
Date: Thu, 26 Apr 2018 15:52:16 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay5-d.mail.gandi.net
Ironport-phdr: 9a23:eUa19xHf1U7P+eOALGplL51GYnF86YWxBRYc798ds5kLTJ7zpsSwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOhZtYb6u0cOogG4BQa0Be3vyztIiWTo0q0gz+QqDAbL3AM6EN0QrHTbttP1OL0dUeC0yKnH1ivMb+lK2Trm84jIcRAgoeqPXbJxdMrRzFcgFxnfglWWt4PlIyqY2+IQuGaV6OpgUPigi28hqwxprTivx9ssionUho0O0FzL6SJ5wIMzKNalS0B7ecapHIVNuyyYLYd7QN8uT3t1tCs5xLAKo4O3cSwIxZg/2hLSb/KKf5KI7x/sTuqcIzZ1iGh4dL++hxu/91WrxPfmWcmuyllKqzJIktnSuXAJ0Bze8tKHReV5/ki72TeC1xnf5fxeLUAxj6XbKpohzqQ/lpUJt0TMAy72lF/wjKCIakUo4umo6+L5bbX6vpKQKZJ4hwPkPqkshsCzG/k0PwsAUmSB5Oix0L/u8VX8QLpQj/02lqfZsIrdJcQevqO5DBVa3Zg/6xmlCTeqytsYnXgDLF1eZh2HlZTpNkrVIPD7Dfa/mFeskDZux/DDILLhGI/BLn7dn7f9Zbp98VJTyBIvzdBD4JJZEq0OIPXqWkPoqNPYCgI5PBevzub8CNR905seVniVDq+YNqPSq16I6fg1L+mCfo9G8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzDEwafXPqtfgAFW0HpBZ2GOPjhUGLV3hcZnK4Urggzio4GZmlDILGS5rrhrGdinToVqZKb3xLXwjfWUzjcJ+JDq9VOXCiZ/R5mzlBboCPDooo1BWgrgj/kuQ1NenF4S4ZsJfuzp5z6vGBzEhupwwxNNyU1iS2d08xhnkBHmFkx6Nuuk98z1KOy+5+juAKTYUOtcMMaR8zMNvn98I/C932XVicLM2ETF+3H5CqRzQ4T9Z3zNYIb0c7Hdi+3EjO

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