Deterministic timeout debugging

Stream: general

[Geoffrey Irving]

After upgrading mathlib I'm getting a lot of deterministic timeouts, and I am not sure how to debug them (the profiler was uninformative). Here's one self-contained file example. I wouldn't call it a minimal example, but minimizing deterministic timeouts is hard since they are fragile. I am on Lean (version 3.50.3, Release), Mathlib 44b58b42794e5abe2bf86397c38e26b587e07e59.

bug.lean

[Geoffrey Irving]

Hmm, unfortunately that deterministic timeout happens in VSCode but doesn't happen if I do lean --make bug.lean. :/

[Martin Dvořák]

Been there.

[Geoffrey Irving]

In VSCode my "Lean: Time Limit" is 100000. Is the command line default different?

[Mauricio Collares]

Pass -T100000 as an argument to replicate the VSCode behavior. I don't know the default limit, though.

[Geoffrey Irving]

Thanks, now command line agrees:

% lean --make bug.lean -T100000
/Users/geoffreyi/ray/src/bug.lean:51:0: error: (deterministic) timeout
/Users/geoffreyi/ray/src/bug.lean:27:0: error: (deterministic) timeout

[Geoffrey Irving]

Here's a smaller timeout example. Of course the circle_integral import is unnecessary, but importing just what I need fixes the timeout.

import measure_theory.integral.circle_integral
open complex (abs)
open_locale real

-- Given z ≠ 0, we can find a slightly smaller nearby w
lemma slightly_smaller {z : ℂ} (nz : z ≠ 0) {r : ℝ} : r > 0 → ∃ w, abs (w - z) < r ∧ abs w < abs z :=
begin
  intro rp,
  by_cases rz : r > abs z, {
    use 0, simp, finish,
  },
  simp at rz,
  have azp : abs z > 0 := complex.abs.pos nz,
  generalize ha : 1 - r / 2 / abs z = a,
  have a0 : a ≥ 0, {
    rw ←ha, refine sub_nonneg.mpr ((div_le_one azp).mpr _),
    transitivity r,
    sorry,
    assumption,
  },
  have a1 : a < 1, { rw ←ha, simp, positivity },
  generalize hw : ↑a * z = w,
  use w, constructor, {
    rw [←hw,←ha], simp, rw mul_sub_right_distrib, simp,
    rw abs_of_pos rp, field_simp [ne_of_gt azp],
    simp,
  }, {
    sorry
  },
end

[Geoffrey Irving]

A bit smaller:

import measure_theory.integral.circle_integral
open complex (abs)
open_locale real

-- Given z ≠ 0, we can find a slightly smaller nearby w
lemma slightly_smaller {z : ℂ} (nz : z ≠ 0) {r : ℝ} (rp : r > 0) : ∃ w, abs (w - z) < r ∧ abs w < abs z :=
begin
  by_cases rz : r > abs z, {
    use 0, simp, finish,
  },
  simp at rz,
  have azp : abs z > 0 := sorry,
  generalize ha : 1 - r / 2 / abs z = a,
  use ↑a * z, constructor, {
    rw [←ha], simp, rw mul_sub_right_distrib, simp,
    rw abs_of_pos rp, field_simp [ne_of_gt azp],
    simp,
  },
end

[Kevin Buzzard]

Fix up your non-terminal simps. Lean is spending ages trying to close a goal with simp and the more you import the more ways there are to fail. Non-terminal simps are a code smell as you are discovering

[Kevin Buzzard]

Squeeze them with squeeze_simp. Non-terminal simp onlys are fine.

[Junyan Xu]

When I try to fix up a file with lots of slow proofs such as in #18018, I'd put set_option profiler true at the top of the file, then as Lean compiles the file, elaboration time and other info will show up in the right panel (infoview). I'd copy that to a file and search for elaboration of and see which ones are particularly slow.

The fix is usually just replace simp by simp only. If you're unsure which part is slow, try replacing { ... } blocks by sorry { ... } and see which makes elaboration a lot faster. You can also insert sorry anywhere to check if the part above the sorry elaborates fast enough. (You may need multiple sorries if there are multiple goals, though.)

[Junyan Xu]

You can also replace all simp by squeeze_simp and come back after a while, and the simp only suggestions will all show up in the infoview, and you can copy them elsewhere and apply them individually. (If you click on the suggestion to apply it, the other suggestions will go away, which isn't nice. Maybe you can click on the "pause" button to freeze the infoview, but I haven't tried.) Since squeeze_simp is even slower than simp, you may need to increase the timeout limit (search for setting "Lean: Time Limit" in VSCode). As I'm writing this, I realize you can probably just replace simp by squeeze_simp, save the file, and then lean --make -T1000000.

[Geoffrey Irving]

Thank you! The squeeze_simp → simp only route works very well!

[Kevin Buzzard]

finish is even worse than simp!

import measure_theory.integral.circle_integral
open complex (abs)
open_locale real

set_option profiler true
-- Given z ≠ 0, we can find a slightly smaller nearby w
lemma slightly_smaller {z : ℂ} (nz : z ≠ 0) {r : ℝ} (rp : r > 0) : ∃ w, abs (w - z) < r ∧ abs w < abs z :=
begin
  by_cases rz : r > abs z, {
    use 0, simp, finish,
  },
  sorry end

-- elaboration of slightly_smaller took 4.13s

[Kevin Buzzard]

import measure_theory.integral.circle_integral
open complex (abs)
open_locale real

set_option profiler true
-- I changed r > 0 to 0 < r and r > abs z to abs z < r; we prefer < to > in mathlib
-- Given z ≠ 0, we can find a slightly smaller nearby w
lemma slightly_smaller {z : ℂ} (nz : z ≠ 0) {r : ℝ} (rp : 0 < r) : ∃ w, abs (w - z) < r ∧ abs w < abs z :=
begin
  by_cases rz : abs z < r, {
    use 0,
    split,
    { simp only [rz, zero_sub, absolute_value.map_neg], },
    { simp only [nz, absolute_value.pos_iff, ne.def, not_false_iff, absolute_value.map_zero], },
  },
  sorry end

-- 310ms = factor of > ten speedup