Add Plausible

Seems like we should be doing some property-based testing.
This is a POC for comments.

TensorLib/Common.lean

@@ -5,8 +5,20 @@ Authors: Jean-Baptiste Tristan, Paul Govereau, Sean McLaughlin
 -/
 
 import Std.Tactic.BVDecide
+import Plausible
+open Plausible
+
 namespace TensorLib
 
+private def plausibleDefaultConfig : Plausible.Configuration := {}
+/-
+This suppresses messages from Plausible on the commandline when building, such as
+    info: ././././TensorLib/Common.lean:37:0: Unable to find a counter-example
+If you want to see the counterexample in the IDE, you need to remove the configuration argument,
+but remember to add it back once you've fixed the bug.
+-/
+def cfg : Plausible.Configuration := { plausibleDefaultConfig with quiet := true }
+
 --! The error monad for TensorLib
 abbrev Err := Except String
 
@@ -26,6 +38,29 @@ def dot [Add a][Mul a][Zero a] (x y : List a) : a := (x.zip y).foldl (fun acc (a
 
 def natDivCeil (num denom : Nat) : Nat := (num + denom - 1) / denom
 
+section Test
+
+#eval Testable.check (cfg := cfg) (
+  ∀ (x y : Nat),
+  let c := natDivCeil x y
+  let f := x / y
+  c == f || c == (f + 1)
+)
+
+local instance : SampleableExt (Nat × Nat) :=
+  SampleableExt.mkSelfContained do
+    let x ← SampleableExt.interpSample Nat
+    let n <- SampleableExt.interpSample Nat
+    return (x * n, x)
+
+#eval Testable.check (cfg := cfg) (
+  ∀ (xy : Nat × Nat),
+  let (x, y) := xy
+  x % y = 0 → x / y = natDivCeil x y
+)
+
+end Test
+
 def natProd (shape : List Nat) : Nat := shape.foldl (fun x y => x * y) 1
 
 

lake-manifest.json

@@ -11,24 +11,34 @@
    "inputRev": "v2.2.0-lv4.14.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.15.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "scope": "leanprover-community",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "TensorLib",

lakefile.lean

@@ -12,7 +12,10 @@ lean_exe "tensorlib" where
   root := `Main
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop" @ "master" -- 'master' rather than a tag is a workaround for segfault bug https://github.com/leanprover/lean4/issues/6518#issuecomment-2574607960
+  "https://github.com/leanprover-community/aesop" @ "v4.15.0"
+
+require plausible from git
+  "https://github.com/leanprover-community/plausible" @ "v4.15.0"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli.git" @ "v2.2.0-lv4.14.0-rc1"