new release

Stream: mathlib4

[Jon Eugster]

Is there a reason the commit a9a186c isn't tagged as v4.3.0-release yet? Could some admit quickly do that, please?

[Johan Commelin]

cc @Scott Morrison

[Scott Morrison]

I've tagged f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d as v4.3.0 now.

[Scott Morrison]

@Jon Eugster, I agree this needed doing, but I'm curious why it was time-sensitive for you. I'd be happy to hear accounts of how people are making use of these tags.

[Jon Eugster]

It's not time sensitive sensitive at all! Just wrote "quickly" because I assumed that's about 3 clicks in the UI, not because I needed it today. But thanks for adding the tag:blush:.

I just decided to update the games to account for the new .lake changes as I was just doing something where its relevant and would have preferred to directly go to v4.3.0

In the lakefiles, I use something like

def leanVersion : String := s!"v{Lean.versionString}"

require mathlib from git "..." @ leanVersion
require xy from git "..." @ leanVersion

to keep all packages on a compatible version with an easy update mechanism (edit lean-toolchain and call lake update -R), therefore Im currently relying on these tags.

I guess it could be lake's job to provide some package version managing system that respects the lean toolchain, but as that's not that trivial, this was the simplest solution I came up with to have some sort of automatism keeping downstream projects updated.

[Jon Eugster]

(only time sensitivity is that Im not supposed to work on the weekend, while I know two people who wanted a fix of my code so they could work over the weekend:wink:)