Deprecated import

Stream: lean4

[Joe Hendrix]

Since removing a (public) import is a breaking change, would it be feasible to allow deprecated annotations to import statements?

The meaning would be that if you have modules A, B, and C with C importing B and B having a deprecated public import of A, then referring to any declarations of A in C would trigger a warning until C directly imports A or another module with a non-deprecated public import of A.

I think this would require marking each transitive imported module whether it is accessible only via deprecated imports, but would make it easier to fix breakage caused by removing imports.