Automatically extract page contributor information during web build

[VojtechStep]

The contributor list is sorted by number of commits. Any suggestions for wording and visual style are appreciated. There is a new system for attributing work to contributors, which is now opt-in; add yourself to scripts/contributors_data.toml if you want to be mentioned on the website, or have someone do it for you.

See the latest version here: https://unimath.vojtechstep.eu

Homepage

The logo now properly changes color on dark themes. The font size is bigger, and some of the window size calculations were changed so that the content doesn't overlap the right sidebar, and that sidebar is hidden on smaller screens where it's not useful. It's also hidden when printing a page with Ctrl+P, which should make it more usable.

Page attribution

The "Content created by:" line is only included in Agda source files, and the Created/Modified and Recent changes sections are only included in Agda source files and guides in the Overview section.

Recent changes

Updated list of contributors

Now including co-authors; visible names, links to github and association between visible names and git usernames can be customized via the scripts/contributors_data.toml file

Proper syntax highlighting with dark theme support

Next steps

#777 and #459 are still open; I'm still not convinced about Egbert's idea of listing changed files for every contributor.

Fixes #439
Fixes #507

[EgbertRijke]

Would it be possible/desirable to display this information immediately below the title of the page?

Don't we want to sort contributors by last name, if a first and last name are available?

Would it be possible to also display the date that the file was created, and perhaps the last date that the file was edited?

[EgbertRijke]

Also: Awsome!!

[VojtechStep]

I moved the contributors to the top.

[VojtechStep]

I added the "Created" and "Modified" fields, and now's the time when I'll need anyone's aesthetic help to make it look reasonable 😅.
I can also offer the following alternative date formats:

Personally I prefer the current one, %as, i.e. YYYY-MM-DD.

[VojtechStep]

I added the "Recent changes" section to the bottom, I'll need ideas to style that as well. I also don't think it should be a problem to add links to the corresponding commits in the GitHub repo.

That's everything from me for today.

[VojtechStep]

I also didn't address the contributor sorting; TBH I like it sorted by number of commits (if only for the fact that git does that automatically for me and I don't have to do any further processing 😅).

[EgbertRijke]

I added the "Created" and "Modified" fields, and now's the time when I'll need anyone's aesthetic help to make it look reasonable 😅.
I can also offer the following alternative date formats:

Personally I prefer the current one, %as, i.e. YYYY-MM-DD.

Yes, just the date is fine

[EgbertRijke]

I also didn't address the contributor sorting; TBH I like it sorted by number of commits (if only for the fact that git does that automatically for me and I don't have to do any further processing 😅).

Sure, that works for now. But that also sounds like we can't manually add names because this script will always rewrite the contributor attribution?

[EgbertRijke]

Instead of just "Modified" I would say "Last modified"

[VojtechStep]

I also didn't address the contributor sorting; TBH I like it sorted by number of commits (if only for the fact that git does that automatically for me and I don't have to do any further processing 😅).

Sure, that works for now. But that also sounds like we can't manually add names because this script will always rewrite the contributor attribution?

That is correct, all of this information is automatically extracted from git metadata with no option to tweak it from within the file whatsoever.

[EgbertRijke]

BTW it doesn't look like its sorted by number of commits, but it's sorted by first name. We had this problem before: with this sorting it displays capitalized names before uncapitalized names. It looks wrong to me.

[VojtechStep]

BTW it doesn't look like its sorted by number of commits, but it's sorted by first name. We had this problem before: with this sorting it displays capitalized names before uncapitalized names. It looks wrong to me.

Nope, it's certainly sorted by number of commits - the names are explicitly generated with the -n flag to git shortlog for it to be so, and some file have "Egbert Rijke and Fredrik Bakke", while others have "Fredrik Bakke and Egbert Rijke".

[VojtechStep]

It is possible that multiple users have the same number of commits (as is the case in the Order theory file, where Jonathan, Victor and Louis all have 1 commit); in which case I assume it sorts alphabetically

[EgbertRijke]

BTW it doesn't look like its sorted by number of commits, but it's sorted by first name. We had this problem before: with this sorting it displays capitalized names before uncapitalized names. It looks wrong to me.

Nope, it's certainly sorted by number of commits - the names are explicitly generated with the -n flag to git shortlog for it to be so, and some file have "Egbert Rijke and Fredrik Bakke", while others have "Fredrik Bakke and Egbert Rijke".

Darn! I have to find those files and work on them harder!

[EgbertRijke]

There is one more issue I would like to know. Sometimes people change their names. When they do, and update their info on github, do the updated names show up automatically on our website? Or does it show their names at the time they committed the work? I would not like it if our website accidentally outs those people.

[VojtechStep]

All this information is from git, not GitHub; git has no concept of identity beyond username and email, which are associated to every commit at the time of authoring, and they are part of the commit data, so changing it would require rewriting history. I would like to show GitHub usernames instead, but we'd need some sort of mapping from git usernames to GitHub usernames. I haven't thought this through, I'll take a look at it either tomorrow or on Sunday.

[EgbertRijke]

Ok, let's think this through carefully.

[VojtechStep]

I summarized the result of our discussion with @EgbertRijke in the description of the last commit, let me paste it here as well:

After some discussion with Egbert, we came to the conclusion that we
should make it possible for contributors to the library to choose how
they are presented on the website, without that presentation being
immediately linked to their GitHub account(s), and without needing to
rewrite the commit history in situations where the identity associated
with past commits is no longer the one a contributor wants to be
identified with.

The solution we came up with is to have a collection of contributor
identities, not a priori linked to any other service, where
individuals can set their preferred display name and "claim" git
usernames. When information obtained from the git log is
presented (currently the "Created by" page header and "Recent changes"
footer of pages), this table is consulted at website build-time to
display the preferred name.

