policy for copyright header in deprecated modules

Stream: mathlib4

[Kevin Buzzard]

I see that the last two deprecated_modules PRs that we merged, namely #24942 and #24947, had different ideas about whether copyright headers should be put in the deprecated files. Do we have a policy about this? I was just checking them to see what such a PR looked like before I hit merge on #25148 and now I'm confused.

Edit: Is the idea that these files get deleted by Jeremy in 6 months' time anyway?

Edit: Andrew now added the copyright header so the question is kind of moot (to be honest I am slightly surprised that #24942 passed CI!)

[Ruben Van de Velde]

The header linter is turned off for deprecated modules

[Ruben Van de Velde]

When I added them, I copied the copyright from the pre-removal module

[Damiano Testa]

The automated tool for deprecating used to preserve the copyright header, but someone, possibly @Yaël Dillies ?, suggested that it did not include the header.

[Kevin Buzzard]

Do we have a policy? Or is the policy "we don't care"?

[Mario Carneiro]

IMO they should not be treated differently

[Mario Carneiro]

deprecation and copyright are completely unrelated concepts

[Eric Wieser]

I think the point is that the deprecated module has no code from the original file any more

[Eric Wieser]

So there is nothing left to copyright

[Eric Wieser]

It doesn't even share a git history with the original file, if things are working how we wanted them to

[Eric Wieser]

Phrased another way: these are generated files, and we don't currently have a copyright notice on such files (e.g. Mathlib.lean). It would probably reasonable to put a generic "mathlib project" copyright in such files, but I doubt it really matters