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: Mon, 9 Jan 2017 11:02:49 +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:gTRPuRaHWp8SfAshNNtMUqb/LSx+4OfEezUN459isYplN5qZpsu4bnLW6fgltlLVR4KTs6sC0LuK9fq8EjReqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KZkMKc6zVP1q2BTeqwCyGVyJFmU2Qr1/dyx1J9l6SVZ/fw7oZ0TGZ7mdrg1GOQLRA8tNHo4sZXm

On Mon, Jan 09, 2017 at 10:43:52AM +0100, Ralf Jung wrote:
> All right. I'll first follow up in the aforementioned bugreport, as
> that's a prerequisite (and would be helpful otherwise).
> Does "make vio2vo incremental and make it call 'make quick'" also need a
> CEP, or just a PR?

For the specific change you propose, I think a PR on coq_makefile2 is
enough (there is little to design, it is a bugfix to me).

I mentioned the CEP because, given I'm rewriting coq_makefile, if people
have a lot of feature wishes (i.e. support for a particular workflow)
it is better to collect them in a single place.

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