Make dashboard generation project-agnostic

[grunweg]

@jcommelin raised the idea of making the dashboard generation to other projects, i.e. allowing other projects (on github, but perhaps also on other platforms) to re-use the same logic. In fact, the frontend of this project ("take a bunch of PR metadata and generate the dashboard webpage(s) from it") is pretty agnostic --- so this could be done!

The following is the current state of the various parts of the project front-end.

• util.py and ci_status.py are fully generic; nothing to do
• classify_pr_state.py contains the particular classification logic (which is somewhat mathlib-specific); perhaps this can be made configurable (see below)
• state_evolution.py has a mild mathlib dependency: it hard-codes the organisation name, and the "on_the_queue" methods assume there's a PRStatus variant AwaitingReview
• mathlib_dashboards.py is entirely mathlib-specific; could be replaced by a configuration file in the future
• compute_dashboard_prs.py: first half is mathlib-agnostic (100 lines); second half is mathlib-specific
• dashboard.py: first half is mathlib-agnostic (400 lines); webpage layout is project-specific for now
• generate_assignment_page.py is considered internal-only for now (but should not be hard to generalise if needed)
• send_zulip_dm.py: completely project-agnostic; currently unused, but could be used in generate_assignment_page.py

(The files process.py and check-data-integrity.py are part of the backend, hence not relevant.)

[grunweg]

Current plan for moving towards this goal

• make a first pass over the files, separating mathlib-agnostic and more specific parts
• simplify the dashboard generation, by making it operate on aggregate data only --- see leanprover-community/queueboard#70
• retrieve certain parameters from a configuration file instead (see below)
• once happy, add instructions how to adapt this dashboard to a different project

---

About the mathlib-specific parts, some of them are easy to make configurable via e.g. a toml file.

Make configuration options

• organisation on github (determines repo URL, but also when a PR is from a fork)
• repository name

Unsure/up for discussion, but could be mostly configured/kept as generic logic

• overall PR states --- perhaps, the enumeration is generic enough to not require customisation?
• if the former is kept fixed, the map "label names to PR states" could be configurable: simply have a list of "these label names map to these states"
• priorisation of PR states: that is perhaps fine for other projects, and we're simply making slightly opinionated decisions?

Could be made configurable:

• list of possible dashboards, with their descriptions etc.

Harder to configure: it might be easier to have a clearly marked Python file, which must be edited to produce the desired output, than inventing (or using) a bespoke configuration language to re-implement the logic.

• maybe: the detailed computation of each PR dashboard (e.g., putting a query string similar to Github's search syntax) --- that would entail parsing the string, and turning that into a sequence of my internal methods.
• the particular webpages generated: including PR statistics, a table of contents or the explanatory paragraphs on the triage page