Zulip Chat Archive

Stream: general

Topic: import analysis


view this post on Zulip Scott Morrison (May 15 2019 at 00:37):

@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?

view this post on Zulip Scott Morrison (May 15 2019 at 00:37):

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.

view this post on Zulip Scott Morrison (May 15 2019 at 00:38):

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.

view this post on Zulip Scott Morrison (May 15 2019 at 00:41):

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

view this post on Zulip Floris van Doorn (May 15 2019 at 02:09):

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

view this post on Zulip Floris van Doorn (May 15 2019 at 02:10):

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

view this post on Zulip Reid Barton (May 15 2019 at 02:23):

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

view this post on Zulip Floris van Doorn (May 15 2019 at 02:26):

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.

view this post on Zulip Mario Carneiro (May 15 2019 at 02:28):

I would suggest looking for indented later lines

view this post on Zulip Mario Carneiro (May 15 2019 at 02:33):

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

view this post on Zulip Mario Carneiro (May 15 2019 at 02:34):

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

view this post on Zulip Mario Carneiro (May 15 2019 at 02:35):

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

view this post on Zulip Simon Hudon (May 15 2019 at 15:34):

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


Last updated: May 16 2021 at 05:21 UTC