rss bot, include author?

Stream: general

[Kyle Miller]

For the recent commits topics on #rss, would it be possible to include the commit author? I think it would be some nice information to more easily keep up with who is doing what.

(Right now, we can see who coauthors are, but that can be sort of random -- sometimes it's just a reviewer whose 1-line suggestion was included.)

[Eric Rodriguez]

(or, if you use the Github web stuff, sometimes yourself again!)

[Eric Rodriguez]

It would also be nice to fix the links so links with brackets don't break so much, and also so that repos that aren't mathlib have clickable # numbers - does anyone know where the source is?

[Gabriel Ebner]

I think it's a script running on @Sebastian Ullrich's infrastructure.

[Sebastian Ullrich]

Yes. Since it really is just GitHub's RSS feed, I don't see a straightforward way to customize it.

[Eric Rodriguez]

Can't you make it fetch the details with the URL / number when it gets received?

[Eric Wieser]

https://github.com/leanprover-community/mathlib/commits/master.atom seems to contain the user information

[Eric Wieser]

Is that not the feed you're using?

[Gabriel Ebner]

And the #-numbers should be fixable with a regex.

[Sebastian Ullrich]

The implementation is at https://github.com/zulip/python-zulip-api/blob/main/zulip/integrations/rss/rss-bot. I'm not planning to fiddle with it, but I'm happy to switch to a fork or something.

[Kyle Miller]

If we change this statement to this:

    content = "{}\n\nAuthored-by: [{}]({})\n[Commit]({})".format(
        strip_tags(body),
        entry.author,
        entry.author_detail.href,
        entry.link,
    )  # type: str

then the rss-bot messages would look like this:

feat(*): localized R[X] notation for polynomial R (#11895)

I did not change polynomial (complex_term_here taking args) in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.

Co-authored-by: Johan Commelin <johan@commelin.net>

Authored-by: pechersky
Commit

[Kyle Miller]

Eric Rodriguez said:

It would also be nice to fix the links so links with brackets don't break so much

One solution to this (reflected above) is to not include the entry title, which is redundant anyway. It comes from github truncated with an ellipsis, like feat(model_theory/substructures): More operations on substructures (#…

[Eric Wieser]

I assume we're not using https://zulip.com/integrations/doc/github due to it being inferior in some other regard?

[Kyle Miller]

Eric Rodriguez said:

and also so that repos that aren't mathlib have clickable # numbers

One solution I thought of is to take the # in the first line and prefix it with the repo name from the feed name, but it's a real hack. On the Zulip side we could then make sure each possibility linkifies correctly.

    body = strip_tags(body)

    import re
    repo = re.search(r"(\w+):\w", feed_name).group(1)
    body = re.sub(r"#\d+", lambda m: repo + m.group(0), body, 1)

    content = "{}\n\nAuthored-by: [{}]({})\n[Commit]({})".format(
        body,
        entry.author,
        entry.author_detail.href,
        entry.link,
    )  # type: str

This gives

feat(*): localized R[X] notation for polynomial R (mathlib#11895)

I did not change polynomial (complex_term_here taking args) in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.

Co-authored-by: Johan Commelin <johan@commelin.net>

Authored-by: pechersky
Commit

[Kyle Miller]

Another example of that:

feat(library/init/meta): import unfreezing tactic from mathlib (lean#667)

And remove misleading mentions of unfreeze_local_instances from error messages.

Authored-by: gebner
Commit

[Kyle Miller]

I've made a fork https://github.com/kmill/python-zulip-api and here is the change

I've only been able to test this using a mock environment and I can't be sure it actually works -- I've tried to program it defensively, and it falls back to the original behavior for messages that aren't obviously commits.

[Sebastian Ullrich]

I've updated to your fork. Let's see what happens.

[Kyle Miller]

@Sebastian Ullrich Hmm, it doesn't seem to be doing anything different. The most recent commit, according to my mock environment, should look like

chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (mathlib#11981)

Since the introduction of the has_measurable_* typeclasses, the topological assumptions in that file are only used to derive the measurability assumptions. This PR removes that step.

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Authored-by: RemyDegenne
Commit

but it's still doing the old behavior:
rss-bot said:

chore(measure_theory/function/ae_eq_fun): replace topological assumpt…
chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (#11981)

Since the introduction of the has_measurable_* typeclasses, the topological assumptions in that file are only used to derive the measurability assumptions. This PR removes that step.

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
https://github.com/leanprover-community/mathlib/commit/5f70cd95e9797d171453652c4c1b913951deae26

[Sebastian Ullrich]

Yeah, I had to revert for now because of Python version troubles

[Kyle Miller]

Was it this line?

    if m := re.match("Recent Commits to (\w+):", feed_name):

[Julian Berman]

(You need a r"" there, or to write \\w, though not having it should just be a warning)

[Kyle Miller]

@Julian Berman Thanks, changed it (though Python seems to be happy to have "\w" mean "\\w"), and also switched from the walrus operator in case the problem is that the interpreter is older than version 3.8.

[Julian Berman]

Yeah -- Python will take invalid escape sequences and just drop the \\, but it emits a deprecation warning (one that's hidden by default because we're bad). I just mentioned it given Sebastian said he reverted on the off chance that whatever is running this app is running with a different setting for PYTHONWARNINGS (one where they get turned into errors). I didn't notice the walrus operator but that's way more likely to be useful.

[Eric Wieser]

I thought 3.10 raised errors for that type of escape sequence?

[Julian Berman]

Not yet -- they can't make up their minds yet I think -- https://bugs.python.org/issue32912

[Sebastian Ullrich]

Kyle Miller said:

Was it this line?

    if m := re.match("Recent Commits to (\w+):", feed_name):

There are other changes (by other people) that require at least Python 3.6 - but Debian LTS is still on 3.5...

[Gabriel Ebner]

@Kyle Miller Would it be possible to also fix issue references in the commit message? So, if the commit message says "fixes #1234", that it gets replaced by "fixes lean4#1234"?

[Mario Carneiro]

I would rather it be replaced by an explicit markdown link so that it still looks like #1234

[Eric Wieser]

On the topic of rss-bot; could we replace its profile picture in the zulip settings with something like https://cdn-icons-png.flaticon.com/512/124/124033.png so that it's easy to tell from the "recent topics" view whether the posts in RSS are from humans without a profile picture, or from the bot?

[Yaël Dillies]

Same for the new bots on Github, pretty please!

[Yaël Dillies]

... and the community account

[Yaël Dillies]

I think a Lean logo would make sense to all of them. We can have fun and give them to different logos to help differentiate.

[Anne Baanen]

Which logo should we use? ?

[Sebastian Ullrich]

How about image.png ?

[Eric Wieser]

Sebastian Ullrich said:

How about image.png ?

Using the zulip images feels like it might be confusing, as the bots aren't managed by zulip. Not a big deal though.
Note also the zulip welcome and notification bots have different colored backgrounds.

[Eric Wieser]

@Yaël Dillies, can I suggest you split your thread about github profile pictures? I've split your tangent about github avatars to a new thread. Can you update the first message to give more context?

[Yaël Dillies]

Yes you can, indeed you did :grinning: