import analysis

Stream: general

[Scott Morrison]

@Simon Hudon, is there a way to ask olean-rs to show me the chain of imports that results in Y being a dependency of X?

[Scott Morrison]

I have a few cases in mind where I think X really shouldn't depend on Y, but I'm having trouble manually locating the chain of imports.

[Scott Morrison]

Relatedly, I wonder if we could propose a new linting rule: "all imports go on separate lines". This would really help with import analysis, because you can then search/grep for import X and be sure of finding all the locations X is imported.

[Scott Morrison]

As an example, I'm interested in why src/category_theory/instances/Top/presheaf.lean depends on src/data/finset.lean.

[Floris van Doorn]

after a little bit of manual search: data.finset <- data.fintype <- data.set.finite <- data.set.countable <- topology.bases <- topology.opens <- category.instances.Top.opens <- category.instances.Top.presheaf

[Floris van Doorn]

but yeah, a tool for that would be useful :)

[Reid Barton]

About the separate lines--you could grep for ^import.* X or something similar

[Floris van Doorn]

That doesn't work for the following, right?

import data.nat.basic
       data.set.basic

I used to write that if my first line of imports was too long.

[Mario Carneiro]

I would suggest looking for indented later lines

[Mario Carneiro]

I think ^import (\w+(\n )?.*)*?X should work, but it seems to crash vscode

[Mario Carneiro]

but actually, I think searching for data.finset should be sufficient, since it's very unlikely to show up in a lean file unless it's an import

[Mario Carneiro]

I suppose there are a few names that do double duty like tactic but most file names are not also constants

[Simon Hudon]

About the linting rule: we could get olean-rs to find all the places where a specific module is imported.