norm_num is slow

Stream: general

[Kenny Lau]

import tactic

set_option profiler true

theorem test_norm_num : true :=
begin
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
  have : nat.prime 13 := by norm_num,
end

parsing took 1.41s
elaboration of test_norm_num took 2.99s

[Kenny Lau]

for comparison:

import tactic

set_option profiler true

theorem test_ring : true :=
begin
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  have : ∀ n : ℤ, (n+1)^2=n^2+2*n+1 := λ n, by ring,
  trivial
end

parsing took 1.09s
elaboration of test_ring took 2.41s

[Kenny Lau]

so ok let's say norm_num is an expensive tactic

[Kenny Lau]

but somehow it takes longer to parse than ring

[Mario Carneiro]

You can do better if you don't jump in and out of tactic mode so much

[Kenny Lau]

oh, I never knew that

[Mario Carneiro]

repeating have : nat.prime 13, norm_num, has much better parsing performance for me

[Kenny Lau]

because I sometimes use rw show foo = bar, by norm_num

[Mario Carneiro]

It has to create a new context and run the tactic, get the result, and return to the original context

[Kevin Buzzard]

Are there some tips here? I do just the same as Kenny

[Kenny Lau]

import tactic

set_option profiler true

theorem test_norm_num : true :=
begin
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  have : nat.prime 13, norm_num,
  trivial
end

parsing took 1.42s
elaboration of test_norm_num took 2.47s

[Kenny Lau]

looks like it's the same

[Mario Carneiro]

I get a lot more reports with many uses of by

[Mario Carneiro]

that might be contributing to the timing

[Kenny Lau]

so what should we write instead of rw show foo = bar, by norm_num?

[Mario Carneiro]

have foo = bar, {norm_num}, rw this

[Mario Carneiro]

but this seems like hair splitting level optimization

[Kenny Lau]

I think we can move on to another thread, because: