Topic: did finish get faster?
Jalex Stark (May 04 2020 at 18:25):
I have a codewars solution that runs in a couple of seconds on my box with heavy use of
finish but takes 16.5s on codewars. (yay limit increase!) I wonder if this could be explained entirely by finish?
Glancing by eye, the only other tactics are
cases, existsi, by_cases, clear, transitivity, symmetry, have, repeat. Codewars is on Lean 3.7.2. Is that a long time in units of mathlib progress?
Reid Barton (May 04 2020 at 18:36):
finish is some sort of tableau prover, right? I think it can easily take arbitrarily long
Reid Barton (May 04 2020 at 18:39):
Oh you were asking if it was improved. No idea
Kevin Buzzard (May 04 2020 at 18:48):
I write my codewars solutions in a repo with the exact same Lean and mathlib as the codewars version. I think that the codewars servers might have << the number of threads that you have...
Jalex Stark (May 04 2020 at 18:52):
oh, that's a good idea, and I guess easy now with leanproject?
Kevin Buzzard (May 04 2020 at 18:53):
Testing your solution on my clone with
set_option profiler true says that elaboration of your solution takes 5.93 seconds on my machine
Kevin Buzzard (May 04 2020 at 18:54):
Yes. I use a clone of mathlib. My leanpkg.toml is this:
[package] name = "mathlib" version = "0.1" lean_version = "leanprover-community/lean:3.7.2" path = "src" [dependencies]
and I checked out the appropriate mathlib commit and got the oleans with leanproject
Jalex Stark (May 04 2020 at 18:54):
ah, i see, so your machine is running 3ish times faster than what codewars gives you
Jalex Stark (May 04 2020 at 19:05):
oh it looks like a lot of my
finishs are faster as
Last updated: May 09 2021 at 18:17 UTC