stable files in mathlib

Stream: general

[Johan Commelin]

Quiz: Which file in src/ was has the oldest "last-modification-time"?

[Anne Baanen]

Hmm, probably something in data or logic, those don't tend to get a lot of love.

[Anne Baanen]

The oldest-modified file in the whole repo is LICENSE

[Anne Baanen]

According to a quick command, src/data/sigma/default.lean and src/linear_algebra/default.lean were both last touched when they were created, 2019-01-15.

However, those were actually moved into src/, and if we don't count moves, it looks like src/data/sigma/default.lean wins!

[Yury G. Kudryashov]

What if we exclude default.lean files?

[Eric Rodriguez]

Then it's tactic/find.lean (16/03/2020). If you exclude tactic, then meta/uchange.lean (10/05/2020); the last mathematical thing I seem to find is data/equiv/functor.lean, edited on 27/05/2020. (and even then, they're programming functors and not really mathematical - the last thing that 100% has no meta use is category_theory/closed/monoidal.lean, at 17/06/2020.)