We've talked about adding the title to the filename several times over
the years and it seems really valuable. This requires us to compute a
"slug" for the title spelling that can be part of the filename.
Beyond that, we crossed 7000 recently, and so it seems likely that we
will need to add digits sooner rather than later here, so this goes
ahead and moves us to 6 digits so we don't have to adjust again for a
reasonable length of time.
To implement this and ensure we can sustain it going forward this adds a
tool to our pre-commit that validates (and corrects if needed) the
filename.
In order to update everything and keep links working, there are a _lot_
of changes, but the most interesting for direct review are in
`proposals/scripts`.
Assisted-by: Antigravity with Gemini
---------
Co-authored-by: Richard Smith <richard@metafoo.co.uk>
Establish a principle that understanding the meaning and performance should not depend on expensive context, and explain what makes context expensive.
Co-authored-by: Chandler Carruth <chandlerc@gmail.com>
Co-authored-by: Jon Meow <46229924+jonmeow@users.noreply.github.com>
Co-authored-by: Richard Smith <richard@metafoo.co.uk>
Chandler CarruthandRichard Smith
Dennis Onyeka
Jon Ross-Perkins
Jon Meow
