graphs on the website

Stream: general

[Rob Lewis]

I needed something to procrastinate with between lecture planning, so gitstats graphs are now on the community webpage and will be updated every day. Check out what quarantines have done to our commit rates: https://leanprover-community.github.io/mathlib_stats/activity.html#commits_by_year/month

[Rob Lewis]

@Johan Commelin a while back you gave a script for tracking our progress with nolints.txt: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nolints.20stats

I tried to update this slightly and auto generate it as well, but I'm doing something wrong with gnuplot. https://github.com/leanprover-community/mathlib_stats/runs/630157720?check_suite_focus=true
The script it's running is here and it calls gnuplot plot.gnu. I just want it to dump a .png somewhere in the docs folder. Any idea what I'm doing wrong?

[Kevin Buzzard]

more lines were removed in April than were added in January :-)

[Bryan Gin-ge Chen]

cut -f2 -d: nolint_graph.sh > rev_stats.txt

This looks suspicious to me. Should that be nolint_graph_out.txt instead?

[Rob Lewis]

Of course it should, thanks!

[Rob Lewis]

Let's see if it works in 2+x minutes. Actions isn't very precise with its cron job timing.
oops, coming soon...

[Bryan Gin-ge Chen]

It still looks wrong (ends in .sh rather than .txt).

[Bryan Gin-ge Chen]

Still broken :sad:. What do nolints_graph_out.txt and rev_stats.txt look like? Should they be uploaded at the end of the action?

[Johan Commelin]

Ooops... that script was really hackish

[Johan Commelin]

1 sec... I can try to help

[Rob Lewis]

I just pushed another fix, the bash script was running on the mathlib_stats repo instead of mathlib.

[Rob Lewis]

As I say every time I push a CI fix: this time it should work.

[Rob Lewis]

@Johan Commelin this is 99% for my own amusement, so don't worry about it too much :) I like graphs and I like to see them decrease automatically.

[Bryan Gin-ge Chen]

It'd be nice to auto-generate import graphs or leancrawler graphs too.

[Rob Lewis]

Yes, that would be very amusing too!

[Johan Commelin]

leanproject import-graph does take about 2 minutes to run on my machine. But it would be quite nice to get those too.

[Patrick Massot]

Rob Lewis said:

As I say every time I push a CI fix: this time it should work.

This patience is really admirable. I hate this CI cycle.

[Johan Commelin]

And I guess we don't do this in the normal CI right? This is some separate action, or something?

[Rob Lewis]

Yes, it's a separate action. It's a cron job that will run once a day (once it's working right).

[Rob Lewis]

https://github.com/leanprover-community/mathlib_stats

[Rob Lewis]

It's easy enough to add more stages to it.

[Bryan Gin-ge Chen]

I think the jobs will still count against our limit of 20 concurrent Github actions jobs (though this isn't likely to be a problem for a while).

[Rob Lewis]

Anything in the /docs folder of that repo will appear at http://leanprover-community.github.io/mathlib_stats . If we want to host something at a different URL we need another repo, which isn't a big deal.

[Patrick Massot]

Bryan Gin-ge Chen said:

It'd be nice to auto-generate import graphs or leancrawler graphs too.

The full import graph in svg is already easy with leanproject, but it's a mess. What would be much nicer is something more dynamic, using a JS graph library, but this requires quite a bit of structured procrastination. Improving leancrawler and integrating it to leanproject is still on my TODO list, but also requires time

[Rob Lewis]

Running once a day, we don't have much to worry about with concurrent actions. We can schedule them for whatever we think the quietest time is.

[Patrick Massot]

and we'll reevaluate when Scott will return to Australia

[Rob Lewis]

[Rob Lewis]

<https://leanprover-community.github.io/mathlib_stats/nolints.png>

[Johan Commelin]

Patrick Massot said:

and we'll reevaluate when Scott will return to Australia

He already has

[Bryan Gin-ge Chen]

Since we're on the topic of nolints, what do we think about lean#200 (linting the core library)?

[Bryan Gin-ge Chen]

Oh, maybe this should be a different thread.

[Johan Commelin]

Bryan Gin-ge Chen said:

Since we're on the topic of nolints,

No we're not :grinning:

[Johan Commelin]

@Rob Lewis What is the URL for the autogenerated nolints graph?

[Rob Lewis]

Rob Lewis said:

<https://leanprover-community.github.io/mathlib_stats/nolints.png>

[Johan Commelin]

Thanks, I guess we don't really want to link to it from the main site, right?

[Rob Lewis]

I'm not sure it's really of general interest. Maybe we could customize the gitstats output to include it, but I don't really feel like figuring out how to do that myself.

[Johan Commelin]

No, it's fine like this... I guess

[Johan Commelin]

There's probably only 14 people interested in that graph anyway, and they can remember (where to find) the url

[Rob Lewis]

I did put the mathlib loc graph on the front page of the website because it's pretty.

[Rob Lewis]

Rob Lewis said:

https://leanprover-community.github.io/mathlib_stats/nolints.png

And now there's a lovely cliff edge in the graph! Thanks @Mario Carneiro