Gource video of set.mm contributions

67 views
Skip to first unread message

David A. Wheeler

unread,
Sep 28, 2019, 10:02:33 PM9/28/19
to metamath
I've created a Youtube video showing set.mm contributions over time using Gource.
You might enjoy this:

https://youtu.be/rjlRGAfjPMs

The video shows the state of set.mm over time.
The date is at the top center, increasing over time.
Every small dot is an assertion ($a or $p).
The structure is the structure of the set.mm headings (as of 2019-09-28).
The little "people" represent contributors; the flashes from
contributors to dots shows the creation or modification of an assertion.
You can see a lonely Norman Megill at the beginning, and it
gets progressively busier over time.

The video is "unpublished" (unlisted) on Youtube,
because I don't know if I need to make
important changes before publicly listing it there.

Let me know what you think!

--- David A. Wheeler

ookami

unread,
Sep 29, 2019, 3:09:52 AM9/29/19
to Metamath
The video is really cool.  Thanks for this.

Wolf

Benoit

unread,
Sep 29, 2019, 8:26:06 AM9/29/19
to Metamath
Thanks David, nice video!

Is it possible to have a less lossy compression (I watched the 1080p version on youtube and it's very pixelized)?

Is it possible (and fast enough to implement) to put some color on the tree?  If I understand correctly, the leaves are the $a- and $p-statements and I see at the beginning that some are colored (what color code?), and the internal nodes are the sections of set.mm?  Would it be possible, without too much work, to use the colors used in the MPE (the rainbow-like hue), both for the leaves and for the internal nodes and branches (the color of a section would be that of its first statement)?

Benoit

Alexander van der Vekens

unread,
Sep 29, 2019, 9:01:56 AM9/29/19
to Metamath
Really amazing! But it would be great if one can obtain more information (the labels aren't really readable), e.g. which field (chapter?) each of the "blossoms" belongs to. Maybe colors (as proposed by Benoit) may help...

Alexander

David A. Wheeler

unread,
Sep 29, 2019, 10:03:17 AM9/29/19
to Benoit, Metamath
On September 29, 2019 8:26:06 AM EDT, Benoit <benoit...@gmail.com> wrote:
>Thanks David, nice video!
>
>Is it possible to have a less lossy compression (I watched the 1080p
>version on youtube and it's very pixelized)?

I will try. I will have to investigate ffmpeg options, there are a huge number of options that I need to track down and try.

>Is it possible (and fast enough to implement) to put some color on the
>tree? If I understand correctly, the leaves are the $a- and
>$p-statements
>and I see at the beginning that some are colored (what color code?),
>and
>the internal nodes are the sections of set.mm? Would it be possible,
>without too much work, to use the colors used in the MPE (the
>rainbow-like
>hue), both for the leaves and for the internal nodes and branches (the
>color of a section would be that of its first statement)?

In the video, the colored ones are ones that have been modified. I have already made a local tweak so that $a will look different.

I think I will set the default colors so that they are generated from a hash of the top level header. I'll have to tweak that, since otherwise some of the colors will be close to Black and thus hard to see. That should produce much more differentiated colors.

Gource has a number of options, but not quite enough to make some things more distinct. An upcoming version we'll add some options that should make it much easier to handle large systems like this, but it has not been released yet, and I don't feel like trying to fight with an unreleased version.


--- David A.Wheeler

David A. Wheeler

unread,
Sep 29, 2019, 3:42:52 PM9/29/19
to metamath, Benoit
> On September 29, 2019 8:26:06 AM EDT, Benoit <benoit...@gmail.com> wrote:
> >Is it possible to have a less lossy compression (I watched the 1080p
> >version on youtube and it's very pixelized)?
...
> >Is it possible (and fast enough to implement) to put some color on the
> >tree?

Done and done. I've posted an updated Gource video here:

https://youtu.be/HWjpq1R828U

I think this one looks nicer, in particular, it's much less pixellated.
I made a few other visual tweaks as well to improve its looks.

--- David A. Wheeler

Benoit

unread,
Sep 29, 2019, 4:09:58 PM9/29/19
to Metamath
Much nicer !
And I even noticed a problem in set.mm thanks to your video: the very early appearance of "Supplementary material.../Mathbox for BJ" is due to my copy-paste error in the comment of bj-equsb1v, which I'm going to fix right now.  (There will still be bj-eu3f and bj-eumo0 which are backups of demoted theorems placed in my mathbox.)

Benoit

David A. Wheeler

unread,
Sep 29, 2019, 8:09:11 PM9/29/19
to metamath, Metamath
On Sun, 29 Sep 2019 13:09:57 -0700 (PDT), Benoit <benoit...@gmail.com> wrote:
> Much nicer !

Excellent! The Gource video is now viewable by the public. You can see it here:

https://www.youtube.com/watch?v=HWjpq1R828U

--- David A. Wheeler
Reply all
Reply to author
Forward
0 new messages