Coverage and executed code

Stream: lean4

[Yakov Pechersky]

I'd like to understand better the introspection of execution in lean4. Is it possible to write a "coverage" tool that, for a given target example and query source, indicates which lines in the source needed to be executed/elaborated for the example to elaborate/compile/execute properly?

[Yakov Pechersky]

Specifically, I am thinking of two applications. One is for coverage of code as it is tested. If I write some meta code for creating tactics, or elaborating expressions, I want to make sure that each line I've written is tested thoroughly, so that my implementation matches my imagined specification. And my "spec" is implemented through "empirical" example and "guard_hyp" tests, because I don't know how prove things about partial, meta, or elaboration code.

[Yakov Pechersky]

The other application is finding lines in tactic proofs that are, at easiest, as no-op for proving the goals at hand, and in general, not necessary for proving the goal.

[Henrik Böving]

Regarding partial code you cannot prove stuff about it, it is implemented as a constant + implementedBy an unsafe def, unfortunately I dont know how one would include a coverage tool though

[Yakov Pechersky]

Specifically for this question, I'm more interested in the meta code application

[Yakov Pechersky]

Precisely, since we are barred from proving about it, can we still have some diagnostic information of what branches were hit?

[Henrik Böving]

The internally generated definition is still very much accessible by meta code so I think it should be possible to analyze the internal definition yes. But I don't really know how one would implement coverage...to be honest I dont even know how coverage is implemented in any language.

[Yakov Pechersky]

One could rephrase any meta code in some sort of debug coverage monad, where each original line of code is instead written with a call to some "write" monadic op. And then when the function is executed, we can query the writer to see which lines were visited. However, that means all code that one wants to test for coverage must now be rewritten in this debug monad.

[Henrik Böving]

Eeeeh that sounds rather primitive, I'm sure there is some way to make it work without rewriting code we have right now.

[Yakov Pechersky]

Totally. I'm just first setting my "null model" expectation.

[Yakov Pechersky]

As in, it's "doable" if we restructure in undesired ways. Can it be done without that undesired restructure?

[Yakov Pechersky]

In python, the coverage tool works by attaching to the underlying code model tracer: https://docs.python.org/3/library/sys.html#sys.settrace. That is, _all_ python code does run in that "debug" writer monad, but usually the info is thrown away. And coverage retrieves that info.

[Yakov Pechersky]

I am not familiar with how rust or Haskell do it.