Release packages automatically for mathlib4 docs?

Stream: general

[Jz Pan]

Is it possible to make the CI of mathlib4 docs https://github.com/leanprover-community/mathlib4_docs uploads a package of compressed mathlib4 docs pages to the Release page https://github.com/leanprover-community/mathlib4_docs/releases ? I think this can be done by adding extra steps before/after Upload artifact step in https://github.com/leanprover-community/mathlib4_docs/blob/main/.github/workflows/docs.yaml .

It's best to have this as a source of offline mathlib4 docs for my TryLean4 Windows bundle as I don't need to compile it by myself, which takes several hours on the Windows CI machine.

Currently it can only be downloaded in the Actions tab (for example https://github.com/leanprover-community/mathlib4_docs/actions/runs/13783192013). The file format also seems a little bit weird: it's a zip file, but after unpacking it's a tar file (anyways my build script can still handle such files).

[Kim Morrison]

The problem here is that there is no notion of releases for mathlib4_docs. If we could sort that out (e.g. I've proposed elsewhere that Mathlib should just create master-YYYY-MM-DD tags once per day), I'd be happy to see a PR adding a CI step uploading such a bundle.

[Eric Wieser]

I think even having a tarball for every release for the existing tags would be handy

[Eric Wieser]

For trylean, I would guess we want to pin to major versions to avoid situations where two people in the same class download versions a day or two apart

[Jz Pan]

I think for the mathlib docs, release for each stable tags, plus "nightly" is enough. After all the online version of mathlib docs only have "nightly" version.

[Jz Pan]

Eric Wieser said:

For trylean, I would guess we want to pin to major versions to avoid situations where two people in the same class download versions a day or two apart

That's a TODO in my build script, but I haven't add code to actually handle it yet.

FYI, the trylean bundle is discussed here #general > trylean bundle for lean4 @ 💬