leanchecker timeout

Stream: general

[Yury G. Kudryashov]

Hi, something in #7124 causes a leanchecker timeout. How can I debug/fix it?

[Yury G. Kudryashov]

@Gabriel Ebner @Mario Carneiro Ping here

[Gabriel Ebner]

pong
The problem was that a proof for unique_diff_on (for the pi instance which uses the L^∞ norm) was used for unique_diff_on (for the pi_Lp instance using the L^2 norm). It turns that unique_diff_on doesn't actually depend on the norm (only the topology) even though it takes normed_space argument, so this type-checks after a lot of unfolding. Generalizing unique_diff_on from normed spaces to semimodules that are also topological spaces gets rid of the unfolding. I've also made unique_diff_within_at a structure to prevent unfolding.

[Yury G. Kudryashov]

Thanks a lot!

[Mario Carneiro]

How did you debug this?

[Yury G. Kudryashov]

Leanchecker works

[Gabriel Ebner]

I added print statements to leanchecker so that I could see where it hanged. This way I could identify model_with_corners_euclidean_half_space._proof_7 as the culprit. Running leanchecker in gdb showed that it was normalizing list.map ... nnnorm .... which looks like the norm on fin n → ℝ.
From there it was natural to prevent reduction of some complicated definition. After turning unique_diff_within_at into a structure, the two manifold definitions broke because of the mismatch between the normed_space instances. The rest was just figuring out why it should actually work, and adjusting the type class parameters to unique_diff_within_at accordingly.

[Mario Carneiro]

You had to recompile lean to do that I guess?

[Gabriel Ebner]

Just leanchecker.

[Mario Carneiro]

Isn't that the same code?

[Mario Carneiro]

Is it possible to put the print statements behind a CLI flag?

[Gabriel Ebner]

It is in the same repository, but it only depends on the kernel (not the tactics, not the vm, not even the type context).

[Mario Carneiro]

Something like leanchecker -v to print all the theorems, and then leanchecker -vv model_with_corners_euclidean_half_space._proof_7 to print normalization steps would be awesome

[Mario Carneiro]

my main worry is that for the latter, it can't be compiled out since the CLI flag is a runtime thing so it might be a performance regression

[Mario Carneiro]

Ah, actually I guess it can be behind a compile time setting that is true for leanchecker and false for lean