## Stream: general

### Topic: graphs on the website

#### Rob Lewis (Apr 29 2020 at 15:38):

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 (Apr 29 2020 at 15:41):

@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 (Apr 29 2020 at 15:41):

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

#### Bryan Gin-ge Chen (Apr 29 2020 at 16:01):

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


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

#### Rob Lewis (Apr 29 2020 at 16:04):

Of course it should, thanks!

#### Rob Lewis (Apr 29 2020 at 16:05):

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 (Apr 29 2020 at 16:16):

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

#### Bryan Gin-ge Chen (Apr 29 2020 at 16:33):

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 (Apr 29 2020 at 16:33):

Ooops... that script was really hackish

#### Johan Commelin (Apr 29 2020 at 16:33):

1 sec... I can try to help

#### Rob Lewis (Apr 29 2020 at 16:33):

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

#### Rob Lewis (Apr 29 2020 at 16:34):

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

#### Rob Lewis (Apr 29 2020 at 16:37):

@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 (Apr 29 2020 at 16:37):

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

#### Rob Lewis (Apr 29 2020 at 16:38):

Yes, that would be very amusing too!

#### Johan Commelin (Apr 29 2020 at 16:38):

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 (Apr 29 2020 at 16:39):

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 (Apr 29 2020 at 16:39):

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

#### Rob Lewis (Apr 29 2020 at 16:40):

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

#### Rob Lewis (Apr 29 2020 at 16:40):

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

#### Rob Lewis (Apr 29 2020 at 16:40):

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

#### Bryan Gin-ge Chen (Apr 29 2020 at 16:41):

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 (Apr 29 2020 at 16:41):

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 (Apr 29 2020 at 16:41):

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 (Apr 29 2020 at 16:42):

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.

#### Johan Commelin (Apr 29 2020 at 16:43):

Patrick Massot said:

#### Bryan Gin-ge Chen (Apr 29 2020 at 16:44):

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

#### Bryan Gin-ge Chen (Apr 29 2020 at 16:44):

Oh, maybe this should be a different thread.

#### Johan Commelin (Apr 29 2020 at 16:45):

Bryan Gin-ge Chen said:

Since we're on the topic of nolints,

No we're not :grinning:

#### Johan Commelin (Apr 30 2020 at 11:38):

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

Rob Lewis said:

#### Johan Commelin (Apr 30 2020 at 11:40):

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

#### Rob Lewis (Apr 30 2020 at 13:23):

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 (Apr 30 2020 at 13:25):

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

#### Johan Commelin (Apr 30 2020 at 13:25):

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

#### Rob Lewis (Apr 30 2020 at 13:28):

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

#### Rob Lewis (May 11 2020 at 16:26):

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

Last updated: May 11 2021 at 00:31 UTC