These extensions are unloved and largely unmaintained. So we should probably mark them deprecated so people stop using them. How should we do that? -- Mathematics is the supreme nostalgia of our time.