nightly#127 adaptations for nightly-2025-11-25

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-11-25 nightly#127 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

Looking through this now. The diff is huge (300+ files, 1600+ lines) and seems to be many many changes cutsat -> lia and omega -> lia. Is there anything else in there?

[Kevin Buzzard]

It would be interesting to benchmark these changes.

[Kevin Buzzard]

The scrollbar on the Files page is lying to me :-) It looks like I'm nearly at the bottom but occasionally it jumps up a bit. From the files list on the left I can see I'm abuot half way through and still no changes other than cutsat -> lia and omega -> lia

Much better than the old files page though, which would give up after around 200 files and make you open the rest manually.

[Markus Himmel]

There are a tiny number of adaptations to the String API in Mathlib.Data.String and Mathlib.Tactic. Aparat from that I think it's all lia.

[Kevin Buzzard]

I am happy to bors d+ this, I've gone through it all now.

@Joscha Mennicken is it possible to use radar on this repo to see what effect these changes have had?

[Joscha Mennicken]

Not at the moment, but we're working on getting it into radar.

[Kevin Buzzard]

Happy to merge this if someone else is prepared to look at my two comments on the PR and say "yeah this is fine".

[Robin Arnez]

Regarding the two small comments:
cutsat has been renamed to lia in lean4#11330 and Lean.Parser.Tactic.lia is in fact the correct new name.
grobner is a frontend to grind with specific options, so the fact the grobner can handle scientific literals comes directly from grind being able to normalize them.

[Kevin Buzzard]

Thanks. I merged.