chore: bump toolchain to v4.26.0-rc1 (#51)

* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* toolchain

* list deprecations

* chore: bump toolchain to v4.26.0-rc1

Author: kim-em

Plausible/Arbitrary.lean

@@ -158,7 +158,7 @@ instance ULift.Arbitrary [Arbitrary α] : Arbitrary (ULift α) where
   arbitrary := do let x : α ← arbitrary; return ⟨x⟩
 
 instance String.Arbitrary : Arbitrary String where
-  arbitrary := return String.mk (← Gen.listOf arbitrary)
+  arbitrary := return String.ofList (← Gen.listOf arbitrary)
 
 instance Array.Arbitrary [Arbitrary α] : Arbitrary (Array α) := ⟨Gen.arrayOf arbitrary⟩
 

Plausible/Sampleable.lean

@@ -233,7 +233,7 @@ instance ULift.shrinkable [Shrinkable α] : Shrinkable (ULift α) where
   shrink u := (shrink u.down).map ULift.up
 
 instance String.shrinkable : Shrinkable String where
-  shrink s := (shrink s.toList).map String.mk
+  shrink s := (shrink s.toList).map String.ofList
 
 instance Array.shrinkable [Shrinkable α] : Shrinkable (Array α) where
   shrink xs := (shrink xs.toList).map Array.mk

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.1
+leanprover/lean4:v4.26.0-rc1