From 957893d410eb1e80c8fed3d1f7dfc3e2db14713d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Aug 2025 12:54:40 -0700 Subject: [PATCH 01/10] chore: Bump toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1e70935..980709b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.21.0 From f58ea76f5bf4779bd20dfb19c817334ab91fb3e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Aug 2025 13:34:53 -0700 Subject: [PATCH 02/10] fix: Use `NeZero` semantics instead of Fin n.succ --- {LSpec => Examples}/Examples.lean | 22 ++++++++++----------- {LSpec => Examples}/Testing.lean | 0 LSpec.lean | 2 +- LSpec/SlimCheck.lean | 3 +++ LSpec/SlimCheck/Control/Random.lean | 30 +++++++++++++++-------------- LSpec/SlimCheck/Sampleable.lean | 10 +++++----- 6 files changed, 36 insertions(+), 31 deletions(-) rename {LSpec => Examples}/Examples.lean (94%) rename {LSpec => Examples}/Testing.lean (100%) create mode 100644 LSpec/SlimCheck.lean diff --git a/LSpec/Examples.lean b/Examples/Examples.lean similarity index 94% rename from LSpec/Examples.lean rename to Examples/Examples.lean index 840611c..c656927 100644 --- a/LSpec/Examples.lean +++ b/Examples/Examples.lean @@ -6,7 +6,7 @@ section LSpec open LSpec /- The simplest way to invoke `LSpec` is in a file via the `#lspec` command -/ -#lspec test "Nat equality" (4 ≠ 5) +#lspec test "Nat equality" (4 ≠ 5) /- `#lspec` runs a sequence of tests which are encoded with the inductive type `TestSeq` which allows @@ -18,7 +18,7 @@ for tests to be composable /- Tests that can be tested are of the `Testable` typeclass, which have a low-priority instance -`(p : Prop) : Decidable p → Testable p` which can be over-ridden to allow for more intricate +`(p : Prop) : Decidable p → Testable p` which can be over-ridden to allow for more intricate failure or success messages. This instance is generic enough that tests like `∀ n, n < 10 → n - 5 < 5` can be evaluated @@ -48,7 +48,7 @@ def main := do -- ✓ fiveIO equals 5 -- 0 -/- +/- There are even more ways to invoke LSpec tests (`lspecEachIO` for example) for more intricate moandic testing -/ @@ -72,7 +72,7 @@ example : SampleableExt Nat := by infer_instance check "mul_comm" $ ∀ n m : Nat, n * m = m * m -- ? add_comm -- × mul_comm - + -- =================== -- Found problems! -- n := 1 @@ -95,7 +95,7 @@ private def mkPairs (as : List α) (bs : List β) : List (α × β) := /- An instance of `Shrinkable` is needed -/ open Shrinkable in instance : Shrinkable Pairs where - shrink := fun p => + shrink := fun p => let shrinkl := shrink p.left let shrinkr := shrink p.right mkPairs shrinkl shrinkr |>.map fun (a, b) => ⟨a, b⟩ @@ -103,14 +103,14 @@ instance : Shrinkable Pairs where /- As is one for `SampleableExt`. -In both of these cases we are using the instances already written for more primitive types like +In both of these cases we are using the instances already written for more primitive types like `Nat`, but it's possible to write a these instances by hand if we want more fine-grained behavior. -/ open SampleableExt def pairsGen : Gen Pairs := return ⟨← Gen.chooseAny Nat, ← Gen.chooseAny Nat⟩ -/- +/- To generate the instance of `SampleableExt α` we use the `mkSelfContained` function which relies only on having a `Gen α`. @@ -121,11 +121,11 @@ instance : SampleableExt Pairs := mkSelfContained pairsGen /- Now we can conduct the tests just as we did before for `Nat` -/ #lspec check "left + 2 is less than right" $ ∀ pair : Pairs, pair.left + 2 ≤ pair.right -/- -You always have to be careful with your implementation for `shrink` and `SampleableExt` because +/- +You always have to be careful with your implementation for `shrink` and `SampleableExt` because Slimcheck may not flag tests that should fail, in this case `⟨0, 0⟩` should fail the test but isn't detected -/ -#lspec check "left + right > right" $ ∀ pair : Pairs, pair.left + pair.right > pair.right +#lspec check "left + right > right" $ ∀ pair : Pairs, pair.left + pair.right > pair.right -end SlimCheck \ No newline at end of file +end SlimCheck diff --git a/LSpec/Testing.lean b/Examples/Testing.lean similarity index 100% rename from LSpec/Testing.lean rename to Examples/Testing.lean diff --git a/LSpec.lean b/LSpec.lean index d215c2b..50f1702 100644 --- a/LSpec.lean +++ b/LSpec.lean @@ -1,3 +1,3 @@ import LSpec.LSpec import LSpec.Instances -import LSpec.SlimCheck.Checkable +import LSpec.SlimCheck diff --git a/LSpec/SlimCheck.lean b/LSpec/SlimCheck.lean new file mode 100644 index 0000000..111b730 --- /dev/null +++ b/LSpec/SlimCheck.lean @@ -0,0 +1,3 @@ +import LSpec.SlimCheck.Gen +import LSpec.SlimCheck.Checkable +import LSpec.SlimCheck.Sampleable diff --git a/LSpec/SlimCheck/Control/Random.lean b/LSpec/SlimCheck/Control/Random.lean index 9d3b348..126e351 100644 --- a/LSpec/SlimCheck/Control/Random.lean +++ b/LSpec/SlimCheck/Control/Random.lean @@ -33,13 +33,13 @@ namespace SlimCheck /-- A monad to generate random objects using the generic generator type `g` -/ abbrev RandT (g : Type) := StateM (ULift g) -instance inhabitedRandT [Inhabited g] [Inhabited α] : Inhabited (RandT g α) where +instance inhabitedRandT [Inhabited g] [Inhabited α] : Inhabited (RandT g α) where default := fun _ => pure (default, .up default) /-- A monad to generate random objects using the generator type `Rng` -/ abbrev Rand (α : Type u) := RandT StdGen α -instance inhabitedStdGen : Inhabited StdGen where +instance inhabitedStdGen : Inhabited StdGen where default := mkStdGen /-- `Random α` gives us machinery to generate values of type `α` -/ @@ -76,36 +76,38 @@ namespace Random open Rand /-- Generate a random value of type `α`. -/ -def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : RandT g α := +def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : RandT g α := Random.randomR range.lo range.hi /-- Generate a random value of type `α` between `x` and `y` inclusive. -/ def randBound (α : Type u) [Random α] (lo hi : α) [RandomGen g] : RandT g α := Random.randomR lo hi -def randFin {n : Nat} [RandomGen g] : RandT g (Fin n.succ) := - λ ⟨g⟩ => randNat g 0 n.succ |>.map Fin.ofNat ULift.up +def randFin {n : Nat} [NeZero n] [RandomGen g] : RandT g (Fin n) := + λ ⟨g⟩ => + let (x, gen) := randNat g 0 n.succ + (Fin.ofNat n x, ULift.up gen) instance : Random Bool where - randomR := fun lo hi g => + randomR := fun lo hi g => let (n, g') := RandomGen.next g.down match lo, hi with - | true, false => (n % 2 == 1, .up g') + | true, false => (n % 2 == 1, .up g') | false, true => (n % 2 == 0, .up g') -- this doesn't matter btw, I'm just being quirky | x, _ => (x, .up g') instance : Random Nat where - randomR := fun lo hi g => - let (n, g') := randNat g.down lo hi + randomR := fun lo hi g => + let (n, g') := randNat g.down lo hi (n, .up g') -instance {n : Nat} : Random (Fin n.succ) where - randomR := fun lo hi g => - let (n, g') := randNat g.down lo hi - (.ofNat n, .up g') +instance {n : Nat} [NeZero n] : Random (Fin n) where + randomR := fun lo hi g => + let (x, g') := randNat g.down lo hi + (Fin.ofNat n x, .up g') instance : Random Int where - randomR := fun lo hi g => + randomR := fun lo hi g => let lo' := if lo > hi then hi else lo let hi' := if lo > hi then lo else hi let hi'' := (hi' - lo').toNat diff --git a/LSpec/SlimCheck/Sampleable.lean b/LSpec/SlimCheck/Sampleable.lean index f6bdf88..9785d5d 100644 --- a/LSpec/SlimCheck/Sampleable.lean +++ b/LSpec/SlimCheck/Sampleable.lean @@ -125,7 +125,7 @@ instance Nat.shrinkable : Shrinkable Nat where shrink := Nat.shrink /-- `Fin.shrink` works like `Nat.shrink` but instead operates on `Fin`. -/ -partial def Fin.shrink {n : Nat} (m : Fin n.succ) : List (Fin n.succ) := +partial def Fin.shrink {n : Nat} [NeZero n] (m : Fin n) : List (Fin n) := if 0 < m then let m := m / 2 let rest := shrink m @@ -133,7 +133,7 @@ partial def Fin.shrink {n : Nat} (m : Fin n.succ) : List (Fin n.succ) := else [] -instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where +instance Fin.shrinkable {n : Nat} [NeZero n] : Shrinkable (Fin n) where shrink := Fin.shrink local instance Int_sizeOfAbs : SizeOf Int := ⟨Int.natAbs⟩ @@ -161,8 +161,8 @@ open Gen SampleableExt instance Nat.sampleableExt : SampleableExt Nat := mkSelfContained (do choose Nat 0 (← getSize)) -instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) := - mkSelfContained (do choose (Fin n.succ) (Fin.ofNat 0) (Fin.ofNat (← getSize))) +instance Fin.sampleableExt {n : Nat} [NeZero n] : SampleableExt (Fin n) := + mkSelfContained (do choose (Fin n) (Fin.ofNat n 0) (Fin.ofNat n (← getSize))) instance Int.sampleableExt : SampleableExt Int := mkSelfContained (do choose Int (-(← getSize)) (← getSize)) @@ -221,4 +221,4 @@ instance sampleableExt [SampleableExt α] [Repr α] : SampleableExt (NoShrink α end NoShrink -end SlimCheck \ No newline at end of file +end SlimCheck From 90c9c06c9d74b4d630418fcce28d091a397083a0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Aug 2025 13:35:59 -0700 Subject: [PATCH 03/10] chore: Remove deprecated notation --- LSpec/SlimCheck/Gen.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LSpec/SlimCheck/Gen.lean b/LSpec/SlimCheck/Gen.lean index 3c3f392..675e9e2 100644 --- a/LSpec/SlimCheck/Gen.lean +++ b/LSpec/SlimCheck/Gen.lean @@ -66,12 +66,12 @@ def listOf (x : Gen α) : Gen (List α) := /-- Given a list of example generators, choose one to create an example. -/ def oneOf [Inhabited α] (xs : Array (Gen α)) : Gen α := do let x ← chooseNatLt 0 xs.size - xs.get! x + xs[x]! /-- Given a list of examples, choose one to create an example. -/ def elements [Inhabited α] (xs : List α) : Gen α := do let x ← chooseNatLt 0 xs.length - pure $ xs.get! x + pure xs[x]! open List in /-- Generate a random permutation of a given list. -/ From 03997ec5294663e46a8d71985c90e18499a882de Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Aug 2025 13:46:34 -0700 Subject: [PATCH 04/10] chore: Remove deprecated function --- LSpec/LSpec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean index c98a393..3dab516 100644 --- a/LSpec/LSpec.lean +++ b/LSpec/LSpec.lean @@ -183,7 +183,7 @@ def lspecIO (map : HashMap String (List TestSeq)) (args : List String) : IO UInt let filteredMap := if args.isEmpty then map else Id.run do - let mut acc := .empty + let mut acc := .emptyWithCapacity args.length for arg in args do for (key, tSeq) in map do if key.startsWith arg then @@ -191,7 +191,7 @@ def lspecIO (map : HashMap String (List TestSeq)) (args : List String) : IO UInt pure acc -- Accumulate error messages - let mut testsWithErrors : HashMap String (Array String) := .empty + let mut testsWithErrors : HashMap String (Array String) := .emptyWithCapacity map.size for (key, tSeqs) in filteredMap do IO.println key for tSeq in tSeqs do From 3fb462de4fa8c3c9b1ef924356b8b358b29398cc Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 7 Aug 2025 15:56:16 -0700 Subject: [PATCH 05/10] chore: Update lean4-nix --- flake.lock | 38 ++++++++++++++++++++++++++------------ flake.nix | 5 +---- 2 files changed, 27 insertions(+), 16 deletions(-) diff --git a/flake.lock b/flake.lock index 91c25fb..fad311d 100644 --- a/flake.lock +++ b/flake.lock @@ -39,31 +39,29 @@ "lean4-nix": { "inputs": { "flake-parts": "flake-parts_2", - "nixpkgs": [ - "nixpkgs" - ] + "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1744206621, - "narHash": "sha256-17kctQIIENhliHEQzzM06OlzrF4uyq6w7KOXSeNbZc4=", - "owner": "argumentcomputer", + "lastModified": 1753488936, + "narHash": "sha256-NETxbzgc9t/eiaZWN8yexDHNS7qKdnpdAc0QqVLcCLY=", + "owner": "lenianiva", "repo": "lean4-nix", - "rev": "f798c4f818301c3dd3f5ffa1b667f824b72921a4", + "rev": "7a1d030195bc5e986d7a64e3257622bfdd7ec410", "type": "github" }, "original": { - "owner": "argumentcomputer", + "owner": "lenianiva", "repo": "lean4-nix", "type": "github" } }, "nixpkgs": { "locked": { - "lastModified": 1744098102, - "narHash": "sha256-tzCdyIJj9AjysC3OuKA+tMD/kDEDAF9mICPDU7ix0JA=", + "lastModified": 1754498491, + "narHash": "sha256-erbiH2agUTD0Z30xcVSFcDHzkRvkRXOQ3lb887bcVrs=", "owner": "nixos", "repo": "nixpkgs", - "rev": "c8cd81426f45942bb2906d5ed2fe21d2f19d95b7", + "rev": "c2ae88e026f9525daf89587f3cbee584b92b6134", "type": "github" }, "original": { @@ -103,11 +101,27 @@ "type": "github" } }, + "nixpkgs_2": { + "locked": { + "lastModified": 1744098102, + "narHash": "sha256-tzCdyIJj9AjysC3OuKA+tMD/kDEDAF9mICPDU7ix0JA=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "c8cd81426f45942bb2906d5ed2fe21d2f19d95b7", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "flake-parts": "flake-parts", "lean4-nix": "lean4-nix", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs_2" } } }, diff --git a/flake.nix b/flake.nix index d8edd2b..9c57b4a 100644 --- a/flake.nix +++ b/flake.nix @@ -4,10 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean4-nix = { - url = "github:argumentcomputer/lean4-nix"; - inputs.nixpkgs.follows = "nixpkgs"; - }; + lean4-nix.url = "github:lenianiva/lean4-nix"; }; outputs = inputs @ { From 1e3c987f31e27aca2a58024d7892ed7aaedfe7f0 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 8 Aug 2025 09:33:55 -0400 Subject: [PATCH 06/10] chore: Use Garnix cache for lean4-nix --- .github/workflows/ci.yml | 6 +----- flake.nix | 9 +++++++++ 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4658f50..231500a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,12 +25,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - - uses: cachix/install-nix-action@v30 + - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable github_access_token: ${{ secrets.GITHUB_TOKEN }} - - uses: cachix/cachix-action@v14 - with: - name: argumentcomputer - authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}' - run: nix build diff --git a/flake.nix b/flake.nix index 9c57b4a..c689a6b 100644 --- a/flake.nix +++ b/flake.nix @@ -1,6 +1,15 @@ { description = "LSpec Nix Flake"; + nixConfig = { + extra-substituters = [ + "https://cache.garnix.io" + ]; + extra-trusted-public-keys = [ + "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g=" + ]; + }; + inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; From ceaba89cf117faaac90b3173e4da9fe81a39efa8 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 8 Aug 2025 09:35:28 -0400 Subject: [PATCH 07/10] Test CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 231500a..3bd1178 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,7 +2,7 @@ name: CI Tests on: push: - branches: main + branches: [main, 61-lean4-nix] pull_request: workflow_dispatch: From 358061d99981fdbd1c064a8b26c19034faec97e6 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 8 Aug 2025 09:44:32 -0400 Subject: [PATCH 08/10] Accept flake config --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3bd1178..7531d94 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,4 +29,4 @@ jobs: with: nix_path: nixpkgs=channel:nixos-unstable github_access_token: ${{ secrets.GITHUB_TOKEN }} - - run: nix build + - run: nix build --accept-flake-config From 3a0db668ce4ce758c0def950e0eaa9a8b7894483 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 8 Aug 2025 16:23:58 -0400 Subject: [PATCH 09/10] Update flake.lock --- flake.lock | 33 +++++++++++++++------------------ 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/flake.lock b/flake.lock index fad311d..3ee6b10 100644 --- a/flake.lock +++ b/flake.lock @@ -23,11 +23,11 @@ "nixpkgs-lib": "nixpkgs-lib_2" }, "locked": { - "lastModified": 1743550720, - "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "c621e8422220273271f52058f618c94e405bb0f5", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", "type": "github" }, "original": { @@ -42,11 +42,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1753488936, - "narHash": "sha256-NETxbzgc9t/eiaZWN8yexDHNS7qKdnpdAc0QqVLcCLY=", + "lastModified": 1754679239, + "narHash": "sha256-b/sd16BbXD2O/llObC4EaT4iBFvtLuqOv48XwOmfAtU=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "7a1d030195bc5e986d7a64e3257622bfdd7ec410", + "rev": "3fda6e88605a229cc9e777e10bb7ac35fc2ed8db", "type": "github" }, "original": { @@ -57,11 +57,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1754498491, - "narHash": "sha256-erbiH2agUTD0Z30xcVSFcDHzkRvkRXOQ3lb887bcVrs=", + "lastModified": 1743095683, + "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=", "owner": "nixos", "repo": "nixpkgs", - "rev": "c2ae88e026f9525daf89587f3cbee584b92b6134", + "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6", "type": "github" }, "original": { @@ -88,17 +88,14 @@ }, "nixpkgs-lib_2": { "locked": { - "lastModified": 1743296961, - "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", - "owner": "nix-community", - "repo": "nixpkgs.lib", - "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", - "type": "github" + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" }, "original": { - "owner": "nix-community", - "repo": "nixpkgs.lib", - "type": "github" + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" } }, "nixpkgs_2": { From 0bb7826e8a82fa82cfa2aec5c4ccb75106e4ccc1 Mon Sep 17 00:00:00 2001 From: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 8 Aug 2025 16:31:10 -0400 Subject: [PATCH 10/10] Fix CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7531d94..52532e8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,7 +2,7 @@ name: CI Tests on: push: - branches: [main, 61-lean4-nix] + branches: main pull_request: workflow_dispatch: