forthcoming release of v4.18.0 and v4.19.0-rc1

Stream: nightly-testing

[Kim Morrison]

Just a heads up: we've mostly finished releasing v4.18.0, Mathlib CI is processing #23520 now.

[Kim Morrison]

We're hoping to cut v4.19.0-rc1 from the nightly that lands in a few hours.

[Ruben Van de Velde]

@Kim Morrison The v4.18.0 tag points to the bot commit now - do you want to update it to your commit?

[Kim Morrison]

I don't think it's too problematic: my commit will have a every so slightly later commit of aesop/plausible, but nothing has changed there except the declared toolchain in the upstream repository.

[Kim Morrison]

Generally it's better to override overwriting tags that have already been made public unless there's a good reason to.

[Kim Morrison]

I've prevented the bot from jumping the gun on future releases.

[Eric Wieser]

Kim Morrison said:

I don't think it's too problematic: my commit will have a every so slightly later commit of aesop/plausible, but nothing has changed there except the declared toolchain in the upstream repository.

Isn't this problematic if there is a dependency graph like

Mathlib -> Aesop;
MyBasePackage ->  Aesop;
MyBigPackage -> Mathlib;
MyBigPackage -> Aesop;

as if I pin aesop to v4.18.0 in MyBasePackage , then I end up with a subtly different version to what mathlib wants in MyBigPackage, which invalidates the mathlib cache?

[Eric Wieser]

But maybe lake exe cache get doesn't even notice the mismatch, and obviously the oleans will match either way

[Johan Commelin]

Let's worry about that if the problem actually occurs.
Next month the bot should no longer interfere. We've put it on a leash :dog: