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

Plausible/Gen.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 import Plausible.Random
-import Batteries.Data.List.Perm
 
 /-!
 # `Gen` Monad
@@ -98,15 +97,22 @@ def elements (xs : List α) (pos : 0 < xs.length) : Gen α := do
   let ⟨x, _, h2⟩ ← up <| chooseNatLt 0 xs.length pos
   return xs[x]
 
-open List in
 
+/-!
+adaptation_note
+
+Due to an error in `nightly-2025-01-04`, we temporarily need `open Classical in` here,
+and `(α := α)` at the call site of `List.perm_insertIdx`. Both should be removed after `nightly-2025-01-05` is available.
+-/
+open List in
+open Classical in
 /-- Generate a random permutation of a given list. -/
 def permutationOf : (xs : List α) → Gen { ys // xs ~ ys }
   | [] => pure ⟨[], Perm.nil⟩
   | x::xs => do
     let ⟨ys, h1⟩ ← permutationOf xs
     let ⟨n, _, h3⟩ ← up <| choose Nat 0 ys.length (by omega)
-    return ⟨insertIdx n x ys, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx _ _ h3).symm⟩
+    return ⟨insertIdx n x ys, Perm.trans (Perm.cons _ h1) (List.perm_insertIdx (α := α) _ _ h3).symm⟩
 
 /-- Given two generators produces a tuple consisting out of the result of both -/
 def prodOf {α : Type u} {β : Type v} (x : Gen α) (y : Gen β) : Gen (α × β) := do

Plausible/Sampleable.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 import Lean.Elab.Command
+import Lean.Meta.Eval
 import Plausible.Gen
 
 /-!

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "rev": "18c0c2e5a1edb93e8bc86536872872522cea50f4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "plausible",

lakefile.toml

@@ -8,8 +8,3 @@ name = "Test"
 
 [[lean_lib]]
 name = "Plausible"
-
-[[require]]
-name = "batteries"
-scope = "leanprover-community"
-rev = "v4.16.0-rc1"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc1
+leanprover/lean4:nightly-2025-01-04