Rudi Grinberg (Aug 18 2020 at 20:24): Rudi Grinberg (Aug 18 2020 at 20:24):Dune 2.7.0 should be available in opam shortly. It contains a small improvement to setting flags globally for coq projects thanks to @gares. For coq itself, the new bisect support might be relevant. I don't how relevant coverage is going to be to coq, but it's always cool to look at.
More details here https://discuss.ocaml.org/t/ann-dune-2-7-0/6255
Karl Palmskog (Aug 18 2020 at 20:31):interesting, but I wonder how one would even define coverage in a Coq project (that doesn't use Quickchick and defines its coverage by Quickchick property checks). The best approximation to coverage presently is in my mind percent killed mutants out of all mutants in mutation analysis.
Rudi Grinberg (Aug 18 2020 at 20:32):Yeah, I meant coverage for the coq project itself and coq plugins when built with dune. Rather than coq projects. I also have no idea what's coverage in a coq project.
Karl Palmskog (Aug 18 2020 at 20:35):wait, so basically, you can see what [percent, etc.] code was recompiled by Dune after a diff?
Rudi Grinberg (Aug 18 2020 at 20:35):More like: you instrument coqc and then use it to build a project. Then you get to see which parts of coqc were actually executed (with frequency counts)
Karl Palmskog (Aug 18 2020 at 20:37):I see, and you get that for free? I think stats like that were discussed recently in a Coq issue, but for even finer granularity: https://github.com/coq/coq/pull/10652
Rudi Grinberg (Aug 18 2020 at 20:40):Not for free. The instrumented version of coq will be much slower.
Gaëtan Gilbert (Aug 18 2020 at 20:47):see also https://x80.org/coq-coverage/ (generated with adhoc build system changes IIUC, for stdlib + test suite)
Last updated: Apr 18 2024 at 04:02 UTC