Please make Dune aware of `-inlining-report`

[ejgallego]

Dear Dune devs,

some OCaml flags such as -inlining-report will generate extra development files, however, as noted in rocq-prover/rocq#8651 , Dune is not aware of the extra targets thus some problems may occur, in particular, deleting the reports on a rebuild.

Please make Dune aware of this option and similar ones.

[rgrinberg]

I wonder if it's just simpler to turn off dune's automatic cleaning. There's quite a few of these options, and it doesn't seem all that practical to keep track of all of them.

[ejgallego]

That indeed would also work I think.

we do need to clean stale cmi files to avoid problems. However, we could limit cleaning to things that used to be targets but no longer are

[ejgallego]

I guess that the solution with the less implementation overhead should do the trick. This is after all a very specific developer-only need, to inspect the debug info of the compiler.

[cpitclaudel]

@ejgallego Although as you pointed in a recent discussion, this corresponds to the case of extraction from Coq modules, too: compiling a .v to .vo can create extracted OCaml files, and Dune will then delete them between runs.

I wonder if a general solution for this would be to add a stanza to register additional outputs of a rule, so that I could say "compiling x.v also produces x_extraction.ml" and "compiling xyz.ml also produces xyz.0.inlining.org, xyz.1.inlining.org, xyz.2.inlining.org, etc.".

[rgrinberg]

I wonder if a general solution for this would be to add a stanza to register additional outputs of a rule,

The difficulty here is to have a way to select the rule  for which the targets need to be adjusted. If possible, I think it would be simpler if normal coq libraries did no extraction and all the extraction was done through a separate stanza.

…

On Nov 1, 2019, 10:31 PM +0900, Clément Pit-Claudel ***@***.***>, wrote: @ejgallego Although as you pointed in a recent discussion, this corresponds to the case of extraction from Coq modules, too: compiling a .v to .vo can create extracted OCaml files, and Dune will then delete them between runs. I wonder if a general solution for this would be to add a stanza to register additional outputs of a rule, so that I could say "compiling x.v also produces x_extraction.ml" and "compiling xyz.ml also produces xyz.0.inlining.org, xyz.1.inlining.org, xyz.2.inlining.org, etc.". — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe.

[cpitclaudel]

The difficulty here is to have a way to select the rule for which the targets need to be adjusted. If possible, I think it would be simpler if normal coq libraries did no extraction and all the extraction was done through a separate stanza.

I doubt that's possible, since there's such a broad variety of extraction commands — especially given how stateful the whole thing is (you'd have to attach the extraction commands to a particular file, since each coq file can set stateful options that affect extraction)

[rgrinberg]

I see. Although I think that commands that modify how extraction works shouldn’t pose a problem. The only commands that are problematic to dune are those that somehow change the set of file targets extraction produces. Those are the only ones that I advocate be separated from coq libraries. Of course, I’m quite optimistic because I have very little idea how coq works :)

…

On Nov 1, 2019 23:12 +0900, ocaml/dune ***@***.***>, wrote: I doubt that's possible, since there's such a broad variety of extraction commands — especially given how stateful the whole thing is (you'd have to attach the extraction commands to a particular file, since each coq file can set stateful options that affect extraction)

[cpitclaudel]

I see. Although I think that commands that modify how extraction works shouldn’t pose a problem.

That could be true :) Being able to say something like "run this extraction command after processing this specific file" would work, but at that point it might be just as simple to embed the command inside of the Coq file (and it makes dune's job easier, since it doesn't have to learn about the various forms of extraction that Coq supports).

[ejgallego]

This could maybe be an use case for the instrumentation framework #3526 ?