Zulip Chat Archive

Stream: lean4

Topic: Obtaining imports of a specific module


Henrik Böving (Jan 15 2022 at 13:35):

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 (Jan 15 2022 at 16:33):

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

Henrik Böving (Jan 15 2022 at 16:48):

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 (Jan 15 2022 at 16:50):

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

Sebastian Ullrich (Jan 15 2022 at 16:52):

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

Henrik Böving (Jan 15 2022 at 17:01):

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 (Jan 15 2022 at 17:07):

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 (Jan 15 2022 at 17:15):

I'll get to it!


Last updated: Dec 20 2023 at 11:08 UTC