From 189ebbfb19cef956fa8c39aae7368b0e1120e0b5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 5 Jan 2025 10:33:09 +1100 Subject: [PATCH 1/9] 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 44f33866..12b358e8 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 37aeef14..8e976c96 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 aeb508b8..f98e851a 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 e262e7d9..e12448bc 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 62ccd717..61f7bcf8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0-rc1 +leanprover/lean4:nightly-2025-01-04 From 7a6030b92f001a0e08c59c8f39a97cdf32f627ed Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 6 Jan 2025 08:15:28 +1100 Subject: [PATCH 2/9] fix adaptation note --- Plausible/Gen.lean | 9 +-------- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/Plausible/Gen.lean b/Plausible/Gen.lean index 12b358e8..68a8b88a 100644 --- a/Plausible/Gen.lean +++ b/Plausible/Gen.lean @@ -98,21 +98,14 @@ def elements (xs : List α) (pos : 0 < xs.length) : Gen α := do return xs[x] -/-! -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/lean-toolchain b/lean-toolchain index 61f7bcf8..2d3971cd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-01-04 +leanprover/lean4:nightly-2025-01-05 From 368559effa4e27f8381fc35ade545103fa8bb409 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 17 Mar 2025 14:26:55 +1100 Subject: [PATCH 3/9] merge main --- lean-toolchain | 4 ---- 1 file changed, 4 deletions(-) diff --git a/lean-toolchain b/lean-toolchain index e75edba9..62e3298f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1,5 +1 @@ -<<<<<<< HEAD -leanprover/lean4:nightly-2025-01-05 -======= leanprover/lean4:v4.18.0-rc1 ->>>>>>> origin/main From f473315def172d9bb6528ffdb5d68cc5ddfa5c2b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 17 Mar 2025 14:28:04 +1100 Subject: [PATCH 4/9] fixes for leanprover/lean4#7516 --- Plausible/Gen.lean | 2 +- Plausible/Sampleable.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Plausible/Gen.lean b/Plausible/Gen.lean index 68a8b88a..0314c04b 100644 --- a/Plausible/Gen.lean +++ b/Plausible/Gen.lean @@ -105,7 +105,7 @@ def permutationOf : (xs : List α) → Gen { ys // xs ~ ys } | 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 ⟨ys.insertIdx n x, 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 8e976c96..6bef2ff5 100644 --- a/Plausible/Sampleable.lean +++ b/Plausible/Sampleable.lean @@ -215,7 +215,7 @@ open Shrinkable instance List.shrinkable [Shrinkable α] : Shrinkable (List α) where shrink := fun L => (L.mapIdx fun i _ => L.eraseIdx i) ++ - (L.mapIdx fun i a => (shrink a).map fun a' => L.modify (fun _ => a') i).flatten + (L.mapIdx fun i a => (shrink a).map fun a' => L.modify i (fun _ => a')).flatten instance ULift.shrinkable [Shrinkable α] : Shrinkable (ULift α) where shrink u := (shrink u.down).map ULift.up diff --git a/lean-toolchain b/lean-toolchain index 62e3298f..405a0a20 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0-rc1 +leanprover/lean4-pr-releases:pr-release-7516 From 4dfba8b20a5ce570b9ef8bae969dd163782f9793 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 17 Mar 2025 23:15:15 +1100 Subject: [PATCH 5/9] merge lean-pr-testing-7516 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 405a0a20..2b37244f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-7516 +leanprover/lean4:nightly-2025-03-17 From fde3fc21dd68a10791dea22b6f5b53c5a5a5962d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 29 May 2025 21:07:52 +1000 Subject: [PATCH 6/9] deprecations --- Plausible/Random.lean | 2 +- Plausible/Sampleable.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Plausible/Random.lean b/Plausible/Random.lean index 98e1a3e8..582a0167 100644 --- a/Plausible/Random.lean +++ b/Plausible/Random.lean @@ -137,7 +137,7 @@ def randBound (α : Type u) [LE α] [BoundedRandom m α] (lo hi : α) (h : lo Generate a random `Fin`. -/ def randFin {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ) := - fun ⟨g⟩ => return randNat g 0 n |>.map (Fin.ofNat' _) ULift.up + fun ⟨g⟩ => return randNat g 0 n |>.map (Fin.ofNat _) ULift.up instance {n : Nat} : Random m (Fin n.succ) where random := randFin diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean index d538d3f0..45584105 100644 --- a/Plausible/Sampleable.lean +++ b/Plausible/Sampleable.lean @@ -158,7 +158,7 @@ instance Nat.shrinkable : Shrinkable Nat where shrink := Nat.shrink instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where - shrink m := Nat.shrink m |>.map (Fin.ofNat' _) + shrink m := Nat.shrink m |>.map (Fin.ofNat _) instance BitVec.shrinkable {n : Nat} : Shrinkable (BitVec n) where shrink m := Nat.shrink m.toNat |>.map (BitVec.ofNat n) @@ -270,7 +270,7 @@ instance Nat.sampleableExt : SampleableExt Nat := instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) := mkSelfContained do let m ← choose Nat 0 (min (← getSize) n) (Nat.zero_le _) - return (Fin.ofNat' _ m) + return (Fin.ofNat _ m) instance BitVec.sampleableExt {n : Nat} : SampleableExt (BitVec n) := mkSelfContained do diff --git a/lean-toolchain b/lean-toolchain index 6d5cfdc7..7b37314c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.20.0-rc2 +leanprover/lean4:nightly-2025-05-29 From 26bcd128f999594a280ec55fd0422fbd0b1df5fa Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 21 Oct 2025 03:19:20 +0200 Subject: [PATCH 7/9] toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 7b37314c..4208d094 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-05-29 +leanprover/lean4:nightly-2025-10-20 From ca46151b876597b20728bd65794928efda180d13 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Nov 2025 01:13:38 +0100 Subject: [PATCH 8/9] list deprecations --- Plausible/Arbitrary.lean | 2 +- Plausible/Sampleable.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Plausible/Arbitrary.lean b/Plausible/Arbitrary.lean index a02db649..6b221992 100644 --- a/Plausible/Arbitrary.lean +++ b/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⟩ diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean index 45f1d560..341ae916 100644 --- a/Plausible/Sampleable.lean +++ b/Plausible/Sampleable.lean @@ -232,7 +232,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 diff --git a/lean-toolchain b/lean-toolchain index 5946692c..5876d7d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0-rc1 +leanprover/lean4:nightly-2025-11-02 From 533254087537a4f856164602f4689e630a5fba32 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 14 Dec 2025 22:17:14 +1100 Subject: [PATCH 9/9] chore: bump toolchain to v4.27.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index e59446d5..bd19bde0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1