From 63287596a0146e9064908235b4349f71f5237bb4 Mon Sep 17 00:00:00 2001 From: Billy Snikkers Date: Thu, 20 Aug 2026 15:49:37 +1000 Subject: [PATCH 1/3] RFC: state Mandelbrot connectedness in a trusted file via proof-only import Ray/Mandelbrot.lean becomes the trusted file: it defines mandelbrot itself and authors the connectedness statements, elaborated with only its own imports active (Trustless plus three basic Mathlib modules). The proofs arrive by trustless import from the new untrusted Ray/MandelbrotBridge, which repeats the definition, proves it equals multibrot 2, and transports isConnected_multibrot across. Every imported constant is re-checked by this toolchain's kernel against the trusted file's own definitions, so the import fails unless the bridge proved exactly the statements authored here. None of the bridge's notation, instances, or macros is activated in the trusted file, and its olean is never mapped into the elaborating process: lean4export walks it in a sandboxed subprocess and only text crosses back. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Kvxi5Pm1yyXH1mtDHXhEqq --- Ray/Mandelbrot.lean | 44 ++++++++++++++++------------------- Ray/MandelbrotBridge.lean | 48 +++++++++++++++++++++++++++++++++++++++ lake-manifest.json | 19 +++++++++++++++- lakefile.lean | 22 ++++++++++++++++-- 4 files changed, 105 insertions(+), 28 deletions(-) create mode 100644 Ray/MandelbrotBridge.lean diff --git a/Ray/Mandelbrot.lean b/Ray/Mandelbrot.lean index 6a66b2d..f707ec8 100644 --- a/Ray/Mandelbrot.lean +++ b/Ray/Mandelbrot.lean @@ -1,40 +1,34 @@ module -public import Ray.Multibrot.Defs -import Ray.Misc.Cobounded -import Ray.Multibrot.Basic -import Ray.Multibrot.Connected +import Trustless +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Topology.Connected.Basic +public import Mathlib.Order.Filter.AtTopBot.Basic /-! -## The Mandelbrot set and its complement are connected +# The Mandelbrot set and its complement are connected -The rest of our proof works via manifolds and other machinery. Here we strip that away: - -1. We define the Mandebrot set directly -2. We show it is equal to `multibrot 2` -3. Thus, the Mandelbrot set and its complement are connected +`mandelbrot` is defined here, and the proofs arrive via `trustless import` from +`Ray.MandelbrotBridge`: kernel-re-checked against this file's definitions, with +none of the bridge's notation, instances, or other elaborator surface active, +and without mapping its olean into this process. The bridge repeats the +definition; the re-check fails unless the copies agree. -/ open Filter (Tendsto atTop) -open RiemannSphere open Set -open scoped Topology Real noncomputable section -/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c` -/ +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ @[expose] public def mandelbrot : Set ℂ := {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} -/-- The Mandelbrot set is the `d = 2` Multibrot set -/ -public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by - ext c - simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, - tendsto_cobounded_iff_norm_tendsto_atTop] - rfl +trustless import Ray.MandelbrotBridge + (MandelbrotBridge.isConnected_mandelbrot MandelbrotBridge.isConnected_compl_mandelbrot) -/-- The Mandelbrot set is connected -/ -public theorem isConnected_mandelbrot : IsConnected mandelbrot := by - rw [mandelbrot_eq_multibrot]; exact isConnected_multibrot 2 +/-- The Mandelbrot set is connected. -/ +public theorem isConnected_mandelbrot : IsConnected mandelbrot := + MandelbrotBridge.isConnected_mandelbrot -/-- The complement of the Mandelbrot set is connected -/ -public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := by - rw [mandelbrot_eq_multibrot]; exact isConnected_compl_multibrot 2 +/-- The complement of the Mandelbrot set is connected. -/ +public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := + MandelbrotBridge.isConnected_compl_mandelbrot diff --git a/Ray/MandelbrotBridge.lean b/Ray/MandelbrotBridge.lean new file mode 100644 index 0000000..d6d2b94 --- /dev/null +++ b/Ray/MandelbrotBridge.lean @@ -0,0 +1,48 @@ +module + +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Topology.Connected.Basic +public import Mathlib.Order.Filter.AtTopBot.Basic +public import Ray.Multibrot.Defs +import Ray.Misc.Cobounded +import Ray.Multibrot.Basic +import Ray.Multibrot.Connected + +/-! +# Untrusted bridge: `mandelbrot` ⟶ Mathlib's `multibrot` + +Repeats the trusted `mandelbrot` definition (`Ray.Mandelbrot` does not import +this file), proves it equals `multibrot 2`, and transports Mathlib's +`isConnected_multibrot` across. `Ray.Mandelbrot` kernel-re-checks everything it +imports from here, so nothing in this file is trusted. +-/ + +open Filter (Tendsto atTop) +open RiemannSphere +open Set +open scoped Topology Real +noncomputable section + +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ +@[expose] public def mandelbrot : Set ℂ := + {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} + +-- Namespaced so the canonical names stay free for `Ray.Mandelbrot`. +namespace MandelbrotBridge + +/-- The trusted Mandelbrot set is the `d = 2` Multibrot set. -/ +public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by + ext c + simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, + tendsto_cobounded_iff_norm_tendsto_atTop] + rfl + +/-- The Mandelbrot set is connected. -/ +public theorem isConnected_mandelbrot : IsConnected mandelbrot := by + rw [mandelbrot_eq_multibrot]; exact isConnected_multibrot 2 + +/-- The complement of the Mandelbrot set is connected. -/ +public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := by + rw [mandelbrot_eq_multibrot]; exact isConnected_compl_multibrot 2 + +end MandelbrotBridge diff --git a/lake-manifest.json b/lake-manifest.json index 697a179..a9dfc30 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/mathlib4", + [{"type": "path", + "scope": "", + "name": "trustless", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../trustless", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", @@ -11,6 +18,16 @@ "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4export", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "15f6055e299ad5b89345e533cc2192f4cc00f659", + "name": "lean4export", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index de23a16..130adb3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,12 +4,30 @@ open Lake DSL package ray where leanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` - ⟨`linter.docPrime, false⟩, + ⟨`weak.linter.docPrime, false⟩, -- `weak.` so libs that don't import Mathlib (which defines this linter) don't error ⟨`autoImplicit, false⟩, ⟨`experimental.module, true⟩, ] require "leanprover-community" / "mathlib" @ git "v4.33.0" +require trustless from ".." / "trustless" + +-- `Ray.Mandelbrot`'s `trustless import` needs the bridge olean and the +-- lean4export binary, edges Lake cannot see; build them first. @[default_target] -lean_lib Ray +lean_lib Ray where + extraDepTargets := #[`RayMandelbrotBridge, `lean4exportBin] + +-- The lean4export exe as a package-local target (`extraDepTargets` cannot name +-- targets of other packages). +target lean4exportBin _pkg : System.FilePath := do + let some l4e := (← getWorkspace).packages.find? (·.name == `lean4export) + | error "lean4export package not found in workspace" + let some exe := l4e.findLeanExe? `lean4export + | error "lean4export executable target not found" + exe.exe.fetch + +-- The untrusted bridge, kept out of `Ray`'s import closure. +lean_lib RayMandelbrotBridge where + roots := #[`Ray.MandelbrotBridge] From 55a56680aef4e848a0e2a6446fccc77cc83715fc Mon Sep 17 00:00:00 2001 From: Billy Snikkers Date: Fri, 28 Aug 2026 16:19:16 +1000 Subject: [PATCH 2/3] RFC: contract-first trusted Mandelbrot via const_fill The trusted files live at the package root. Mandelbrot.lean defines mandelbrot, states the two connectedness theorems, and proves each with const_fill Ray.Mandelbrot (the provider defaults to the theorem's own name). Mandelbrot2.lean is the manual comparison via const import and namespaced re-authoring. The untrusted proofs live in Ray/Mandelbrot.lean and Ray/Mandelbrot2.lean (lib RayMandelbrotSource), replacing Ray/MandelbrotBridge.lean. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01Kvxi5Pm1yyXH1mtDHXhEqq --- Mandelbrot.lean | 59 +++++++++++++++++++ Mandelbrot2.lean | 30 ++++++++++ Ray/Mandelbrot.lean | 44 ++++++++------ ...MandelbrotBridge.lean => Mandelbrot2.lean} | 30 ++++------ lakefile.lean | 27 ++++----- 5 files changed, 138 insertions(+), 52 deletions(-) create mode 100644 Mandelbrot.lean create mode 100644 Mandelbrot2.lean rename Ray/{MandelbrotBridge.lean => Mandelbrot2.lean} (54%) diff --git a/Mandelbrot.lean b/Mandelbrot.lean new file mode 100644 index 0000000..8a1fcf2 --- /dev/null +++ b/Mandelbrot.lean @@ -0,0 +1,59 @@ +module +import Trustless +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Topology.Connected.Basic +public import Mathlib.Order.Filter.AtTopBot.Basic + +/-! +## The Mandelbrot set and its complement are connected (trustless) + +A verifier of `IsConnected mandelbrot` and `IsConnected mandelbrotᶜ` that does not +trust what the Ray library does while constructing a proof. +It does trust Mathlib and Trustless. + +const_fill: reads the named theorem's proof term and its dependency closure straight out of +`Ray.Mandelbrot`'s compiled olean, re-checks every constant through the kernel, and closes the +goal with the transplanted term, activating none of the library's elaboration (notation, +macros, instances). +trustless_fill: The same as above except the constants are extracted from lean4export, run in a +sandbox. +-/ + +open Filter (Tendsto atTop) +open Set +section + +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ +@[expose] public def mandelbrot : Set ℂ := + {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} + +/-- The Mandelbrot set is connected. -/ +public theorem isConnected_mandelbrot : IsConnected mandelbrot := + trustless_fill Ray.Mandelbrot + +/-- The complement of the Mandelbrot set is connected. -/ +public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := + trustless_fill Ray.Mandelbrot + +/-! +Appendix: + The meaning of the above theorems depends on `IsConnected` and the topology on ℂ is given by + an instance of `[TopologicalSpace ℂ]`. We prove they both have the usual meaning. +-/ + +/-- The topology on ℂ being used is the open ball topology -/ +example (u : Set ℂ) : IsOpen u ↔ ∀ z ∈ u, ∃ ε > 0, ∀ w : ℂ, ‖w - z‖ < ε → w ∈ u := by + simp only [Metric.isOpen_iff, subset_def, Metric.mem_ball, Complex.dist_eq] + +/-- `‖·‖` above is the ordinary modulus on `ℂ` -/ +example (z : ℂ) : ‖z‖ = Real.sqrt (z.re ^ 2 + z.im ^ 2) := Complex.norm_eq_sqrt_sq_add_sq z + +/-- IsConnected s means: s is non-empty, and if two open sets cover s + and each have nontrivial intersection with s, then so does their intersection. + -/ +example {α} [TopologicalSpace α] (s : Set α) : + IsConnected s ↔ + s.Nonempty ∧ + ∀ u v : Set α, IsOpen u → IsOpen v → s ⊆ u ∪ v → + (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty := + Iff.rfl diff --git a/Mandelbrot2.lean b/Mandelbrot2.lean new file mode 100644 index 0000000..7844857 --- /dev/null +++ b/Mandelbrot2.lean @@ -0,0 +1,30 @@ +module +import Trustless +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Topology.Connected.Basic +public import Mathlib.Order.Filter.AtTopBot.Basic + +/-! +const import pulls in constants without triggering elaboration (it also replays them into the +Kernel.Environment so they get rechecked again). +Use `trustless import` for a version that extracts a the constants from lean4export +running in a sandbox. + +Ray.Mandelbrot2 declares everything inside the `Ray` namespace, so that it doesn't collide with +our mandelbrot, isConnected_mandelbrot and isConnected_compl_mandelbrot. +-/ +const import Ray.Mandelbrot2 + +open Filter (Tendsto atTop) +open Set +section + +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ +@[expose] public def mandelbrot : Set ℂ := + {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} + +-- The Mandelbrot set is connected. +public theorem isConnected_mandelbrot : IsConnected mandelbrot := Ray.isConnected_mandelbrot + +-- The complement of the Mandelbrot set is connected. +public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := Ray.isConnected_compl_mandelbrot diff --git a/Ray/Mandelbrot.lean b/Ray/Mandelbrot.lean index f707ec8..6a66b2d 100644 --- a/Ray/Mandelbrot.lean +++ b/Ray/Mandelbrot.lean @@ -1,34 +1,40 @@ module -import Trustless -public import Mathlib.Analysis.Complex.Basic -public import Mathlib.Topology.Connected.Basic -public import Mathlib.Order.Filter.AtTopBot.Basic +public import Ray.Multibrot.Defs +import Ray.Misc.Cobounded +import Ray.Multibrot.Basic +import Ray.Multibrot.Connected /-! -# The Mandelbrot set and its complement are connected +## The Mandelbrot set and its complement are connected -`mandelbrot` is defined here, and the proofs arrive via `trustless import` from -`Ray.MandelbrotBridge`: kernel-re-checked against this file's definitions, with -none of the bridge's notation, instances, or other elaborator surface active, -and without mapping its olean into this process. The bridge repeats the -definition; the re-check fails unless the copies agree. +The rest of our proof works via manifolds and other machinery. Here we strip that away: + +1. We define the Mandebrot set directly +2. We show it is equal to `multibrot 2` +3. Thus, the Mandelbrot set and its complement are connected -/ open Filter (Tendsto atTop) +open RiemannSphere open Set +open scoped Topology Real noncomputable section -/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c` -/ @[expose] public def mandelbrot : Set ℂ := {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} -trustless import Ray.MandelbrotBridge - (MandelbrotBridge.isConnected_mandelbrot MandelbrotBridge.isConnected_compl_mandelbrot) +/-- The Mandelbrot set is the `d = 2` Multibrot set -/ +public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by + ext c + simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, + tendsto_cobounded_iff_norm_tendsto_atTop] + rfl -/-- The Mandelbrot set is connected. -/ -public theorem isConnected_mandelbrot : IsConnected mandelbrot := - MandelbrotBridge.isConnected_mandelbrot +/-- The Mandelbrot set is connected -/ +public theorem isConnected_mandelbrot : IsConnected mandelbrot := by + rw [mandelbrot_eq_multibrot]; exact isConnected_multibrot 2 -/-- The complement of the Mandelbrot set is connected. -/ -public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := - MandelbrotBridge.isConnected_compl_mandelbrot +/-- The complement of the Mandelbrot set is connected -/ +public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := by + rw [mandelbrot_eq_multibrot]; exact isConnected_compl_multibrot 2 diff --git a/Ray/MandelbrotBridge.lean b/Ray/Mandelbrot2.lean similarity index 54% rename from Ray/MandelbrotBridge.lean rename to Ray/Mandelbrot2.lean index d6d2b94..0966050 100644 --- a/Ray/MandelbrotBridge.lean +++ b/Ray/Mandelbrot2.lean @@ -1,20 +1,18 @@ +-- Same as Mandelbrot.lean but I put namespace Ray module - -public import Mathlib.Analysis.Complex.Basic -public import Mathlib.Topology.Connected.Basic -public import Mathlib.Order.Filter.AtTopBot.Basic public import Ray.Multibrot.Defs import Ray.Misc.Cobounded import Ray.Multibrot.Basic import Ray.Multibrot.Connected /-! -# Untrusted bridge: `mandelbrot` ⟶ Mathlib's `multibrot` +## The Mandelbrot set and its complement are connected + +The rest of our proof works via manifolds and other machinery. Here we strip that away: -Repeats the trusted `mandelbrot` definition (`Ray.Mandelbrot` does not import -this file), proves it equals `multibrot 2`, and transports Mathlib's -`isConnected_multibrot` across. `Ray.Mandelbrot` kernel-re-checks everything it -imports from here, so nothing in this file is trusted. +1. We define the Mandebrot set directly +2. We show it is equal to `multibrot 2` +3. Thus, the Mandelbrot set and its complement are connected -/ open Filter (Tendsto atTop) @@ -22,27 +20,23 @@ open RiemannSphere open Set open scoped Topology Real noncomputable section +namespace Ray -/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/ +/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c` -/ @[expose] public def mandelbrot : Set ℂ := {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop} --- Namespaced so the canonical names stay free for `Ray.Mandelbrot`. -namespace MandelbrotBridge - -/-- The trusted Mandelbrot set is the `d = 2` Multibrot set. -/ +/-- The Mandelbrot set is the `d = 2` Multibrot set -/ public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by ext c simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, tendsto_cobounded_iff_norm_tendsto_atTop] rfl -/-- The Mandelbrot set is connected. -/ +/-- The Mandelbrot set is connected -/ public theorem isConnected_mandelbrot : IsConnected mandelbrot := by rw [mandelbrot_eq_multibrot]; exact isConnected_multibrot 2 -/-- The complement of the Mandelbrot set is connected. -/ +/-- The complement of the Mandelbrot set is connected -/ public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := by rw [mandelbrot_eq_multibrot]; exact isConnected_compl_multibrot 2 - -end MandelbrotBridge diff --git a/lakefile.lean b/lakefile.lean index 130adb3..045ed5e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -13,21 +13,18 @@ require "leanprover-community" / "mathlib" @ git "v4.33.0" require trustless from ".." / "trustless" --- `Ray.Mandelbrot`'s `trustless import` needs the bridge olean and the --- lean4export binary, edges Lake cannot see; build them first. +-- The trusted `Mandelbrot`'s `const import` reads `Ray.Mandelbrot`'s olean, an +-- edge Lake cannot see; build it first. (`extraDepTargets` is best-effort +-- ordering; a cold build may need `lake build RayMandelbrotSource` first.) @[default_target] lean_lib Ray where - extraDepTargets := #[`RayMandelbrotBridge, `lean4exportBin] + -- `Mandelbrot` (the trusted file) lives at the package root, outside the `Ray` + -- namespace, so it must be named as a root for Lake to build it. + roots := #[`Ray, `Mandelbrot, `Mandelbrot2] + extraDepTargets := #[`RayMandelbrotSource] --- The lean4export exe as a package-local target (`extraDepTargets` cannot name --- targets of other packages). -target lean4exportBin _pkg : System.FilePath := do - let some l4e := (← getWorkspace).packages.find? (·.name == `lean4export) - | error "lean4export package not found in workspace" - let some exe := l4e.findLeanExe? `lean4export - | error "lean4export executable target not found" - exe.exe.fetch - --- The untrusted bridge, kept out of `Ray`'s import closure. -lean_lib RayMandelbrotBridge where - roots := #[`Ray.MandelbrotBridge] +-- The untrusted proof (`Ray.Mandelbrot`), kept out of `Ray`'s import closure so +-- its results arrive only through the trusted `Mandelbrot`'s `const import`, +-- never as a second copy. +lean_lib RayMandelbrotSource where + roots := #[`Ray.Mandelbrot, `Ray.Mandelbrot2] From 2c269c05da748c093e247322627da148d5df3027 Mon Sep 17 00:00:00 2001 From: Billy Snikkers Date: Fri, 28 Aug 2026 17:24:16 +1000 Subject: [PATCH 3/3] cleanup lakefile --- lakefile.lean | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 045ed5e..8eb2c79 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL package ray where leanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` - ⟨`weak.linter.docPrime, false⟩, -- `weak.` so libs that don't import Mathlib (which defines this linter) don't error + ⟨`weak.linter.docPrime, false⟩, -- `weak.`: defined by Mathlib, absent in libs that don't import it ⟨`autoImplicit, false⟩, ⟨`experimental.module, true⟩, ] @@ -13,18 +13,12 @@ require "leanprover-community" / "mathlib" @ git "v4.33.0" require trustless from ".." / "trustless" --- The trusted `Mandelbrot`'s `const import` reads `Ray.Mandelbrot`'s olean, an --- edge Lake cannot see; build it first. (`extraDepTargets` is best-effort --- ordering; a cold build may need `lake build RayMandelbrotSource` first.) @[default_target] lean_lib Ray where - -- `Mandelbrot` (the trusted file) lives at the package root, outside the `Ray` - -- namespace, so it must be named as a root for Lake to build it. roots := #[`Ray, `Mandelbrot, `Mandelbrot2] + -- The fills read the sources' oleans, an edge Lake cannot see; build them first. extraDepTargets := #[`RayMandelbrotSource] --- The untrusted proof (`Ray.Mandelbrot`), kept out of `Ray`'s import closure so --- its results arrive only through the trusted `Mandelbrot`'s `const import`, --- never as a second copy. +-- The untrusted proofs, kept out of `Ray`'s import closure. lean_lib RayMandelbrotSource where roots := #[`Ray.Mandelbrot, `Ray.Mandelbrot2]