Extracting definition from source into individual file

Stream: lean4

[nrs]

As I'm continuing the project at #metaprogramming / tactics > Manual derecursification of PreDefinition, I realize that something that would make this significantly easier would be a way to grab any given definition and determine all its module dependencies, then create a new file containing only that definition along with its module dependencies (importing private declarations with Batteries.Tactic.OpenPrivate). I think this might be useful e.g. to butcher an internal definition until it stops working, in order to determine where the critical components lie (particularly, the context-independent components, but maybe a variation of this idea might help us determine context-dependent components too).

Anyone ever tinker with this? or the idea of extracting module dependencies from a definition in general?

[nrs]

seems like a starting point for this would be some sort of variation on using

#eval show CoreM Unit from do
  let env <- getEnv
  let consts := env.constants

where given a constant in consts.map\2 we somehow attempt to get dependencies in the same file (from consts.map\2) and the imported ones from consts.map\1

[Ruben Van de Velde]

Have you looked at #min_imports and similar commands?

[nrs]

@Ruben Van de Velde did not know of it, will be checking it out, thanks a lot!

edit: relevant topic #general > Minimal lean file for a definition or theorem