diff --git a/FFI.lean b/FFI.lean index 75d1d9f..675ef9e 100644 --- a/FFI.lean +++ b/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 diff --git a/FFI/FMA.lean b/FFI/FMA.lean deleted file mode 100644 index f663f99..0000000 --- a/FFI/FMA.lean +++ /dev/null @@ -1,57 +0,0 @@ -/- -Copyright (c) 2026 Gaëtan Serré. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gaëtan Serré --/ -module - -prelude -public import Init.Data.Float.Model.Unpacked.Round - --- This file is part of the logical model for floats which authors of float libraries --- need to rely on. -@[expose] public section - -namespace Float.Model.UnpackedFloat - -/-- -Computes the fused multiply-add `x * y + z` of three floating point numbers and rounds the -result according to the given specification. The product `x * y` is exact and never rounded -on its own; only the final sum is rounded. --/ -def fma (spec : Format) : UnpackedFloat → UnpackedFloat → UnpackedFloat → UnpackedFloat - | .notANumber, _, _ => .notANumber - | _, .notANumber, _ => .notANumber - | _, _, .notANumber => .notANumber - | .zero _, .infinity _, _ => .notANumber - | .infinity _, .zero _, _ => .notANumber - | .infinity sign₁, .infinity sign₂, .infinity sign₃ => - if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber - | .infinity sign₁, .finite sign₂ .., .infinity sign₃ => - if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber - | .finite sign₁ .., .infinity sign₂, .infinity sign₃ => - if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber - | .infinity sign₁, .infinity sign₂, _ => .infinity (sign₁ * sign₂) - | .infinity sign₁, .finite sign₂ .., _ => .infinity (sign₁ * sign₂) - | .finite sign₁ .., .infinity sign₂, _ => .infinity (sign₁ * sign₂) - | _, _, .infinity sign₃ => .infinity sign₃ - | .zero sign₁, .zero sign₂, .zero sign₃ => - if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive - | .zero sign₁, .finite sign₂ .., .zero sign₃ => - if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive - | .finite sign₁ .., .zero sign₂, .zero sign₃ => - if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive - | .zero _, _, z => z - | _, .zero _, z => z - | .finite s₁ m₁ e₁ _, .finite s₂ m₂ e₂ _, .zero _ => - roundWithAccuracy spec (s₁ * s₂) (m₁ * m₂) (e₁ + e₂) .exact - | .finite s₁ m₁ e₁ _, .finite s₂ m₂ e₂ _, .finite s₃ m₃ e₃ _ => - let productMantissa := m₁ * m₂ - let productExponent := e₁ + e₂ - let smallerExponent := min productExponent e₃ - let (productMantissa, _) := decreaseExponent productMantissa productExponent smallerExponent - let (m₃, _) := decreaseExponent m₃ e₃ smallerExponent - let mantissa := (s₁ * s₂).apply productMantissa + s₃.apply m₃ - normalize spec mantissa smallerExponent .positive - -end Float.Model.UnpackedFloat diff --git a/FFI/Float.lean b/FFI/Float.lean index 292bb9f..b9fe61e 100644 --- a/FFI/Float.lean +++ b/FFI/Float.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 diff --git a/FFI/Float32.lean b/FFI/Float32.lean index d51bb0e..bc34676 100644 --- a/FFI/Float32.lean +++ b/FFI/Float32.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 diff --git a/FFI/Model/Float.lean b/FFI/Model/Float.lean deleted file mode 100644 index 4475657..0000000 --- a/FFI/Model/Float.lean +++ /dev/null @@ -1,24 +0,0 @@ -/- -Copyright (c) 2026 Gaëtan Serré. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gaëtan Serré --/ -module - -prelude -public import Init.Data.Float.Model.Float -public import FFI.FMA - --- This file is part of the logical model for floats which authors of float libraries --- need to rely on. -@[expose] public section - -namespace Float.Model - -/-- -Compute the fused multiply-add `a * b + c` of three `Float.Model`, with a single rounding. --/ -def fma (a b c : Float.Model) : Float.Model := - pack (UnpackedFloat.fma Format.binary64 a.unpack b.unpack c.unpack) - -end Float.Model diff --git a/FFI/Model/Float32.lean b/FFI/Model/Float32.lean deleted file mode 100644 index 04b6842..0000000 --- a/FFI/Model/Float32.lean +++ /dev/null @@ -1,26 +0,0 @@ -/- -Copyright (c) 2026 Gaëtan Serré. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gaëtan Serré --/ -module - -prelude -public import Init.Data.Float.Model.Float32 -public import FFI.FMA - --- This file is part of the logical model for floats which authors of float libraries --- need to rely on. -@[expose] public section - -namespace Float32.Model - -open Float.Model (Format UnpackedFloat) - -/-- -Compute the fused multiply-add `a * b + c` of three `Float32.Model`, with a single rounding. --/ -def fma (a b c : Float32.Model) : Float32.Model := - pack (UnpackedFloat.fma Format.binary32 a.unpack b.unpack c.unpack) - -end Float32.Model diff --git a/RandomDo/Measurable.lean b/RandomDo/Measurable.lean index 262db34..2aab168 100644 --- a/RandomDo/Measurable.lean +++ b/RandomDo/Measurable.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 diff --git a/lake-manifest.json b/lake-manifest.json index 3a05c19..6e83939 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -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} diff --git a/lean-toolchain b/lean-toolchain index d5ae4e3..e5b681c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc2 \ No newline at end of file +leanprover/lean4:v4.35.0-rc4 \ No newline at end of file