fix: repair many examples in manual to run in isolation (#617)

There are a few dozen `:::example` directives in the manual that won't
run correctly if you copy and paste them into
https://live.lean-lang.org/ . Fix them all, and include a CI check to
ensure that they are all fixes. A sampling of reasons include:
- `#check_decl` is defined in reference manual but not available in live
- `import`s of `Lean` or `Std` are missing
- `open`s prior to the `:::example` are necessary
- important definitions are in `+error` blocks and needed to be hoisted
.
Progress towards leanprover/verso#569 .

Author: jcreedcmu

.github/workflows/ci.yml

@@ -131,7 +131,7 @@ jobs:
             rm parse_times.py
           else
             echo "No build log found" >> $GITHUB_STEP_SUMMARY
-          fi            
+          fi
 
       - name: Save cache for .lake
         uses: actions/cache/save@v4
@@ -149,6 +149,10 @@ jobs:
         run: |
           lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single
 
+      - name: Check Manual Examples are Isolated
+        run: |
+          scripts/check-examples-isolated.sh
+
       - name: Generate proofreading HTML
         if: github.event_name == 'pull_request'
         id: generate
@@ -380,4 +384,3 @@ jobs:
         run: |
           cd _out/html-multi/-verso-search
           tsc --noEmit -p jsconfig.json
-

Manual/Axioms.lean

@@ -272,8 +272,8 @@ Consider the following three constants:
 
 ```lean
 def addThree (n : Nat) : Nat := 1 + n + 2
-theorem excludedMiddle (P : Prop) : P ∨ ¬ P := Classical.em P
-theorem simpleEquality (P : Prop) : (P ∨ False) = P := or_false P
+theorem excluded_middle (P : Prop) : P ∨ ¬ P := Classical.em P
+theorem simple_equality (P : Prop) : (P ∨ False) = P := or_false P
 ```
 
 Regular functions like {lean}`addThree` that we might want to actually evaluation typically do not depend on any axioms:
@@ -288,35 +288,40 @@ Regular functions like {lean}`addThree` that we might want to actually evaluatio
 The excluded middle theorem is only true if we use classical reasoning, so the foundation for classical reasoning shows up alongside other axioms:
 
 ```lean (name := printAxEx1)
-#print axioms excludedMiddle
+#print axioms excluded_middle
 ```
 ```leanOutput printAxEx1
-'excludedMiddle' depends on axioms: [propext, Classical.choice, Quot.sound]
+'excluded_middle' depends on axioms: [propext, Classical.choice, Quot.sound]
 ```
 
 Finally, the idea that two equivalent propositions are equal directly relies on {tech}[propositional extensionality].
 
 ```lean (name := printAxEx3)
-#print axioms simpleEquality
+#print axioms simple_equality
 ```
 ```leanOutput printAxEx3
-'simpleEquality' depends on axioms: [propext]
+'simple_equality' depends on axioms: [propext]
 ```
 :::
 
 :::example "Using {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` with {keywordOf Lean.guardMsgsCmd}`#guard_msgs`"
 
-You can use {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` together with {keywordOf Lean.guardMsgsCmd}`#guard_msgs` to ensure that updates to libraries from other projects cannot silently introduce unwanted dependencies on axioms.
+You can use {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`
+together with {keywordOf Lean.guardMsgsCmd}`#guard_msgs` to ensure
+that updates to libraries from other projects cannot silently
+introduce unwanted dependencies on axioms.
 
-Perhaps you are worried that some future update to {lean}`or_false` in the previous example's {lean}`simpleEquality` proof might quietly introduce a new axiom dependency.
-You can guard against this by writing a command that will fail if {lean}`simpleEquality` uses any axioms besides {lean}`propext`:
+For example, if the proof of {name}`double_neg_elim` below changed in such a way that it used more
+axioms than those listed, then the {keywordOf Lean.guardMsgsCmd}`#guard_msgs` would report an error.
 
 ```lean
-/--
-info: 'simpleEquality' depends on axioms: [propext]
--/
+theorem double_neg_elim (P : Prop) : (¬ ¬ P) = P :=
+  propext Classical.not_not
+
+/-- info: 'double_neg_elim' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in
-#print axioms simpleEquality
+#print axioms double_neg_elim
+
 ```
 :::
 

Manual/BasicTypes/BitVec.lean

@@ -170,6 +170,10 @@ The resulting proofs rely only on the axiom {name}`Lean.ofReduceBool`; the exter
 
 :::example "Popcount"
 
+```imports
+import Std.Tactic.BVDecide
+```
+
 The function {lean}`popcount` returns the number of set bits in a bitvector.
 It can be implemented as a 32-iteration loop that tests each bit, incrementing a counter if the bit is set:
 

Manual/BasicTypes/Maps.lean

@@ -7,6 +7,7 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Manual.Meta
+import Manual.Meta.ImportsBlock
 
 import Manual.BasicTypes.Maps.TreeSet
 import Manual.BasicTypes.Maps.TreeMap
@@ -176,6 +177,10 @@ A nested inductive type that occurs inside a map or set should be defined in thr
 
 :::example "Nested Inductive Types with `Std.HashMap`"
 
+```imports
+import Std
+```
+
 This example requires that `Std.Data.HashMap.RawLemmas` is imported.
 To keep the code shorter, the `Std` namespace is opened:
 ```lean
@@ -305,6 +310,10 @@ These operations avoid creating a second reference to the value during modificat
 
 :::example "Modifying Values in Maps"
 
+```imports
+import Std
+```
+
 ```lean
 open Std
 ```

Manual/BasicTypes/Option.lean

@@ -38,6 +38,10 @@ The {lean}`Option` API makes frequent use of this perspective.
 
 :::example "Options as Nullability"
 
+```imports
+import Std
+```
+
 ```lean -show
 open Std (HashMap)
 variable {Coll} [BEq α] [Hashable α] (a : α) (b : β) {xs : Coll} [GetElem Coll α β fun _ _ => True] {i : α} {m : HashMap α β}
@@ -64,6 +68,10 @@ In many programming languages, it is important to remember to check for the null
 When using {name}`Option`, the type system requires these checks in the right places: {lean}`Option α` and {lean}`α` are not the same type, and converting from one to the other requires handling the case of {lean  (type := "Option α")}`none`.
 This can be done via helpers such as {name}`Option.getD`, or with pattern matching.
 
+```imports
+import Std
+```
+
 ```lean
 def postalCodes : Std.HashMap Nat String :=
   .empty |>.insert 12345 "Schenectady"

Manual/Classes/DerivingHandlers.lean

@@ -96,6 +96,11 @@ Lean includes deriving handlers for the following classes:
 
 ::::keepEnv
 :::example "Deriving Handlers"
+
+```imports
+import Lean.Elab
+```
+
 Instances of the {name}`IsEnum` class demonstrate that a type is a finite enumeration by providing a bijection between the type and a suitably-sized {name}`Fin`:
 ```lean
 class IsEnum (α : Type) where

Manual/Coercions.lean

@@ -168,7 +168,7 @@ def Bin.ofNat (n : Nat) : Bin :=
   | n + 1 => (Bin.ofNat n).succ
 ```
 
-```lean -show
+```lean -show -keep
 --- Internal tests
 /-- info: [0, 1, 10, 11, 100, 101, 110, 111, 1000] -/
 #check_msgs in
@@ -182,7 +182,8 @@ def Bin.ofNat (n : Nat) : Bin :=
   Bin.done.succ.succ.succ.succ.succ.succ,
   Bin.done.succ.succ.succ.succ.succ.succ.succ,
   Bin.done.succ.succ.succ.succ.succ.succ.succ.succ]
-
+```
+```lean -show
 def Bin.toNat : Bin → Nat
   | .done => 0
   | .zero b => 2 * b.toNat
@@ -206,12 +207,13 @@ theorem Bin.ofNat_toNat_eq {n : Nat} : (Bin.ofNat n).toNat = n := by
 
 
 Even if {lean}`Bin.ofNat` is registered as a coercion, natural number literals cannot be used for {lean}`Bin`:
-```lean (name := nineFail) +error
+```lean
 attribute [coe] Bin.ofNat
 
 instance : Coe Nat Bin where
   coe := Bin.ofNat
-
+```
+``` lean (name := nineFail) +error
 #eval (9 : Bin)
 ```
 ```leanOutput nineFail

Manual/Grind.lean

@@ -104,6 +104,9 @@ example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) :
 
 This proof uses {tactic}`grind`'s commutative ring solver.
 
+```lean -show
+open Lean.Grind
+```
 ```lean
 example [CommRing α] [NoNatZeroDivisors α] (a b c : α) :
     a + b + c = 3 →

Manual/Grind/Algebra.lean

@@ -37,6 +37,9 @@ open Lean Grind
 ```
 
 :::example "Commutative Rings" (open := true)
+```lean -show
+open Lean.Grind
+```
 ```lean
 example [CommRing α] (x : α) : (x + 1) * (x - 1) = x ^ 2 - 1 := by
   grind
@@ -45,6 +48,9 @@ example [CommRing α] (x : α) : (x + 1) * (x - 1) = x ^ 2 - 1 := by
 :::example "Ring Characteristics" (open := true)
 The solver “knows” that `16*16 = 0` because the [ring characteristic](https://en.wikipedia.org/wiki/Characteristic_%28algebra%29) (that is, the minimum number of copies of the multiplicative identity that sum to the additive identity) is `256`, which is provided by the {name}`IsCharP` instance.
 
+```lean -show
+open Lean.Grind
+```
 ```lean
 example [CommRing α] [IsCharP α 256] (x : α) :
     (x + 16)*(x - 16) = x^2 := by
@@ -53,6 +59,9 @@ example [CommRing α] [IsCharP α 256] (x : α) :
 :::
 
 :::example "Standard Library Types" (open := true)
+```lean -show
+open Lean.Grind
+```
 Types in the standard library are supported by the solver out of the box.
 `UInt8` is a commutative ring with characteristic `256`, and thus has instances of {inst}`CommRing UInt8` and {inst}`IsCharP UInt8 256`.
 ```lean
@@ -62,6 +71,9 @@ example (x : UInt8) : (x + 16) * (x - 16) = x ^ 2 := by
 :::
 
 :::example "More Commutative Ring Proofs" (open := true)
+```lean -show
+open Lean.Grind
+```
 The axioms of a commutative ring are sufficient to prove these statements.
 
 ```lean
@@ -83,6 +95,9 @@ example [CommRing α] (x y : α) :
 :::
 
 :::example "Characteristic Zero" (open := true)
+```lean -show
+open Lean.Grind
+```
 `ring` proves that `a + 1 = 2 + a` is unsatisfiable because the characteristic is known to be 0.
 
 ```lean
@@ -93,6 +108,9 @@ example [CommRing α] [IsCharP α 0] (a : α) :
 :::
 
 :::example "Inferred Characteristic" (open := true)
+```lean -show
+open Lean.Grind
+```
 Even when the characteristic is not initially known, when `grind` discovers that `n = 0` for some numeral `n`, it makes inferences about the characteristic:
 ```lean
 example [CommRing α] (a b c : α)
@@ -163,7 +181,9 @@ It also rewrites every disequality `p ≠ 0` as the equality `p * p⁻¹ = 1`.
 :::
 
 ::::example "Fields and `grind`"
-
+```lean -show
+open Lean.Grind
+```
 This example requires its {name}`Field` instance:
 
 ```lean
@@ -198,6 +218,9 @@ For example, the polynomial `2 * x * y + 4 * z = 0` is simplified to `x * y + 2
 It also used when processing disequalities.
 
 :::example "Using `NoNatZeroDivisors`"
+```lean -show
+open Lean.Grind
+```
 In this example, {tactic}`grind` relies on the {name}`NoNatZeroDivisors` instance to simplify the goal:
 ```lean
 example [CommRing α] [NoNatZeroDivisors α] (a b : α) :
@@ -310,6 +333,9 @@ example (x y : Nat) :
 Gröbner basis computation can be very expensive. You can limit the number of steps performed by the `ring` solver using the option `grind (ringSteps := <num>)`
 
 :::example "Limiting `ring` Steps"
+```lean -show
+open Lean.Grind
+```
 This example cannot be solved by performing at most 100 steps:
 ```lean +error (name := ring100)
 example [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α) :

Manual/Grind/Linarith.lean

@@ -38,6 +38,12 @@ It can be disabled using the option `grind -linarith`.
 
 
 :::example "Goals Decided by `linarith`" (open := true)
+```imports
+import Std
+```
+```lean -show
+open Lean.Grind
+```
 All of these examples rely on instances of the following ordering notation and `linarith` classes:
 ```lean
 variable [LE α] [LT α] [Std.LawfulOrderLT α]  [Std.IsLinearOrder α]
@@ -69,7 +75,12 @@ example {a b c d e : α} :
 :::
 
 :::example "Commutative Ring Goals Decided by `linarith`" (open := true)
-
+```imports
+import Std
+```
+```lean -show
+open Lean.Grind
+```
 For types that are commmutative rings (that is, types in which the multiplication operator is commutative) with {name}`CommRing` instances, `linarith` has more capabilities.
 
 ```lean