FRONTEND: Develop a CI to regularly compute the latest statistics of implications, and add them (e.g., as a time series) to README.md (or some other file linked from README.md).

[teorth]

Relevant statistics could include those from #29, as well as number of outstanding implications modulo known equivalences. Links to text files enumerating these various implications would also be useful.

[Shreyas4991]

Should we consider this task completed?

[teorth]

I don't think we actually have a time series yet - as far as I know the dashboard output is not being saved in any file - but we should have all the architecture to do so, and I think it is a good idea (I am manually recording the dashboard status each day now, but this is clearly not the long-term solution).

[euprunin]

To ensure the time series is fully reproducible, the headline data could be stored on a per-commit basis. This approach would allow one to "replay" the Git history and recreate the point-in-time measurements for each commit.

Additionally, commits could be mapped to specific pull request (PR) merges, which are timestamped in sequential order, enabling the creation of a time series.

By implementing this method, we avoid the issue of relying on external or aggregated data snapshots, which may not reflect the true state at each commit. This also ensures that historical analysis can be consistently reproduced, preserving data integrity across the project's lifetime.

[carlini]

I've started a PR #479 to add this data for all past commits. Currently it has going back to the 2nd, and I'll get the commits from before then later today.

The main question is how to make it automatically add this data for the future. It appears there are three options:

1. Because main is protected, the CI tool can't push anything to main. One option around this is to have it push a commit to the branch that's about to be merged before the merge happens. I think this is possible, but have never done it. So maybe it doesn't work.
2. It might be possible to unprotect main only for the CI tool. I don't know how to do this, but some internet searching suggests that there are ways to grant special permissions that might make this work. A maintainer would have to handle doing this though.
3. A final option is to have the CI tool push to a separate (unprotected) branch of the project every time someone merges a new commit with main, and then have someone manually merge this separate branch into main every once and a while (once a day, say) to keep things on track.

Thoughts?

[Shreyas4991]

The script can be called from inside I think CI? Where do you wish to store this data? The CI cannot add any data or persist files it creates.

[Shreyas4991]

One problem with option 3 is that the project webpage is generated off the main branch of the project.

[carlini]

I think the CI can add additional commits to a PR. So I'd run the tool, store the results, and log it to a file, and commit that to the repo. Or I read somewhere that was possible.

As for option 3: agreed, this would make it only update once a day. But at least it would be automated and would just need someone to click "merge" instead of rerun it.

[Shreyas4991]

Can't the CI make a pull request from a non-main branch with a specific label? Then another CI task can automatically merge these PRs if there are no build issues or merge conflicts

[carlini]

Yeah, I guess that could happen too, but would then double the number of PRs to main.

[Shreyas4991]

Can we run this as a cron job instead?