Zulip Chat Archive

Stream: general

Topic: rw is slow


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:07):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:08):

because rw is in core

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:08):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:08):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 09:08):

parsing took 142ms

???

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:09):

but actually I think you are benchmarking have with these examples

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:09):

yeah, kenny's computer is weird

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 09:09):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:09):

I get 1.17 s

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 09:09):

Which version of Lean are you using?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:10):

3.7.2

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 09:10):

I'm on 3.8.0

view this post on Zulip 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

view this post on Zulip Markus Himmel (Apr 12 2020 at 09:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:13):

Yep, I just updated and the test is much faster

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:14):

codewars uses Lean 3.7.2

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:14):

and @Markus Himmel managed to stay below the time limit

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:14):

in Lean 3.7.2

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 12 2020 at 09:17):

so maybe I can still use rw in my solution

view this post on Zulip 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!

view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:27):

what changed?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:27):

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

view this post on Zulip Gabriel Ebner (Apr 12 2020 at 09:27):

lean#180

view this post on Zulip Gabriel Ebner (Apr 12 2020 at 09:28):

Kenny complained, and I pushed a fix.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:28):

oh right

view this post on Zulip Mario Carneiro (Apr 12 2020 at 09:28):

so this is used in the parsers for various tactics?

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 09:29):

Mario did you see lean#186?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 29 2020 at 02:39):

so a difference of 2000x

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jul 29 2020 at 03:16):

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

view this post on Zulip 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 :=

instead

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:36):

brilliant

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 29 2020 at 08:33):

thanks


Last updated: May 16 2021 at 05:21 UTC