all transitive imports

Stream: general

[Jason Rute]

Is there an easy way to see all the transitive imports for a given set of imports?

[Yury G. Kudryashov]

I run lake exe graph, then sed the output. Probably, there are better ways.

[Mario Carneiro]

you can get this pretty easily from lean metaprogramming, depending on what context you need it for

[Mario Carneiro]

it's already precalculated so you can just print out (<- getEnv).header.moduleNames

[Jason Rute]

@Mario Carneiro Could you give me a complete snippet? I’m not sure what monad I’m working in here.

[Mario Carneiro]

import Lean
open Lean
run_meta logInfo m!"{(← getEnv).header.moduleNames}"

[Mario Carneiro]

that will print out all the modules transitively used by the initial imports, i.e. import Init + import Lean

[Adam Topaz]

I guess if you use docs#CoreM.withImportModules you could specify the modules to import explicitly?