tag

Stream: FLT

[Kevin Buzzard]

Reading this post -- this affects us, right? We should make a 4.17.0 tag? I am a bit unclear about what this means. Does this mean that we have to solve our bump problems being discussed here first, and then make a tag, and then we're done?

[Ruben Van de Velde]

Well, the question is if we'll manage to make flt work with the tagged version of mathlib

[Eric Wieser]

(#general > v4.17.0 @ 💬 is the working link)

[Eric Wieser]

The discussion there suggests waiting for #22488, which would unfortunately mean that you cannot release something compatible with mathlib v4.17.0.

[Salvatore Mercuri]

We can solve our bump problems without #22488, either by increasing maxheartbeats or by inserting some specific letIs to help instance search. I have a build that's working locally

[Yakov Pechersky]

just FYI let and letI are the same in a proof context. the I in letI doesn't have anything to do with instances, unlike in lean3.

[Ruben Van de Velde]

It's no big deal, though

[Salvatore Mercuri]

I've a PR bumping to v4.17.0 here. I think the idea is that we merge this, then someone with direct access tags it, and then I can create another PR to unpin the Lean version from the toml? (at least I wasn't able to tag it through this PR)

[Kevin Buzzard]

I don't know the first thing about tags. I've merged the bump PR -- I then went to "tags" on github but there already seemed to be a v4.17.0 tag?

[Salvatore Mercuri]

Oh maybe that did work then

[Ruben Van de Velde]

Oh cool, CI did it: https://github.com/ImperialCollegeLondon/FLT/actions/runs/13652630981/job/38164487092

[Pietro Monticone]

Yep, we have a workflow file for that

[Salvatore Mercuri]

Oh nice, OK I better unpin the version from the toml then