Lean Chat Archive

Stream: general

[Jason Rute]

The Lean Chat archive for Zulip hasn't been archiving for a few weeks.

[Junyan Xu]

I think the Archive Bot is supposed to update it every day, at least in 2020: https://github.com/leanprover-community/archive/commits/main

[Johan Commelin]

We were storing the archives on github, and they became a bit too large... So we've stopped the updater a while ago.

[Johan Commelin]

Since zulip now has web-accessible streams, imho the need for the archive has decreased a lot

[Eric Wieser]

Updates can still be triggered manually by maintainers

[Junyan Xu]

Johan Commelin said:

Since zulip now has web-accessible streams, imho the need for the archive has decreased a lot

If everything is publicly accessible then yes, but currently there is a disparity between what's available in archive and what's accessible without log-in. For example, I had to manually copy the content when I wanted to share this post in #IMO-grand-challenge. Maybe the solution is to make every archived stream accessible without log-in?

[Eric Wieser]

That seems like a reasonable suggestion. I also don't think that reinstating the bot would be a disaster (since the new CI is significantly lighter on GitHub); but I didn't bother sorting out cron jobs because I wasn't sure anyone cared, and I didn't want to deal with sorting a GitHub token.

[Jason Rute]

I’d be open to making #IMO-grand-challenge and #Machine Learning for Theorem Proving public.

[Junyan Xu]

I like the basic HTML UI of the archive site as it's less resource intensive. However, a drawback is that it doesn't motivate readers to sign up and join the discussion, because there isn't even a direct link to Zulip.

[Scott Morrison]

I've made #IMO-grand-challenge and #Machine Learning for Theorem Proving web-public.

[Joachim Breitner]

The mathlib4 README still says

Much of the discussion surrounding mathlib occurs in a Zulip chat room. Since this chatroom is only visible to registered users, we provide an openly accessible archive of the public discussions. This is useful for quick reference; for a better browsing interface, and to participate in the discussions, we strongly suggest joining the chat. Questions from users at all levels of expertise are welcomed.

but <https://leanprover-community.github.io/archive/stream/113488-general/index.html> seems to be stuck in January and I vaguely remember that this is intentional, now that Zulip doesn’t need registration to view it.

I can PR a fix to the README to remove the link to the archive, but before I do that: Is that really the current plan? Wouldn’t it be useful to keep the static file (I assume) archive for, well, archival, linknig and googleability reasons? There is so much knowledge in the history, it might be prudent to keep it around in that form?

Ah, it seems I found the right topic where this was discussed last. Sounds like @Eric Wieser was running this, and wasn’t sure if it was still useful? I think it is :-)

[Eric Wieser]

I've just triggered a manual job (on github actions) to regenerate the archive

[Joachim Breitner]

So I’ll change the README to no longer claim that zulip is only visible to registered users, but keep the reference to the archive (https://github.com/leanprover-community/mathlib4/pull/6332)