List all definitions/theorems/etc. of a library

Stream: lean4

[Rick de Wolf]

Hi folks, I'm trying to build a tool that reads out the definitions, theorems, and other objects defined in a Lean library. I'm not sure how to list those from Lean, so I could use some pointers. Thanks!

(If someone knows how to do this using the reverse foreign function interface that'd be great to hear about too. I'm planning on using this functionality in a Julia package.)

[Kim Morrison]

Don't have time for a detailed answer, but try the Lean Metaprogramming book, and many examples of variations of this in the repos. e.g. lean-training-data has several extraction tools.

[Damiano Testa]

I could only find this link, but it has been asked other times as well.

[Rick de Wolf]

Thanks for your answers, that looks like it'll be enough for me to find my way :)

I'm honestly surprised there's already a library written for this. It would be nice to have a kind of list for Lean and Mathlib related projects to make it easier for people to find, or does this exist somewhere already?

[Jannis Limperg]

Reservoir aims to track all(?) Lean 4 projects.

[Henrik Böving]

All Lean projects that it can find and do not explicitly opt out yes.

[Damiano Testa]

This is another thread with a related function.