Obtaining imports of a specific module

Stream: lean4

[Henrik Böving]

I'd like to compute an import adjacency Matrix for doc-gen4 to generate the Imported By and Import parts of the internal navbar. My idea was to somehow obtain the module names that are imported per module and then use the module indices to build an adjacency matrix based on that and use it for said purpose.

I dug a bit into how the original doc gen does it and it seems there exists a function that can extract an Environment which only represents a single module and then I can just check the imports in that Environment and am done. So I went to search for a similar function in Lean 4 but I couldn't find one so far, does there exist something like this or maybe another way to do what I want?

[Sebastian Ullrich]

No, doc-gen simply calls lean --deps https://github.com/leanprover-community/doc-gen/blob/3f7734b267ac8119565c9e833e50da16a457e1c7/print_docs.py#L325

[Henrik Böving]

Ah I was looking at how they do the tactic imported by things: https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L362-L372

[Henrik Böving]

Does this mean without the source files it is impossible to determine which inputs are done, based exclusively on the .oleans?

[Sebastian Ullrich]

readModuleData has the information, but importModules currently discards it except for the main module

[Henrik Böving]

So basically if I wanted to do this with just the oleans we would have to modify Environment to already contain the import data for each module, maybe as a Array (Array ModIdx) (with the outer array being indexed by the module indices as well) and let importModules construct said map based on the readModuleData output? Would that be a reasonable change or should I just use lean --deps on the source files as well?

[Sebastian Ullrich]

It would not be unreasonable to just expose the Array ModuleData from ImportState in EnvironmentHeader. They are not freed anyway, so there is no overhead.

[Henrik Böving]

I'll get to it!