If a contributor chooses not to be presented on the website, they can
be left out of the table.

The next step is to use this table to generate the CONTRIBUTORS.md
file from git log as well, instead of relying on GitHub APIs.

[EgbertRijke]

For recent changes, perhaps the following format would be cleaner:

Date. Author (and coathors?). _Short commit title (#PR)_. Short commit hash.

[VojtechStep]

For recent changes, perhaps the following format would be cleaner:

Date. Author (and coathors?). _Short commit title (#PR)_. Short commit hash.

Thanks for pointing out the missing coauthors, they should be properly included in the Recent changes section now. I tried you suggested formatting; I think it's a step in the right direction, although I'm not a fan of the hash at the end. I'll try and play with it a bit more on Sunday.

[EgbertRijke]

Well, since these titles are mostly PR titles (unless the commits are prehistoric) I think it makes sense to link to the specific PR. It is an easy way to get more information about the specific change that is listed here under recent changes.

I see now that your comment was about the hash. We could omit the hash.

[EgbertRijke]

Perhaps if we don't display the hash, the formatting could be cleaned up as follows:

Date. Authors and coauthors. _Title_. [#PR](link-to-pr)

[fredrik-bakke]

This makes it very similar to how we cite references currently, which is a nice bonus to consistency :)

[VojtechStep]

I'd rather not try to be smart and parse the PR from the commit message, but instead make a link to the specific commit (which we can do, since that's derived from the hash), and there GitHub adds the link for us - for example this a link to the last commit above: bfab474

edit: Github shortens the link, it looks like this https://github.com/UniMath/agda-unimath/commit/bfab47422b6f0110462fba1081ebd786257f38fc

[EgbertRijke]

I'd rather not try to be smart and parse the PR from the commit message, but instead make a link to the specific commit (which we can do, since that's derived from the hash), and there GitHub adds the link for us - for example this a link to the last commit above: bfab474

edit: Github shortens the link, it looks like this https://github.com/UniMath/agda-unimath/commit/bfab47422b6f0110462fba1081ebd786257f38fc

Sounds good!

[EgbertRijke]

On the other hand, the link to pull request #XYZ seems to be just

https://github.com/UniMath/agda-unimath/pull/XYZ

So it looks like "trying not to be smart" might actually require some effort in this case

[VojtechStep]

On the other hand, the link to pull request #XYZ seems to be just

https://github.com/UniMath/agda-unimath/pull/XYZ

So it looks like "trying not to be smart" might actually require some effort in this case

"Trying not to be smart" in this case means not parsing the commit message at all, and instead use the commit hash we get from git 🤷

[EgbertRijke]

Yes, I think it will look better with it.

[EgbertRijke]

The following names need corrections:

Elif Uskuplu
Victor Blanchi
Ian Ray
Ivan Kobe
Daniel Gratzer
Maša Žaucer

[VojtechStep]

Thank you; I chose the display names that appeared on the existing contributors page, if these are more appropriate I will change them.

[EgbertRijke]

Can I launch it?:)

[VojtechStep]

If you feel like it 👀

[EgbertRijke]

Let's gooooooo 🚀

[EgbertRijke]

Thank you for your amazing work!

[VojtechStep]

Now let's cross our fingers that the website build runs correctly in the CI 😅

[EgbertRijke]

It would be so funny if you made the entire website redirect here

[EgbertRijke]

Now let's cross our fingers that the website build runs correctly in the CI 😅

You shouldn't have said that:)

[VojtechStep]

macOS doesn't have cp -T? How do you guys live?

[EgbertRijke]

Who said we live?

[VojtechStep]

I think I have to make a new PR for the fix

[EgbertRijke]

Lol, get some sleep

[VojtechStep]

If that next PR doesn't fix it then I'm leaving it for tomorrow

[VojtechStep]

And I just saw that the checkout action does a --depth=1, so I'll also need to fix that, but that'll have to wait until tomorrow

[EgbertRijke]

Actually your fix doesn't show the names and the recent changes anymore

[VojtechStep]

Hm, you're right, it looks like the git metadata option didn't get enabled

[VojtechStep]

That's so weird, the CI straight up doesn't run the script. At least the contributor list is now fixed. I'll investigate more today.

[EgbertRijke]

When I try to build the website locally I get this (if it is any help to you):

Traceback (most recent call last):
  File "/Users/egbertrijke/Repositories/agda-unimath/./scripts/generate_contributors.py", line 7, in <module>
    from utils.contributors import CONTRIBUTORS_FILE, parse_contributors_file, sorted_authors_from_raw_shortlog_lines
  File "/Users/egbertrijke/Repositories/agda-unimath/scripts/utils/contributors.py", line 3, in <module>
    import tomli
ModuleNotFoundError: No module named 'tomli'
make: *** [CONTRIBUTORS.md] Error 1

[VojtechStep]

I added a Python dependency to requirements.txt, I should have mentioned that, please run python3 -m pip install -r scripts/requirements.txt again. The thing is that if the script failed, we'd get an error log from mdbook and the action would fail. As it stands it looks like mdbook never runs the preprocessor at all. I'm experimenting with the action in my repo so that we don't have to speculatively merge PRs

[EgbertRijke]

It seems that one new module called tomli is required. We should make a habit of updating the install guide when we add new dependencies to the repository. Is tomli the only new requirement?

[VojtechStep]

What would the update say? We already say that the developer needs to run the above command, you just need to rerun it when the list of dependencies changes.

Edit: Oh I see that we have an explicit list of dependencies in the prose. I'll update it when I fix the the CI.

[EgbertRijke]

It should say what the script does, i.e., what it installs when you run it. We should not ask people to trust us with our script if we don't tell them what it does:)

[VojtechStep]

#786 should both fix the CI and document the new dependency