Timing function executions

Stream: Is there code for X?

[Tanner Duve]

Is there a way to output the execution time of a function? Something like #eval perhaps that includes time?

[Kim Morrison]

See Mathlib.Util.Time

[Kim Morrison]

which provides #time

[Kim Morrison]

If you tell me Mathlib is not easily available where you are, I will ask that someone PRs it to lean4, and I will promise to hit merge. :-)

[Tanner Duve]

thank you! im working in a large codebase that has had issues every time I've tried to add mathlib to my dependencies and import it. could this be done only in lean4?

[Kim Morrison]

Sure, I've been meaning to do this for some time.

[Kim Morrison]

(@Mario Carneiro, I'm going to move your #time command from Mathlib.Util.Time up to Lean4, assuming that's okay.)

[Tanner Duve]

Thanks!

[Kim Morrison]

@Tanner Duve, lean#5044.

It should be in nightly-2024-08-15 in about 10 hours, (i.e. you could try replacing the contents of your lean-toolchain with leanprover/lean4:nightly-2024-08-15 then), and then in v4.12.0-rc2 at the beginning of September.

[Kim Morrison]

(If you'd like to describe to me either here or via DM your difficulties resulting from adding mathlib, I'd be interested.)

[Tanner Duve]

Thanks I really appreciate it. For adding mathlib, I just followed the directions here for an existing project: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency. I then try to build my project and the entire thing fails to build with a bunch of error messages. Tried lake clean but same issue.

[Tanner Duve]

Hey, wanted to check back in on this. When I replace the contents of lean-toolchain I get the following error:

info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version leanprover/lean4:nightly-2024-08-15
info: caused by: could not download file from 'https://github.com/leanprover/lean4-nightly/releases/expanded_assets/nightly-2024-08-15' to '/Users/tduve/.elan/tmp/v1fx1ugo4bdsy9rd_file'
info: caused by: http request returned an unsuccessful status code: 404

Any idea how to solve this?

[Chris Bailey]

Just wait, I think. If I'm reading the original message right, the nightly for 8-15 gets released in ~5 more hours.

[Kim Morrison]

Sorry, nightly was delayed yesterday. It usually lands at about 2024-08-16T18:00:00+10:00.

[Eric Wieser]

Tanner Duve said:

I then try to build my project and the entire thing fails to build with a bunch of error messages. Tried lake clean but same issue.

Which Lean toolchain were you using? Note that mathlib isn't really compatible with nightlies without extra steps (choosing the right branch and waiting for Kim to magically fix all the errors).