CI task suggestion: Report changes in known facts

Stream: Equational

[Joachim Breitner]

Here is a nice task for those who like writing Github Actions:

Write a bot that builds the project at the base branch and the PR branch (maybe with debug.byAsSorry to be fast), collects the results, and reports how our summary numbers (implications, anti-implications, implied implications, implied anti-implications) have changed in this PR.

[Shreyas Srinivas]

Is there already a script in the main branch that outputs this info?

[Shreyas Srinivas]

I might get to it today or tomorrow

[Shreyas Srinivas]

I see several threads on this topic, hence the question

[Joachim Breitner]

extract_implications kinda does it, but produces huge output (i.e you'd still have to tally the lists).
Maybe add a --stats mode to it that just prints the stats in json format,and post-process that.

[Daniel Weber]

There is lake exe extract_implications outcomes --hist

[Joachim Breitner]

Thanks!

For finding the right base branch,

git merge-base origin/${{ github.base_ref }} HEAD

is used for a similar task in other projects where I have seen that.
May need

    - uses: actions/checkout@v4
      with:
        # fetch full history so that git merge-base works
        fetch-depth: 0
        # fetch PR commit, not predicted merge commit
        ref: ${{ github.event.pull_request.head.sha }}

in the workflow

[Terence Tao]

Should I create an explicit task for this, or is this something that someone can just do directly with an issue or pr?

[Shreyas Srinivas]

I think this is easiest for project contributors because we already have the permissions.

[Shreyas Srinivas]

I am on a different time crunch which is why I am not doing it right away

[Terence Tao]

Ok then i will not make an explicit project task for this.

[David Renshaw]

and reports how our summary numbers (implications, anti-implications, implied implications, implied anti-implications) have changed in this PR

Do you mean mean a bot that would post on zulip? Or something that updates the webpage? (Both sound to me like good ideas.) Or something else?

[Joachim Breitner]

David Renshaw said:

and reports how our summary numbers (implications, anti-implications, implied implications, implied anti-implications) have changed in this PR

Do you mean mean a bot that would post on zulip? Or something that updates the webpage? (Both sound to me like good ideas.) Or something else?

I’d expect a comment on the PR

[David Renshaw]

Here's my go at making something that updates the website: https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/proposal.3A.20add.20a.20dashboard.20page.20to.20the.20website/near/474364688

[Shreyas Srinivas]

Will merge right away

[Shreyas Srinivas]

This helps people see the graph live and then if there are suggestions for improvement we can change it later

[Shreyas Srinivas]

(It passes CI)

[Terence Tao]

Suggestions for additions to the dashboard:

• Links to files for each of the statistics given (i.e., a link to a text file of explicitly true implications, a list of implicitly true implications, etc.).
• Stats about equivalence classes: how many equivalence classes of equations are there? How many unknown implications are there after quotienting by equivalence? See equational#176.
• A list (and count) of "equivalence-closing" implications - implications that, if proven, would generate an equivalence because the converse is already established. See equational#188.
• Similar stats, but only for the equations considered in Equations.lean. Here one can also add a Hasse diagram, as it is small enough to be human digestible. See equational#183.