Zulip Chat Archive

Stream: lean4

Topic: Coverage and executed code


Yakov Pechersky (Feb 06 2022 at 14:29):

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 (Feb 06 2022 at 14:32):

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 (Feb 06 2022 at 14:33):

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 (Feb 06 2022 at 14:34):

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 (Feb 06 2022 at 14:34):

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

Yakov Pechersky (Feb 06 2022 at 14:35):

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

Henrik Böving (Feb 06 2022 at 14:37):

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 (Feb 06 2022 at 14:38):

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 (Feb 06 2022 at 14:38):

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 (Feb 06 2022 at 14:39):

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

Yakov Pechersky (Feb 06 2022 at 14:40):

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

Yakov Pechersky (Feb 06 2022 at 14:44):

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 (Feb 06 2022 at 14:45):

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


Last updated: Dec 20 2023 at 11:08 UTC