listing all declarations used in theorem

Stream: general

[Chris Hughes]

Has anyone written meta code to list all the declarations used in a theorem including the declarations used by theorems that the first theorem uses and so on? I wrote some, but it's not fast enough to execute without a deterministic timeout. I want this for Lean 3 by the way.

[Yaël Dillies]

leancrawler? That's what people use for LTE or sphere eversion

[Alex J. Best]

Does the code in #16911 help, something like this should be possible in lean without timeouts, but if you re-visit declarations more than once I can see why it would be too slow

[Jason Rute]

Lean has a docs#hash_map and even docs#name_map and docs#name_set specialized to names, so it is possible to loop over everything and store what you have already seen to speed it up.

[Chris Hughes]

I wrote the most optimized code I could using name_set and stuff, and it's still not quite fast enough. Is there some way to just increase deterministic timeout to more than 2^32-1

[Mario Carneiro]

if you run lean from the command line there is no timeout