chore: Update Lean to v4.21.0 (#61)

* chore: Bump toolchain

* fix: Use `NeZero` semantics instead of Fin n.succ

* chore: Remove deprecated notation

* chore: Remove deprecated function

* chore: Update lean4-nix

* chore: Use Garnix cache for lean4-nix

* Test CI

* Accept flake config

* Update flake.lock

* Fix CI

---------

Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com>

Author: lenianiva

.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
+      - run: nix build --accept-flake-config

LSpec/Examples.lean Examples/Examples.leanLSpec/Examples.lean renamed to Examples/Examples.lean

@@ -25,6 +25,29 @@ This instance is generic enough that tests like `∀ n, n < 10 → n - 5 < 5` ca
 -/
 #lspec test "all lt" $ ∀ n, n < 10 → n - 5 < 5
 
+/-
+It is also possible to run tests inside the `IO` monad. The purpose of these tests is to plug in
+`LSpec` into a testing script for a `lake script`
+-/
+
+def fourIO : IO Nat :=
+  return 4
+
+def fiveIO : IO Nat :=
+  return 5
+
+def main := do
+  let four ← fourIO
+  let five ← fiveIO
+  lspecIO $
+    test "fourIO equals 4" (four = 4) $
+    test "fiveIO equals 5" (five = 5)
+
+#eval main
+-- ✓ fourIO equals 4
+-- ✓ fiveIO equals 5
+-- 0
+
 /-
 There are even more ways to invoke LSpec tests (`lspecEachIO` for example) for more intricate moandic
 testing

LSpec/Testing.lean Examples/Testing.leanLSpec/Testing.lean renamed to Examples/Testing.lean

@@ -1,3 +1,3 @@
 import LSpec.LSpec
 import LSpec.Instances
-import LSpec.SlimCheck.Checkable
+import LSpec.SlimCheck

LSpec.lean

@@ -183,15 +183,15 @@ 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
             acc := acc.insert key tSeq
       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

LSpec/LSpec.lean

@@ -0,0 +1,3 @@
+import LSpec.SlimCheck.Gen
+import LSpec.SlimCheck.Checkable
+import LSpec.SlimCheck.Sampleable

LSpec/SlimCheck.lean

@@ -83,8 +83,10 @@ def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : Ran
 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 =>
@@ -99,10 +101,10 @@ instance : Random Nat where
     let (n, g') := randNat g.down lo hi
     (n, .up g')
 
-instance {n : Nat} : Random (Fin n.succ) where
+instance {n : Nat} [NeZero n] : Random (Fin n) where
   randomR := fun lo hi g =>
-    let (n, g') := randNat g.down lo hi
-    (.ofNat' _ n, .up g')
+    let (x, g') := randNat g.down lo hi
+    (Fin.ofNat n x, .up g')
 
 instance : Random Int where
   randomR := fun lo hi g =>

LSpec/SlimCheck/Control/Random.lean

@@ -126,15 +126,15 @@ 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
     m :: rest
   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⟩
@@ -162,8 +162,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))

LSpec/SlimCheck/Sampleable.lean

@@ -1,13 +1,19 @@
 {
   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";
-    lean4-nix = {
-      url = "github:argumentcomputer/lean4-nix";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
+    lean4-nix.url = "github:lenianiva/lean4-nix";
   };
 
   outputs = inputs @ {