Zulip Chat Archive

Stream: general

Topic: graphs on the website


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 15:41):

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

view this post on Zulip 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?

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:04):

Of course it should, thanks!

view this post on Zulip 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...

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 16:16):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 29 2020 at 16:33):

Ooops... that script was really hackish

view this post on Zulip Johan Commelin (Apr 29 2020 at 16:33):

1 sec... I can try to help

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:34):

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 16:37):

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

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:38):

Yes, that would be very amusing too!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:40):

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

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:40):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 29 2020 at 16:42):

and we'll reevaluate when Scott will return to Australia

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:43):

view this post on Zulip Rob Lewis (Apr 29 2020 at 16:43):

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

view this post on Zulip Johan Commelin (Apr 29 2020 at 16:43):

Patrick Massot said:

and we'll reevaluate when Scott will return to Australia

He already has

view this post on Zulip 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)?

view this post on Zulip Bryan Gin-ge Chen (Apr 29 2020 at 16:44):

Oh, maybe this should be a different thread.

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Apr 30 2020 at 11:38):

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

view this post on Zulip Rob Lewis (Apr 30 2020 at 11:39):

Rob Lewis said:

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 30 2020 at 13:25):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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