Merge pull request #14 from LeanMachineLearning/bump

Update dependencies

Author: RemyDegenne

FFI.lean

@@ -1,7 +1,4 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import FFI.FMA
 public import FFI.Float
 public import FFI.Float32
-public import FFI.Model.Float
-public import FFI.Model.Float32

FFI/FMA.lean

@@ -7,23 +7,11 @@ module
 
 prelude
 public import Init.Data.Float.Float
-public import FFI.Model.Float
 
 @[expose] public section
 
 namespace Float
 
-/--
-Computes the fused multiply-add `x * y + z` of three floating-point numbers. This operation is
-performed with a single rounding, which can be more accurate than performing the multiplication and
-addition separately.
-
-This function has a logical model in terms of `Float.Model`. It is implemented in compiled code by
-the C function `fma`.
--/
-@[extern "fma"] def fma : Float → Float → Float → Float :=
-  fun x y z => .ofModel (x.toModel.fma y.toModel z.toModel)
-
 /-- `log (1 + x)`, the C99 `log1p`, accurate for small `x` where `log (1 + x)` loses the leading
 digits of the result to the rounding of `1 + x`. -/
 @[extern "log1p"] opaque log1p (x : Float) : Float

FFI/Float.lean

@@ -7,21 +7,11 @@ module
 
 prelude
 public import Init.Data.Float.Float32
-public import FFI.Model.Float32
 
 @[expose] public section
 
 namespace Float32
 
-/--
-Computes the fused multiply-add `x * y + z` of three floating-point numbers. This operation is performed with a single rounding, which can be more accurate than performing the multiplication and addition separately.
-
-This function has a logical model in terms of `Float32.Model`. It is implemented in compiled code
-by the C function `fmaf`.
--/
-@[extern "fmaf"] def fma : Float32 → Float32 → Float32 → Float32 :=
-  fun x y z => .ofModel (x.toModel.fma y.toModel z.toModel)
-
 /-- `log (1 + x)`, the C99 `log1p`, accurate for small `x` where `log (1 + x)` loses the leading
 digits of the result to the rounding of `1 + x`. -/
 @[extern "log1pf"] opaque log1p (x : Float32) : Float32

FFI/Float32.lean

@@ -53,7 +53,7 @@ lemma measurable_ofFn (n : ℕ) : Measurable (List.ofFn : (Fin n → α) → Lis
 @[fun_prop]
 lemma measurable_finCons {n : ℕ} :
     Measurable fun q : α × (Fin n → α) ↦ (Fin.cons q.1 q.2 : Fin (n + 1) → α) := by
-  refine measurable_pi_lambda _ fun i ↦ ?_
+  refine Measurable.of_eval fun i ↦ ?_
   refine Fin.cases ?_ (fun j ↦ ?_) i
   · simp only [Fin.cons_zero]; fun_prop
   · simp only [Fin.cons_succ]; fun_prop

FFI/Model/Float.lean

@@ -1,11 +1,11 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/LeanMachineLearning/LML",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f86702d123689bc1739b65862132d4625a051843",
+   "rev": "288183ac4ad486e094959709b0967c910df9ffa0",
    "name": "LeanMachineLearning",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,27 +15,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf65d43b4f5e1a79482e8c488d121853b9d7ca05",
+   "rev": "41d048456026a1e519fbc9f74b3734eccc4c8556",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "cf65d43b4f5e1a79482e8c488d121853b9d7ca05",
+   "inputRev": "41d048456026a1e519fbc9f74b3734eccc4c8556",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3bdedf29bada13d8103e6c979001c51dcee210c8",
+   "rev": "01a09f320122475119588526857a07d218aef600",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.35.0-rc4",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
+   "rev": "aef59637faa9e85fa2486acaaf906ce3f572af7c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba67e212be1197b84c1f1f6299488a10a3002713",
+   "rev": "234d9e074fbd6e911b920baf32db5291c3125be0",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d8823026ac7ef130c253089d95685f9877b95323",
+   "rev": "80a81552bef492cc13d69cc7abddb61c29abbba3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f",
+   "rev": "d5ad4a0b79fa7f9818fe1380d05a3f6143823c09",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3",
+   "rev": "04879b1e1de744d5c9777c8cf63fa55a8f652e5e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
+   "rev": "e7c4cdd2f1bf9df361ef7f621b4d6867012ab65e",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,17 +95,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d54dddc581e08be364c278052863524bff7a99a9",
+   "rev": "9bfcda9fca2e9438b8a77b6e61e5880f69a82540",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "82c11b9717083154aefc5fe8d4cba4bbf046298f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.35.0-rc4",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6bc815869cba1f19515715dc6b47795acd521f1c",
+   "rev": "86aa7e62f42b2a82daf9692b191febde1f3d65f9",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,22 +135,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3a75ede05278806fd3249bb0c97a6fb5777a4f7d",
+   "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0-rc2",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "RandomDo",
  "lakeDir": ".lake",
  "fixedToolchain": false}

FFI/Model/Float32.lean

@@ -1 +1 @@
-leanprover/lean4:v4.34.0-rc2
+leanprover/lean4:v4.35.0-rc4