change(dashboard.py): use aggregate data as single source of truth #70
Conversation
This simplifies both the webpage generation (no dependency on the .json files) and the code, conceptually. It allows removing all filling in of placeholders. Further clean-ups left for the future include - remove a now-duplicate method in generate_assignment_page - removing the BasicPRInformation class, as its content is essentially a subset of the aggregate PR information. Landing this depends on PR data being updated reliably: not yet.
|
Do not land this PR yet: wait for leanprover-community/mathlib4#21881 to land first. |
|
The mathlib PR has landed. Next (and hopefully last) blocker: make re-downloading more robust to intermittent failures, by downloading to a temporary file and overwriting the existing data only if that download was successful. |
|
Good news: 807e3467087b3919b24b547ddf841fae81ceaaca should make the re-downloading more robust against transient failures. (And subsequent fall-out was fixed, so I am now confident the change works correctly.) Bad news: the mathlib PR does not work as expected (and would, in any case, only apply to PRs which a recent enough master branch). So perhaps it's best to wait for a webhook before landing this (edit: filed as leanprover-community/queueboard-core#11). |
This simplifies both the webpage generation (no dependency on the .json files) and the code, conceptually. It allows removing all filling in of placeholders.
Further clean-ups left for the future include
Landing this depends on PR data being updated reliably: not yet.