Zulip Chat Archive

Stream: general

Topic: leanchecker timeout

Yury G. Kudryashov (Apr 08 2021 at 19:24):

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

Yury G. Kudryashov (Apr 09 2021 at 20:59):

@Gabriel Ebner @Mario Carneiro Ping here

Gabriel Ebner (Apr 12 2021 at 20:08):

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 (Apr 12 2021 at 20:09):

Thanks a lot!

Mario Carneiro (Apr 12 2021 at 20:10):

How did you debug this?

Yury G. Kudryashov (Apr 12 2021 at 20:12):

Leanchecker works

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.

Mario Carneiro (Apr 12 2021 at 20:17):

You had to recompile lean to do that I guess?

Gabriel Ebner (Apr 12 2021 at 20:18):

Just leanchecker.

Mario Carneiro (Apr 12 2021 at 20:18):

Isn't that the same code?

Mario Carneiro (Apr 12 2021 at 20:18):

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

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).

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

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

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: Aug 03 2023 at 10:10 UTC