proposal: add a dashboard page to the website

Stream: Equational

[David Renshaw]

https://github.com/teorth/equational_theories/pull/201

[David Renshaw]

Screenshot from 2024-10-02 14-05-00.png

[David Renshaw]

It got a quick merge and now it's live!
https://teorth.github.io/equational_theories/dashboard/

[David Renshaw]

We can link to this from the README, and maybe also from the webpage topbar.

[Shreyas Srinivas]

@David Renshaw : It seems there is no link to the dashboard from the homepage

[David Renshaw]

correct, and we should add one

[Shreyas Srinivas]

I think in the case of the dashboard it might be nice to have the link be a button along with the ones for blueprint

[David Renshaw]

I agree

[David Renshaw]

I'll prepare a follow-up PR including those things

[David Renshaw]

... now that we've proven the basic thing to work

[David Renshaw]

also, I think I want to tweak the location, so that it's at https://teorth.github.io/equational_theories/dashboard/ (instead of dashboard.html)

[David Renshaw]

added the links and adjusted the URL in equational#205

[David Renshaw]

another quick merge, and the new dashboard location is now live: https://teorth.github.io/equational_theories/dashboard/

[Terence Tao]

I think the dashboard button is pointing to the wrong URL (one needs to insert a "equational_theories"). Also I think @Joachim Breitner also deserves to be listed as a maintainer :grinning_face_with_smiling_eyes:

[Marcus Rossel]

What does "implicitly true/false" mean?

[David Renshaw]

I think equational#208 should fix the url issue, but I don't know of a good way for me to test it other than just landing it and seeing what happens

[Joachim Breitner]

Terence Tao said:

I think the dashboard button is pointing to the wrong URL (one needs to insert a "equational_theories"). Also I think Joachim Breitner also deserves to be listed as a maintainer :grinning_face_with_smiling_eyes:

That's kind of you, but I actually removed myself. I wanted to help kickstart this project, but hope it thrives without continuous involvement.

[David Renshaw]

Now the dashboard says 99.958% complete, which I think means there must be a bug with conjecture handling.

[Terence Tao]

Marcus Rossel said:

What does "implicitly true/false" mean?

Implicitly true means that the statement does not explicitly appear in the Lean repository as a proved theorem, but it can be derived from proved results. For instance, if it is explicitly proven that EquationX implies EquationY, and it is also explicitly proven that EquationY implies EquationZ, then it is implicitly proven that EquationX implies EquationZ.

I guess some text should be added to the dashboard to indicate this. Is there a file for the dashboard template that one can edit directly for this, or is it buried in some script somewhere?

[Terence Tao]

David Renshaw said:

Now the dashboard says 99.958% complete, which I think means there must be a bug with conjecture handling.

This actually matches the numbers @Daniel Weber has reported with his Vampire run (only 7999 open implications remaining!). It's only conjectural because the Vampire output is not yet converted to Lean, and it was more surprising than I expected (the initial projection was in "tens of thousands"), but still remarkable progress.

[Cody Roux]

I appreciate that Vampire has the marketing savvy to propose 7999 instead of the more expensive 8000

[Shreyas Srinivas]

Am I the only person experiencing broken links on the blueprint page?

[David Renshaw]

I was just noticing that

[David Renshaw]

we need to add the {site.url} thing for all the buttons

[Shreyas Srinivas]

I think it's some relative URL kicking in.

[Shreyas Srinivas]

Because I get ..../dashboard/blueprint instead of /blueprint when I click on the buttons from the dashboard page

[Shreyas Srinivas]

Otherwise the other pages work well

[David Renshaw]

equational#213

[David Renshaw]

I guess some text should be added to the dashboard to indicate this. Is there a file for the dashboard template that one can edit directly for this, or is it buried in some script somewhere?

The text of the dashboard comes from here:
https://github.com/teorth/equational_theories/blob/d62e04389479e627c949e960336658448c30e16e/scripts/generate_dashboard.py#L31

[David Renshaw]

It would probably be possible to move the static parts into a checked-in dashboard/index.md and then use jekyll variables or templating or whatever to fill in the dynamic parts.

[David Renshaw]

I'm editing that text right now to fix the issue where conjectures are not counted

[David Renshaw]

PR incoming shortly

[Terence Tao]

Perhaps we can have two percentages, a % of verified completeness, and a % of conjectured completeness

[David Renshaw]

equational#214

[Terence Tao]

Looks great!

By the way, are the statistics being recorded somewhere, say on a daily basis? Eventually it would be nice to have a time series, so it's worth recording the data now as it would be a pain to try to reconstruct it later.

[David Renshaw]

Not currently being recorded. I agree that it would be good to have a time series.

[David Renshaw]

It is always possible to iterate through git history, but definitely easier to record things as we go along.

[David Renshaw]

It's not immediately obvious to me what the best way to do that would be, but I haven't thought about it too much.

[David Renshaw]

I mean, quick and dirty is I set up a cron job on my local machine to record the data. But I'm not sure I want to commit to that.

[Joachim Breitner]

I'm surprised to have such a low number for implicitly false, given that at least for some of the massive counterexamples, I prune verified equations based on known implications

[David Renshaw]

My guess is that equational#224 added a bunch of explicit edges.

[Zoltan A. Kocsis (Z.A.K.)]

Yes, this is it. No pruning based on implications was done on that dataset yet. I plan to look into it tomorrow, though (along with adding a bunch more refutations).

[Joachim Breitner]

Ah, spotted that in the readme now

[David Renshaw]

PR adding the output image from outcomes_to_image.py to the dashboard: equational#327.

[David Renshaw]

@Amir Livne Bar-on if I wanted to updated the svg badge to have numeric precision, how would I do that? I see the make_progress_badge function and the text formatting, but I don't know the best way to edit the svg to make it wider so that more digits fit.

[Amir Livne Bar-on]

The right way to do it is to use the pybadges library. I wasn't sure how to install it in CI, so I used the "blueprint" badge as a template and tweaked the widths manually...

[David Renshaw]

increased to 4 digits after the decimal: equational#383

[Amir Livne Bar-on]

Another thought: show the absolute number of unknown implications

[David Renshaw]

There is the "no proof" column: https://teorth.github.io/equational_theories/dashboard/

[David Renshaw]

is that what you mean?

[Amir Livne Bar-on]

Yes, this one