create deprecated module

Stream: mathlib4

[Jireh Loreaux]

Suppose file A has imports X, Y and Z. Then A gets (cleanly, no splitting / moving) renamed to B. We then perform a module deprecation for A. What should be the imports of the (now deprecated) module A? The create_deprecated_module command uses X, Y and Z, but I think it should be B alone.

cc @Damiano Testa, but I'm interested in input from anybody.

[Jireh Loreaux]

Here is my reasoning for saying B as opposed to X, Y, Z. Suppose I am a downstream file that imports A, and I use the declaration foo within A. After the rename and deprecation, when I tried to build my file, I get a warning on the import line saying "replace A with X, Y, Z", and also my file is broken (because it references foo which is now in B, which I am not importing). Moreover, even if I follow the advice of the deprecation warning, my file still doesn't build. So, yeah, that sucks.

In contrast, if A just contiains B as the import, then I get the warning, and my file builds both before and after the substitution.

[Jireh Loreaux]

nevermind me, I think this is just noise and I'm using create_deprecated_module wrong.

[Michael Rothgang]

I agree that the command should use B, and IIRC create_deprecated_module already does that. If you spot a case where it's wrong, please report the bug :-)

[Jireh Loreaux]

My issue was that find_deleted_files want generating the rename_to, I guess because the match wasn't strong enough.