rw is slow

Stream: general

[Kenny Lau]

set_option profiler true
theorem test_rw : true :=
begin
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, rw mul_add,
end

parsing took 5.08s
elaboration of test_rw took 211ms

[Kenny Lau]

I think this is the most shocking of all my test results

[Kenny Lau]

because rw is in core

[Mario Carneiro]

just because it's in core doesn't mean it's fast

[Mario Carneiro]

in fact that mostly means it hasn't been touched in a long time

[Kevin Buzzard]

parsing took 142ms

???

[Mario Carneiro]

but actually I think you are benchmarking have with these examples

[Mario Carneiro]

yeah, kenny's computer is weird

[Kevin Buzzard]

I can't believe my desktop is 40 times faster than it though

[Mario Carneiro]

I get 1.17 s

[Kenny Lau]

Mario Carneiro said:

but actually I think you are benchmarking have with these examples

this reminds me of the story of the man on the bike

[Kevin Buzzard]

Which version of Lean are you using?

[Mario Carneiro]

3.7.2

[Kevin Buzzard]

I'm on 3.8.0

[Kenny Lau]

a man on a bike would pass through a security guard on the border every week with a big bag of sand; every time the security would check the bag very carefully, but every time the security would find nothing; 2 years after the guard retired, he met the man by chance, and finally asks him: what were you smuggling the whole time?

it was the bikes

[Markus Himmel]

Okay, updating to 3.8 really made parsing 5 times faster on my machine

[Kenny Lau]

control:

set_option profiler true
theorem test_have : true :=
begin
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  have : 7 * (8 + 9) = 7 * 8 + 7 * 9, sorry,
  trivial
end

parsing took 445ms
elaboration of test_rw took 176ms

[Kenny Lau]

Markus Himmel said:

Okay, updating to 3.8 really made parsing 5 times faster on my machine

the problem is that codewars doesn't use 3.8

[Mario Carneiro]

Yep, I just updated and the test is much faster

[Kenny Lau]

codewars uses Lean 3.7.2

[Kenny Lau]

and @Markus Himmel managed to stay below the time limit

[Kenny Lau]

in Lean 3.7.2

[Patrick Massot]

Great! Could you please use all that speed to unstuck me on https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Bolzano-Weirstrass/near/193682245?

[Mario Carneiro]

I haven't been watching the changes carefully, @Gabriel Ebner @Bryan Gin-ge Chen any idea what the culprit is?

[Kevin Buzzard]

Patrick Massot said:

Great! Could you please use all that speed to unstuck me on https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Bolzano-Weirstrass/near/193682245?

?? I never even saw this!

You are not subscribed to stream Is there code for X?

[Kenny Lau]

and on codewars, which is the only benchmark that matters:

/workspace/src/Solution.lean:2:8
parsing took 1.18s

/workspace/src/Solution.lean:2:8
elaboration of test_rw took 87.7ms

[Kenny Lau]

so maybe I can still use rw in my solution

[Kevin Buzzard]

Oh wow and the coolest corollary of not being subscribed to the stream is that every time I reload it it comes up in a different colour!

[Gabriel Ebner]

Mario Carneiro said:

any idea what the culprit is?

What's the problem? I thought it is faster in Lean 3.8? (It should be even faster in Lean 3.9.)

[Mario Carneiro]

what changed?

[Mario Carneiro]

not a problem per se, I just don't like when things mysteriously get better

[Gabriel Ebner]

lean#180

[Gabriel Ebner]

Kenny complained, and I pushed a fix.

[Mario Carneiro]

oh right

[Mario Carneiro]

so this is used in the parsers for various tactics?

[Kevin Buzzard]

Mario did you see lean#186?

[Gabriel Ebner]

I guess this affects various things. All tactic parsers use reflect, and when the has_reflect instance is implemented using subst or expression quotations, then it will be magically faster now.

[Kenny Lau]

set_option profiler true
-- parsing took 2.07s
theorem test (H : true = true) : true :=
begin
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
  rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H, rw H,
end

[Kenny Lau]

control:

set_option profiler true
-- parsing took 1.24ms
theorem test (H : true = true) : true = true :=
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $
H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ H.trans $ rfl

[Kenny Lau]

so a difference of 2000x

[Kenny Lau]

faster when chained:

set_option profiler true
-- parsing took 38.9ms
theorem test (H : true = true) : true :=
begin
  rw [H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H,
      H, H, H, H, H, H, H, H, H, H],
end

[Alex J. Best]

Shouldn't the control be repeating some other tactic a bunch?

[Johan Commelin]

Of course rw is not exactly .trans. Maybe write a term-mode proof of

theorem test (H : true = true) (f : Prop -> Prop) : f true = f true :=

instead

[Johan Commelin]

What I'm mostly surprised by is the massive difference between the chained and unchained rw's

[Kevin Buzzard]

I've noticed this before. I tended not to chain rewrites until I realised it gave a speedup

[Kenny Lau]

brilliant

[Kenny Lau]

@Mario Carneiro is there some hidden bug in the parsing of rw that makes it slow? I remember @Markus Himmel telling me that split has a hidden bug

[Mario Carneiro]

As Alex says, try a control which uses lots of tactics, particularly ones without arguments like skip

[Kenny Lau]

set_option profiler true
-- parsing took 4.33ms
theorem test (H : true = true) : true :=
begin
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
  skip, skip, skip, skip, skip, skip, skip, skip, skip, skip,
end

[Mario Carneiro]

It's all argument parsing. Your first test is about 520 ms for me, and with

import tactic

namespace tactic
namespace interactive
setup_tactic_parser

meta def foo (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
skip
end interactive
end tactic

set_option profiler true
theorem test (H : true = true) : true :=
begin
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
  foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H, foo H,
end

it's about the same, while deleting the cfg argument drops it to 420 ms, deleting l drops to 300 ms, changing the q parser to (q : parse (rw_rule_p texpr)) drops to 240 ms, and (q : parse texpr) drops to 60 ms. As I said in another thread, parser combinators in lean are expensive because inlining sucks

[Kenny Lau]

thanks