Zulip Chat Archive
Stream: general
Topic: efficiency
Scott Morrison (Nov 13 2018 at 05:04):
Hi @Mario Carneiro, @Keeley Hoek and I are having some "fun" profiling rewrite_search, and discovered that all the arithmetic is slow.
Mario Carneiro (Nov 13 2018 at 05:05):
don't generate proofs during the search
Scott Morrison (Nov 13 2018 at 05:05):
We're going to experiment to see if typeclass resolution is partly to blame, but I'm also wondering if you have a sense of whether it's better to use nat or int.
Mario Carneiro (Nov 13 2018 at 05:05):
how are you proving things?
Scott Morrison (Nov 13 2018 at 05:05):
Maybe Keeley can tell me that nat won't actually do for our purposes.
Scott Morrison (Nov 13 2018 at 05:05):
Nope, everything is in meta land.
Scott Morrison (Nov 13 2018 at 05:06):
oh --- sorry, it's not that part that is slow
Scott Morrison (Nov 13 2018 at 05:06):
it is the edit distance calculations that are slow
Scott Morrison (Nov 13 2018 at 05:06):
so this has nothing to do with proofs
Mario Carneiro (Nov 13 2018 at 05:06):
they should both be pretty fast
Keeley Hoek (Nov 13 2018 at 05:07):
We could use nat I think
I just have to find all the typeclass names I think
Mario Carneiro (Nov 13 2018 at 05:07):
for numbers less than 2^30 or so it's just using the C++ addition which should be super fast
Scott Morrison (Nov 13 2018 at 05:07):
ok, all our numbers should be small enough, I think
Keeley Hoek (Nov 13 2018 at 05:07):
do you have any idea why min could be (relatively speaking) slow?
Mario Carneiro (Nov 13 2018 at 05:07):
there is a lot of overhead for VM stuff but no more than anything else
Mario Carneiro (Nov 13 2018 at 05:08):
You can look at the code generated for a definition using set_option trace.compiler.optimize_bytecode true
Scott Morrison (Nov 13 2018 at 05:09):
oooh...
Mario Carneiro (Nov 13 2018 at 05:10):
If you inline the definition of min it's almost as fast as it possibly could be
Mario Carneiro (Nov 13 2018 at 05:11):
if you don't inline there is possible inefficiency in creating and destroying the nat.decidable_linear_ordered_semiring
Mario Carneiro (Nov 13 2018 at 05:12):
but I don't know how significant it is
Mario Carneiro (Nov 13 2018 at 05:12):
(And by inline I mean attribute [inline] min)
Keeley Hoek (Nov 13 2018 at 05:18):
ooooh
Keeley Hoek (Nov 13 2018 at 05:19):
can you inline instances?
Keeley Hoek (Nov 13 2018 at 05:19):
like where they are used
Mario Carneiro (Nov 13 2018 at 05:26):
you don't want to inline instances, you want to inline projections. My experiments with min on nat show exactly the kind of simplification you would want
Keeley Hoek (Nov 13 2018 at 10:29):
Just for the record: we ended up getting a factor-of-three speedup by inlining a bunch of important things in the hotpath, and eliminating some pesky table lookups in favor of using more memory---and parallelisation is to come!
Kenny Lau (Nov 13 2018 at 10:36):
finally someone more clever than me is using a more clever approach to speed up things! :D
Kenny Lau (Nov 14 2018 at 13:54):
@Keeley Hoek would you have any insight as to how I could speed up this without doing what I did?
Keeley Hoek (Nov 14 2018 at 14:00):
Unfortunately not without contriving a tactic kenny
---but I must get to bed!
Keeley Hoek (Nov 14 2018 at 14:00):
:O the string @mv_polynomial σ α (@comm_ring.to_comm_semiring α _inst_3) appears 31 times!
Keeley Hoek (Nov 14 2018 at 14:03):
But its definitely something to think about
(@comm_ring.to_comm_semiring α _inst_3) 67 times!
Keeley Hoek (Nov 14 2018 at 14:04):
Can you think of a general way to hint about this kind of stuff?
Maybe you could say "use comm_ring.to_comm_semiring everywhere you can first"
Keeley Hoek (Nov 14 2018 at 14:05):
To some tactic
Kenny Lau (Nov 14 2018 at 14:20):
I don't write tactics...
Keeley Hoek (Nov 14 2018 at 14:20):
:D
It's on the list, then!
Last updated: Dec 20 2023 at 11:08 UTC