coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] incremental vio2vo

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] incremental vio2vo
Date: Sun, 8 Jan 2017 18:42:47 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:M/+BHxeo/R7o2rid3GvPMa8PlGMj4u6mDksu8pMizoh2WeGdxc29Zx7h7PlgxGXEQZ/co6odzbGH7+a6AidZucrJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43B6AryxDO6kdBYP9XjTdlI0iSlBG6+s6r559L8iJKuvtn+dQWAvayRLgxUbENVGduCGsy/sC+7RQ=

On Fri, Jan 06, 2017 at 09:19:10PM +0100, Ralf Jung wrote:
> However, I don't know very much about the internals of the vio2vo
> machinery, so I'm not entirely sure if this approach even makes sense.
> Can this cause trouble by mixing vo files from different "runs" of
> vio2vo? Is there any good reason "make vio2vo" is *not* incremental?

There is no real good reason, it is just that when I added the target I
could not understand coq_makefile well enough to code something smarter.

Last week I started to rewrite coq_makefile, and now I think it is much
easier to understand what it does and extend it. See

https://github.com/gares/coq/tree/feature/coq_makefile2

and in particular tools/CoqMakefile.in that is where your patch could
land. PR welcome ;-)

Best,
--
Enrico Tassi

[Coq-Club] incremental vio2vo, Ralf Jung, 01/06/2017
- Re: [Coq-Club] incremental vio2vo, Enrico Tassi, 01/08/2017
  - Re: [Coq-Club] incremental vio2vo, Ralf Jung, 01/08/2017
    - Re: [Coq-Club] incremental vio2vo, Enrico Tassi, 01/09/2017
      - Re: [Coq-Club] incremental vio2vo, Ralf Jung, 01/09/2017
        
        Re: [Coq-Club] incremental vio2vo, Enrico Tassi, 01/09/2017