chore: bump to nightly-2025-06-23 (#477)

Author: david-christiansen

Manual/Axioms.lean

@@ -147,7 +147,7 @@ partial def List.length' : List α → Nat
   | _ :: xs => xs.length' + 1
 ```
 ```leanOutput otherZero2
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.otherZero', and it does not have executable code
+axiom 'Nat.otherZero' not supported by code generator; consider marking definition as 'noncomputable'
 ```
 
 Axioms used in proofs rather than programs do not prevent a function from being compiled.

Manual/BasicProps.lean

@@ -418,9 +418,9 @@ end
 
 :::::leanSection
 ::::example "Heterogeneous Equality"
-````lean (show := false)
+```lean (show := false)
 variable {α : Type u} {n k l₁ l₂ l₃ : Nat}
-````
+```
 
 The type {lean}`Vector α n` is wrapper around an {lean}`Array α` that includes a proof that the array has size {lean}`n`.
 Appending {name}`Vector`s is associative, but this fact cannot be straightforwardly stated using ordinary propositional equality:

Manual/BasicTypes/Array/FFI.lean

@@ -33,17 +33,17 @@ The representation of arrays in C. See {ref "array-runtime"}[the description of
 :::
 
 :::ffi "lean_is_array"
-````
+```
 bool lean_is_array(lean_object * o)
-````
+```
 
 Returns `true` if `o` is an array, or `false` otherwise.
 :::
 
 :::ffi "lean_to_array"
-````
+```
 lean_array_object * lean_to_array(lean_object * o)
-````
+```
 Performs a runtime check that `o` is indeed an array. If `o` is not an array, an assertion fails.
 :::
 

Manual/BasicTypes/Maps.lean

@@ -195,7 +195,12 @@ structure Maze where
 This definition is rejected:
 
 ```leanOutput badNesting
-(kernel) arg #1 of '_nested.Std.HashMap_1.mk' contains a non valid occurrence of the datatypes being declared
+(kernel) application type mismatch
+  DHashMap.Raw.WF inner
+argument has type
+  _nested.Std.DHashMap.Raw_3
+but function has type
+  (DHashMap.Raw String fun x => Maze) → Prop
 ```
 
 Making this work requires separating the well-formedness predicates from the structure.

Manual/BasicTypes/String/FFI.lean

@@ -37,17 +37,17 @@ The representation of strings in C. See {ref "string-runtime"}[the description o
 :::
 
 :::ffi "lean_is_string"
-````
+```
 bool lean_is_string(lean_object * o)
-````
+```
 
 Returns `true` if `o` is a string, or `false` otherwise.
 :::
 
 :::ffi "lean_to_string"
-````
+```
 lean_string_object * lean_to_string(lean_object * o)
-````
+```
 Performs a runtime check that `o` is indeed a string. If `o` is not a string, an assertion fails.
 :::
 

Manual/BasicTypes/UInt.lean

@@ -103,7 +103,7 @@ def Permissions.decode (i : UInt8) : Permissions :=
 theorem Permissions.decode_encode (p : Permissions) : p = .decode (p.encode) := by
   let ⟨r, w, x⟩ := p
   cases r <;> cases w <;> cases x <;>
-  simp +decide [encode, decode]
+  simp +decide [decode]
 ```
 :::
 

Manual/BuildTools/Lake.lean

@@ -479,7 +479,7 @@ Because they are Lean definitions, Lake scripts can only be defined in the Lean
 
 Restore the following once we can import enough of Lake to elaborate it
 
-`````
+````
 ```lean (show := false)
 section
 open Lake DSL
@@ -507,7 +507,7 @@ script "list-deps" := do
 ```lean (show := false)
 end
 ```
-`````
+````
 
 :::::
 
@@ -525,7 +525,7 @@ Lint drivers may be executables or scripts, which are run by {lake}`lint`.
 A test or lint driver can be configured by either setting the {tomlField Lake.PackageConfig}`testDriver` or {tomlField Lake.PackageConfig}`lintDriver` package configuration options or by tagging a script, executable, or library with the `test_driver` or `lint_driver` attribute in a Lean-format configuration file.
 A definition in a dependency can be used as a test or lint driver by using the `<pkg>/<name>` syntax for the appropriate configuration option.
 :::TODO
-Restore the ``{attr}`` role for `test_driver` and `lint_driver` above. Right now, importing the attributes crashes the compiler.
+Restore the `{attr}` role for `test_driver` and `lint_driver` above. Right now, importing the attributes crashes the compiler.
 :::
 
 ## GitHub Release Builds

Manual/BuildTools/Lake/CLI.lean

@@ -918,7 +918,7 @@ Other hosts are not yet supported.
 
 ## Cached Cloud Builds
 
-**These commands are still experimental.**
+*These commands are still experimental.*
 They are likely change in future versions of Lake based on user feedback.
 Packages that use Reservoir cloud build archives should enable the {tomlField Lake.PackageConfig}`platformIndependent` setting.
 

Manual/Classes.lean

@@ -158,7 +158,7 @@ use the command `set_option checkBinderAnnotations false` to disable the check
 
 ::::example "Class vs Structure Constructors"
 A very small algebraic hierarchy can be represented either as structures ({name}`S.Magma`, {name}`S.Semigroup`, and {name}`S.Monoid` below), a mix of structures and classes ({name}`C1.Monoid`), or only using classes ({name}`C2.Magma`, {name}`C2.Semigroup`, and {name}`C2.Monoid`):
-````lean
+```lean
 namespace S
 structure Magma (α : Type u) where
   op : α → α → α
@@ -191,7 +191,7 @@ class Monoid (α : Type u) extends Semigroup α where
   ident_left : ∀ x, op ident x = x
   ident_right : ∀ x, op x ident = x
 end C2
-````
+```
 
 
 {name}`S.Monoid.mk` and {name}`C1.Monoid.mk` have identical signatures, because the parent of the class {name}`C1.Monoid` is not itself a class:
@@ -257,7 +257,7 @@ Two instances of the same class with the same parameters are not necessarily ide
 ::::example "Instances are Not Unique"
 
 This implementation of binary heap insertion is buggy:
-````lean
+```lean
 structure Heap (α : Type u) where
   contents : Array α
 deriving Repr
@@ -274,7 +274,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
 def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
   let i := xs.contents.size
   {xs with contents := xs.contents.push x}.bubbleUp i
-````
+```
 
 The problem is that a heap constructed with one {name}`Ord` instance may later be used with another, leading to the breaking of the heap invariant.
 
@@ -283,7 +283,9 @@ One way to correct this is to making the heap type depend on the selected `Ord`
 structure Heap' (α : Type u) [Ord α] where
   contents : Array α
 
-def Heap'.bubbleUp [inst : Ord α] (i : Nat) (xs : @Heap' α inst) : @Heap' α inst :=
+def Heap'.bubbleUp [inst : Ord α]
+    (i : Nat) (xs : @Heap' α inst) :
+    @Heap' α inst :=
   if h : i = 0 then xs
   else if h : i ≥ xs.contents.size then xs
   else

Manual/Coercions.lean

@@ -354,7 +354,7 @@ def tomorrow : Later String :=
 section
 variable {α : Type u}
 ```
-:::example "Duplicate Evaluation in Coercions"
+::::example "Duplicate Evaluation in Coercions"
 Because the contents of {lean}`Coe` instances are unfolded during coercion insertion, coercions that use their argument more than once should be careful to ensure that evaluation occurs just once.
 This can be done by using a helper function that is not part of the instance, or by using {keywordOf Lean.Parser.Term.let}`let` to evaluate the coerced term and then re-use its resulting value.
 
@@ -378,47 +378,58 @@ def twice (x : α) : Twice α where
 instance : Coe α (Twice α) := ⟨twice⟩
 ```
 When the {name}`Coe` instance is unfolded, the call to {name}`twice` remains, which causes its argument to be evaluated before the body of the function is executed.
-As a result, the {keywordOf Lean.Parser.Term.dbgTrace}`dbg_trace` executes just once:
+As a result, the {keywordOf Lean.Parser.Term.dbgTrace}`dbg_trace` is included in the resulting term just once:
 ```lean (name := eval1)
-#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
+#check ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
 ```
+:::comment
+This used to demonstrate the effect:
 ```leanOutput eval1
 hello
 ```
+:::
 ```leanOutput eval1
-{ first := 5, second := 5, first_eq_second := _ }
+↑(dbgTrace (toString "hello") fun x => 5) : Twice Nat
 ```
 
 Inlining the helper into the {name}`Coe` instance results in a term that duplicates the {keywordOf Lean.Parser.Term.dbgTrace}`dbg_trace`:
 ```lean (name := eval2)
 instance : Coe α (Twice α) where
   coe x := ⟨x, x, rfl⟩
 
-#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
+#check ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
 ```
+:::comment
+This used to check the effects, but can't in the new codegen
 ```leanOutput eval2
 hello
 hello
 ```
+:::
 ```leanOutput eval2
-{ first := 5, second := 5, first_eq_second := _ }
+{ first := dbgTrace (toString "hello") fun x => 5, second := dbgTrace (toString "hello") fun x => 5,
+  first_eq_second := ⋯ } : Twice Nat
 ```
 
-Introducing an intermediate name for the result of the evaluation prevents the duplicated work:
+Introducing an intermediate name for the result of the evaluation prevents the duplication of {keywordOf Lean.Parser.Term.dbgTrace}`dbg_trace`:
 ```lean (name := eval3)
 instance : Coe α (Twice α) where
   coe x := let y := x; ⟨y, y, rfl⟩
 
-#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
+#check ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
 ```
+:::comment
+This also checked the effects
 ```leanOutput eval3
 hello
 ```
+:::
 ```leanOutput eval3
-{ first := 5, second := 5, first_eq_second := _ }
+let y := dbgTrace (toString "hello") fun x => 5;
+{ first := y, second := y, first_eq_second := ⋯ } : Twice Nat
 ```
 
-:::
+::::
 ```lean (show := false)
 end
 ```
@@ -485,12 +496,12 @@ Non-dependent coercions are used whenever all values of the inferred type can be
 
 :::example "Defining Dependent Coercions"
 The string "four" can be coerced into the natural number {lean type:="Nat"}`4` with this instance declaration:
-````lean (name := fourCoe)
+```lean (name := fourCoe)
 instance : CoeDep String "four" Nat where
   coe := 4
 
 #eval ("four" : Nat)
-````
+```
 ```leanOutput fourCoe
 4
 ```