issue !4#11292: Using github releases

Stream: triage

[Random Issue Bot]

Today I chose issue 11292 for discussion!

Using github releases
Created by @None (@FordUniver) on 2024-03-11
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 11292 for discussion!

Using github releases
Created by @None (@FordUniver) on 2024-03-11
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 11292 for discussion!

Using github releases
Created by @None (@FordUniver) on 2024-03-11
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 11292 for discussion!

Using github releases
Created by @None (@FordUniver) on 2024-03-11
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

Does this even make sense to do? I thought Mathlib was essentially a nightly always library

[Ruben Van de Velde]

I'm not sure what GitHub releases are, but we do make sure every lean release has a corresponding mathlib commit - and then we immediately move on

[Bryan Gin-ge Chen]

GitHub releases are a way to publish specific versions of a repo. If mathlib had any, they'd show up here: https://github.com/leanprover-community/mathlib4/releases

I guess it wouldn't hurt to highlight the git tags corresponding to major Lean versions there, since currently the list of tags is mostly filled with nightly releases.