coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] sound incremental builds

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] sound incremental builds
Date: Mon, 20 Jul 2020 08:56:32 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f44.google.com
Ironport-phdr: 9a23:+ljiKRTs6Fb+1sjg1/bUiqTkzdpsv+yvbD5Q0YIujvd0So/mwa6zYBSN2/xhgRfzUJnB7Loc0qyK6v6mBTBLv8bJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/eu8QZjodvK6U8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9Drx2hqR5wzY7abo+WKfRwYL/ScMgASmZdRMtcTTBNDp++YoYJEuEPPfxYr474p1YWsRaxHgmsBOL0yj9ImHD23rAx3vgnEQ7c2gwvAs8FvXPOo9ruNKcSUPu1zKnWwjXAdf9ZwzH955LOch88u/2MXLNwcdbeyUQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhGEptxt/rSKzxscwlIbJnIQVx0jA+Ch53Io4O8O0RkB1bNCkEZZcqT2WO5Z2TM0iQ29kpig3x6EatJO1YSQH1YoryhzDZvGbcoWG7R3uWeaMLDp5gn9uZbyxhxG38Ue6y+38UNG530pNripflNnDqHQN1xjJ5seZV/R940Gs0iuM2QDL8uxIP1w4mK7BJ5MiwrM8jIcfvEXCEyPsl0j7g6mbfVg+9Oey8eToeLDmq4ecN4BqjgH+NbwjmsmlDuQ5NggCRmmb+eOh2LH68030T7pHguc5kqnet5DaKsAbqbCjDwBJ1YYj7g6zDzag0NsGgXkKNExJdA6DgoTzOFzDIOr0Aeq+jlmtijtmyP/LMqXkAprXL3jDlLnhfax6605Z0Ac818tQ55JVCrEaIPL8REzxuMbCAR8/KQO0xfvoBM981oMfRWKPDbSUMKzXsVCS5+IvJ/OAa5MSuDb4M/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1ZWL3CagHpBVLklAA1aAWSPhfYWFQPcBa2SbJMZnnnoFVKSuY4Ak3BCq8gT9zuwjZuHT42gTsY/pnIx+4PSWnhUv/xR1Cd6c2ieDVTcnsHkPQmof1qB+ukxwyR+q16F+j7QMHNZT5uhJXwR8PJjVyeA8CtHuVSrOe96ITBCtRdDwUmJ5dc4439JbOxU1IN6llB2Wh3P2UY9QrKSCAdkPyoyZx2L4fp8vxHPP1a1nhF4jEJMWZD+Ww5Vn/g2WPLbn1kCQlqKkb6MZhXef+2KKzG7It0ZdAlcpDPf1GEsHb06TluzXo0PPS7j0VOYiOwpFjM+Fc+5ENoGvglJBS/Puft/ZZjDplg==

I hear the word dune thrown around at every build problem. Is there some place where this Dune's Coq support is explained, especially what it guarantees?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Jul 20, 2020 at 8:51 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Hi Abhishek,

Abhishek Anand <abhishek.anand.iitg AT gmail.com> writes:

> I want to avoid ever having to do clean builds (`make clean`) and
> still ensure soundness of the build.

Modulo bugs, Dune's Coq support will do what you want.

Kind regards,
E.

[Coq-Club] sound incremental builds, Abhishek Anand, 07/18/2020
- Re: [Coq-Club] sound incremental builds, David Holland, 07/19/2020
- Re: [Coq-Club] sound incremental builds, jonikelee AT gmail.com, 07/19/2020
- Re: [Coq-Club] sound incremental builds, Emilio Jesús Gallego Arias, 07/20/2020
  - Re: [Coq-Club] sound incremental builds, Abhishek Anand, 07/20/2020
    - Re: [Coq-Club] sound incremental builds, Emilio Jesús Gallego Arias, 07/20/2020