import-graph lookahead

Stream: mathlib4

[Moritz Doll]

I don't know whether anyone else would be interested in this, but I think it might be neat if we had a option to ask the import-graph script to add the next n (I only care about n=1) dependencies below the --to node. The reason for this is that if I port a file, I can look whether that port immediately makes another file portable and then it is easier to port multiple files at once.

[Andrew Yang]

As an alternative, this information is already available in the docs; you can click on "Imported by" on the right sidebar. But I agree that this would be a useful extension to the script.

[Moritz Doll]

but "imported by" does not tell you whether the other dependencies are ported yet

[Moritz Doll]

I guess I could run the script for every file in "imported by", but this is a bit more tedious

[Patrick Massot]

I'm not sure I understand what you want. Do you want to add only one level of edges beyond the given nodes or also all the ancestors of the successors of the given node?

[Moritz Doll]

I am not too interested in seeing what the ancestors are (I am afraid that is too messy). Ideally they are not shown, but the successors are colored depending on their portability once the --to node is green.

[Moritz Doll]

i.e., all successors that only depend on --to and already ported files are blue, and if there exists an unported ancestor that is not --to then it is white

[Patrick Massot]

Ok, the difficult part is to come up with a name for the command line option trigerring this behavior

[Moritz Doll]

I am really bad with naming things, but maybe "--show-children"?