library indexing speed

Stream: general

[Matthew Pocock]

I'm running library_search for the first time and it is indexing the library for the first time. It is very slow. Several seconds per entry. Many, many minutes for the whole process. My laptop fan says my CPU is hot. Is this expected?

[Alex J. Best]

What version of lean and mathlib are you using? I ask because the latest lean4 and mathlib now call library_search instead apply? and it should be quite fast and not need to index much anymore

[Matthew Pocock]

Alex J. Best said:

What version of lean and mathlib are you using? I ask because the latest lean4 and mathlib now call library_search instead apply? and it should be quite fast and not need to index much anymore

Lean 4 rc4 and matlib4 at 2f410e1ee3eeb7b9953e4e7f66169f0595148263 - not sure exactly what version that corresponds to

[Matthew Pocock]

now that it has finally indexed, I don't think I'm importing the tactics correctly

[Matthew Pocock]

No, that was user error. The apply? tactic works quite well, some of the time. Thanks.

[Scott Morrison]

@Matthew Pocock, did you run lake exe cache get first? You should expect exact? and apply? to be very slow if you haven't done that.

[Matthew Pocock]

Scott Morrison said:

Matthew Pocock, did you run lake exe cache get first? You should expect exact? and apply? to be very slow if you haven't done that.

No, I didn't. Now that it's done with melting my laptop, the queries happen very fast.

[Scott Morrison]

If you have a suggestion about where in the installation steps we could have more prominently encouraged you to run lake exe cache get, please let us know. :-)

[Scott Morrison]

(And we're working on removing the need to run it at all, but are not there yet!)