Cached Mathlib doc of different versions

Stream: new members

[Yicheng Tao]

The doc page of Mathlib seems to only maintain the latest version. I wonder if the community can cache the doc of released versions of Mathlib. It can benefit those who need a specific version of Mathlib. After all, build it locally takes a long time.

[Floris van Doorn]

This is reasonable. We'll try to start doing that.

[Yaël Dillies]

The docs are really huge, no? I don't think we can store more than 10-ish versions or so

[Floris van Doorn]

They're pretty big, yeah. But even just hosting the last few versions would already be very useful.

[Yicheng Tao]

Floris van Doorn said:

They're pretty big, yeah. But even just hosting the last few versions would already be very useful.

Thanks for the reply. Since the existing searching applications like leandojo's retriever and leansearch all rely on a specific version of Mathlib, I think at least we need to know which one is stable and safe to use, and which one needs an update.

By the way, leandojo's retriever seems never update since its release. That means it still uses 4.2.0-rc1. I suspect its validity now. Looking forward to a tool analyzing and visualizing the differences between any two versions of Mathlib. The community page only displays the current status and progress by year, which is not so helpful. If there hasn't been such a tool, maybe I will have a try to build one at my free time.

[Ruben Van de Velde]

I'm not sure this would be a net positive if it encourages people to stay on old versions of mathlib

[Yicheng Tao]

Ruben Van de Velde said:

I'm not sure this would be a net positive if it encourages people to stay on old versions of mathlib

I think it shouldn't be a problem. Despite those who are working on the expansion of Mathlib, there are still people who need a stable version. Maybe for teaching or machine learning.

[Yicheng Tao]

And for those who want to keep up-to-date, the tool I mentioned above is just what they need to quickly migrate from old version to the newest.