Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang and Damiano Testa
Lean数学库Mathlib是形式化数学领域中增长最快的库之一。我们描述了管理这种增长的各种策略，同时允许变更并避免维护者过载。这包括通过弃用系统处理破坏性变更、使用代码质量分析工具（代码检查工具）为用户提供关于常见陷阱的直接反馈、通过有意识的库（重新）设计加快编译时间、处理技术债务以及编写自定义工具来帮助审查和分类新贡献。
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding maintainer overload. This includes dealing with breaking changes via a deprecation system, using code quality analysis tools (linters) to provide direct user feedback about common pitfalls, speeding up compilation times through conscious library (re-)design, dealing with technical debt as well as writ...
