Zulip Chat Archive

Stream: general

Topic: leanchecker timeout


view this post on Zulip Yury G. Kudryashov (Apr 08 2021 at 19:24):

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

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 20:59):

@Gabriel Ebner @Mario Carneiro Ping here

view this post on Zulip Gabriel Ebner (Apr 12 2021 at 20:08):

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.

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 20:09):

Thanks a lot!

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:10):

How did you debug this?

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 20:12):

Leanchecker works

view this post on Zulip Gabriel Ebner (Apr 12 2021 at 20:16):

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.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:17):

You had to recompile lean to do that I guess?

view this post on Zulip Gabriel Ebner (Apr 12 2021 at 20:18):

Just leanchecker.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:18):

Isn't that the same code?

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:18):

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

view this post on Zulip Gabriel Ebner (Apr 12 2021 at 20:19):

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:21):

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:22):

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 20:23):

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


Last updated: May 10 2021 at 18:22 UTC