Zulip archive

Stream: general

[Reid Barton]

The zulip archive seems to be stuck at March 1, anyone know what is going on there?

[Rob Lewis]

@Scott Morrison ? The repo looks fine, most likely a server thing.

[Scott Morrison]

Gah. That computer is offline, and as I'm in Berkeley for the semester it may be a big pain to get it back online. :-(

[Scott Morrison]

Realistically I think we should find a more reliable server for this cron job. Bryan has also just noticed that the online web editor is going stale, for the same reason.

[Patrick Massot]

Could we use that Azure thing that now hosts our oleans?

[Rob Lewis]

Patrick Massot said:

Could we use that Azure thing that now hosts our oleans?

Took the words right out of my keyboard.

[Rob Lewis]

I'm almost certain it can, although there's a small layer of complication in everything to do with Azure.

[Patrick Massot]

I'm glad you recovered from your Super Tuesday sickness so that you can go back to Azure fighting.

[Rob Lewis]

Half recovered, anyway, we'll see if I make it to work tomorrow...

[Anne Baanen]

It seems the Zulip archive bot is having issues. Threads are showing up on the archive page, but recent threads give 404 errors. https://leanprover-community.github.io/archive/113488general/52877Enterlambdainconv.html is the oldest thread I can find giving a 404 (Apr 03 2020 at 10:25). The previous page, https://leanprover-community.github.io/archive/113488general/08031Overlyspecificinstancesininitcategory.html exists (latest: Apr 03 2020 at 05:08)

[Rob Lewis]

Oops, this was me fat fingering the update last time I did it by hand. Should be fixed in a second, but not quite up to date.

[Rob Lewis]

Needless to say, I haven't found the time yet to pick up the Azure fighting.

[Marc Huisinga]

is there a way to search the zulip archive? i've found what i was looking for now but i'm wondering whether there's an easy way to search the entire thing for the future.
i suppose using site:https://leanprover-community.github.io/archive/ <query> in google kind of works ...

[Kevin Buzzard]

The Zulip search functionality is quite good (you can restrict to streams, look for posts by a particular person etc)

[Kevin Buzzard]

I mean on the app or website

[Rob Lewis]

Yeah, the archive isn't really designed to be used directly. The whole point is for people to land there via search engines.

[Marc Huisinga]

ah, i just learned that clicking on "search in all public streams" in zulip when scrolling to the top of the search results yields the full search history

[Marc Huisinga]

i was looking through the archive because i believed that zulip doesn't preserve the full history. turns out that you just need to click that button to look for stuff that happened before your arrival.