The Coq mailing list

[Rudi Grinberg <rudi.grinberg AT gmail.com>]

Dune never executes build rules eagerly. It only executes them when the targets of a rule are needed as dependencies of another rule, or the user requested them to be built.

Regarding coqdep, the coqdep rule for a theory in dune depends on all .v files for that theory. So indeed the behavior should be like coq_makefile’s.

On Aug 31, 2020, 11:44 AM -0700, Abhishek Anand <abhishek.anand.iitg AT gmail.com>, wrote:

would dune then eagerly invoke cpp2v on everything before building even 1 .vo file? coq_makefile's Makefile builds all .v files before invoking coqdep, which makes sense given the current implementation of coqdep.

-- Abhishek

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

On Mon, Aug 31, 2020 at 11:40 AM Rudi Grinberg <rudi.grinberg AT gmail.com> wrote:

I think you’re looking for a rule like this:

(rule
 (deps foo.v)
 (targets foo.cpp)
 (action (cpp2v %{deps} -o %{targets)))

Usually, there’s a straightforward way to port any make rule to a dune rule. Sometimes this will require writing a lot more boilerplate, but it should be doable.

On Aug 31, 2020, 10:22 AM -0700, Gregory Malecha <gregory AT bedrocksystems.com>, wrote:

Does dune have a way to run pre-processors? For example, we have a tool, cpp2v, that takes a C++ file and generates a Coq file. I haven't found a way to get dune to do this for me.

On Sat, Aug 29, 2020 at 5:50 AM Théo Zimmermann <theo AT irif.fr> wrote:

Dear Abhishek,

If you are looking for a way to get away from the limitations of make,
why not try the experimental Dune support for Coq instead?

See:
- https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-dune
- https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
- https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20

Cheers,
Théo

Le jeu. 20 août 2020 à 21:37, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> Has someone written a tool to produce scons declarations (SConstruct) from a _CoqProject?
> I find it advantageous over make, especially in cross-server CI settings, because it uses hashes instead of timestamps to decide whether to rebuild a .vo file.

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING