Support Rocq timing outputs

[SkySkimmer]

Rocq can produce per-command timing info with command line -time-file foo.timing, and more complex profiles with profile foo.json (NB: json profiles benefit from being gzipped after they're produced to reduce space consumption).

Makefiles produced by rocq makefile automatically enables these when env vars TIMING and PROFILING are set respectively (the profile output also depends on ROCQ_PROFILE_COMPONENTS and COQ_PROFILE_COMPONENTS).

Additionally env var TIMED makes make produce per-file timing info in the build log (using time -f "$@ (real: %e, user: %U, sys: %S, mem: %M ko)" rocq compile ...).

These outputs can be processed by some rocq tools. This is done automatically in rocq's benchmarking script.

Currently dune doesn't produce these outputs, so benchmarking projects using dune is missing a lot of data.

Can we get dune to produce these things?

Changing the interface to make it easier or nicer is possible, but for the sake of rocq's benchmarking it should be possible to globally enable (currently done by exporting the env vars, but we could also modify the global dune config or whatever).

[SkySkimmer]

This issue was originally opened on the rocq repo by mistake. There:

@ejgallego said rocq-prover/rocq#20401 (comment)

Thanks @SkySkimmer , I was thinking this issue to be done in the Dune repository, as it is really a feature request for Dune.

I think .timing vs .json files are separate issues, and with different feature sets. I'll comment on them separatedly:

Handling .timing files

This should be easy, we just need to decide on the best interface. Usually using a dune-workspace file as done for coverage could work, but there are other options. This option is friendly for people developing, but I am not sure it works fine for OPAM-based setup, as there we cannot access a "global dune config file"

Using an env var could work but it could have an overhead, need to check at what level the dependency on the env var can be injected.

Handling .json catapult traces and TIMED

Dune can already produce the information that TIMED produces, IAANM, see --trace-file and --trace-extended options.

It'd be nice to integrate that with the profiler components, see rocq-prover/rocq#11542 but it would require a bit of work on Dune itself.

Important differences in the way we propose to handle .timing files vs .json catapult files.

In particular, for .timing files, they would be considered a real result of the build system, so indeed, when a rule is cached, you'd recover the original timing and you wouldn't observe the cache hit.

On the other hand, --trace-file works at a global build level, so indeed you can observe cache hits, etc... debug different machines and understand the "real time" of your incremental build better, in particular you can analyze dependency hotspots.

Both systems cover different use cases, so indeed, YMMV. For example, in coq-lsp, when we retrieve cached data, we make available the original timings, but we also expose a flag that indicates if the timing was retrieved from the cache or not.

[SkySkimmer]

and @ejgallego said rocq-prover/rocq#20401 (comment)

More notes on possible interfaces:

• use an env var: we can try to make the part that generates the flags to depend on a variable, this way we inject one dep edge per theory, I think that should be OK
• allow users to insert -time in flags, parse flags and detect that. Flags in dune files can be controlled by using (include ) and a configure script
• use a dune-workspace file: this is the most logical place, however not sure how to make OPAM use a custom one.

More of a medium term project, but would be nice to move bench from opam, a few issues used to exists about it in the old repos. (Maybe the new dune package management features could work here, not sure)