did finish get faster?

Stream: general

[Jalex Stark]

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]

finish is some sort of tableau prover, right? I think it can easily take arbitrarily long

[Reid Barton]

Oh you were asking if it was improved. No idea

[Kevin Buzzard]

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]

oh, that's a good idea, and I guess easy now with leanproject?

[Kevin Buzzard]

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]

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]

ah, i see, so your machine is running 3ish times faster than what codewars gives you

[Jalex Stark]

oh it looks like a lot of my finishs are faster as ccs