extracting top-level objects from a module

Stream: lean4

[Kliment Serafimov]

I'm creating a website for Lean problems and proofs. I would like to be able to parse out all top-level objects in a module. e.g. def A type body; theorem B type body; I want the tool to extract a list of these as (keyword (e.g. def, lemma etc.), name, type str, body str, and possibly start line, end line), similar to how I would do in python with inspect. I tried doing this with Claude 3.7 and got somewhere but I cant just pass a file to be processed, it works only when the code is hardcoded. It's using Parser but its failing to get it working. Any help? Is there any boilerplate code for source file / ast analysis I can use?

[Kim Morrison]

You might look at my (ancient, unmaintained) https://github.com/kim-em/lean-training-data repository for similar examples, or post some code showing what you've tried so far.