From 189ebbfb19cef956fa8c39aae7368b0e1120e0b5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 5 Jan 2025 10:33:09 +1100
Subject: [PATCH] patches for nightly-2025-01-04, and drop Batteries dependency

---
 Plausible/Gen.lean        | 12 +++++++++---
 Plausible/Sampleable.lean |  1 +
 lake-manifest.json        |  4 ++--
 lakefile.toml             |  5 -----
 lean-toolchain            |  2 +-
 5 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/Plausible/Gen.lean b/Plausible/Gen.lean
index 44f3386..12b358e 100644
--- a/Plausible/Gen.lean
+++ b/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
diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean
index 37aeef1..8e976c9 100644
--- a/Plausible/Sampleable.lean
+++ b/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
 
 /-!
diff --git a/lake-manifest.json b/lake-manifest.json
index aeb508b..f98e851 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/lakefile.toml b/lakefile.toml
index e262e7d..e12448b 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -8,8 +8,3 @@ name = "Test"
 
 [[lean_lib]]
 name = "Plausible"
-
-[[require]]
-name = "batteries"
-scope = "leanprover-community"
-rev = "v4.16.0-rc1"
diff --git a/lean-toolchain b/lean-toolchain
index 62ccd71..61f7bcf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc1
+leanprover/lean4:nightly-2025-01-04