Zulip Chat Archive

Stream: general

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:

name = "mathlib"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.2"
path = "src"


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 ccs

Last updated: Aug 03 2023 at 10:10 UTC