BreakOut 2020 12 03 Paolo

Question 1: better rule parallelism for generated .v files

present: Emilio, Paolo

• a rule can be seen as an arrow: {dep} -[action]-> {targets}

Examples:

• { foo.cpp } -[tool] -> {foo.v,foo_names.v}
• { foo.v } -[coqc]-> { foo.vo }
• { foo_proof.v } -[coqc]-> ...
• { bar_proof.v } -[coqc]-> ...

We'd like a more parallel graph, however coqdep requires the generation of all .v files before it can be called.

Solutions:

1.- modify Coq / coqdep to have a mode similar to ocamldep -modules A first version is implemented by using coqdep's Abshishek's patch, see https://github.com/coq/coq/pull/12108 2.- existing workaround with dune: split projects into (coq.theory ...) in such a way that there is parallelism as Dune handles coqdep invocations per-theory; for {a,b}.cpp do:

(coq.theory
 (name a))

(coq.theory
 (name b))

Discussion about option 1.

We agree that https://github.com/coq/coq/pull/12108 can be merged, improving the specification and adding a few extra checks.

Question 2: Dune inter-scope composition

When is interscope composition going to be ready? Emilio says as soon as possible, absolutely top priority.

opam pin add dune

should work for testing once the branch is ready

Question 3:

How to add custom rules to dune?

There are 2 approaches:

• Use the OCaml API
• Generate Dune files

Notes:

• Other users of code generation https://github.com/coq-community/coqffi
• dune plugins are >= 1 year away, that needs a stable dune API, and maybe a change on the configuration language, discussion is ongoing Dune upstream
• dune is well-funded and maintained
• Dune 3 should make dune file generation much better, as it can be done by regular rules