Stream: Dune devs & users

Topic: Dune 2.7.0


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Aug 18 2020 at 20:40):

Not for free. The instrumented version of coq will be much slower.

view this post on Zulip 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: Oct 16 2021 at 09:07 UTC