## Stream: general

### Topic: rw is slow

#### Kenny Lau (Apr 12 2020 at 09:07):

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 (Apr 12 2020 at 09:07):

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

#### Kenny Lau (Apr 12 2020 at 09:08):

because rw is in core

#### Mario Carneiro (Apr 12 2020 at 09:08):

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

#### Mario Carneiro (Apr 12 2020 at 09:08):

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

#### Kevin Buzzard (Apr 12 2020 at 09:08):

parsing took 142ms


???

#### Mario Carneiro (Apr 12 2020 at 09:09):

but actually I think you are benchmarking have with these examples

#### Mario Carneiro (Apr 12 2020 at 09:09):

yeah, kenny's computer is weird

#### Kevin Buzzard (Apr 12 2020 at 09:09):

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

I get 1.17 s

#### Kenny Lau (Apr 12 2020 at 09:09):

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

Which version of Lean are you using?

3.7.2

I'm on 3.8.0

#### Kenny Lau (Apr 12 2020 at 09:10):

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

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

#### Kenny Lau (Apr 12 2020 at 09:12):

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

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 (Apr 12 2020 at 09:13):

Yep, I just updated and the test is much faster

#### Kenny Lau (Apr 12 2020 at 09:14):

codewars uses Lean 3.7.2

#### Kenny Lau (Apr 12 2020 at 09:14):

and @Markus Himmel managed to stay below the time limit

in Lean 3.7.2

#### Patrick Massot (Apr 12 2020 at 09:14):

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 (Apr 12 2020 at 09:15):

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

#### Kevin Buzzard (Apr 12 2020 at 09:16):

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 (Apr 12 2020 at 09:17):

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 (Apr 12 2020 at 09:17):

so maybe I can still use rw in my solution

#### Kevin Buzzard (Apr 12 2020 at 09:17):

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 (Apr 12 2020 at 09:26):

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

what changed?

#### Mario Carneiro (Apr 12 2020 at 09:27):

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

lean#180

#### Gabriel Ebner (Apr 12 2020 at 09:28):

Kenny complained, and I pushed a fix.

oh right

#### Mario Carneiro (Apr 12 2020 at 09:28):

so this is used in the parsers for various tactics?

#### Kevin Buzzard (Apr 12 2020 at 09:29):

Mario did you see lean#186?

#### Gabriel Ebner (Apr 12 2020 at 09:30):

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 (Jul 29 2020 at 02:37):

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 (Jul 29 2020 at 02:39):

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 (Jul 29 2020 at 02:39):

so a difference of 2000x

#### Kenny Lau (Jul 29 2020 at 02:43):

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 (Jul 29 2020 at 03:16):

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

#### Johan Commelin (Jul 29 2020 at 04:30):

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 :=


#### Johan Commelin (Jul 29 2020 at 04:30):

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

#### Kevin Buzzard (Jul 29 2020 at 07:12):

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

brilliant

#### Kenny Lau (Jul 29 2020 at 07:47):

@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 (Jul 29 2020 at 07:55):

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

#### Kenny Lau (Jul 29 2020 at 08:05):

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 (Jul 29 2020 at 08:06):

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 (Jul 29 2020 at 08:33):

thanks

Last updated: May 16 2021 at 05:21 UTC