chore: update expected test files

Author: insightmind

test/dep/Dep.lean.leanInk.expected

@@ -1,5 +1,5 @@
 [{"contents":
-  "import Mathlib.Tactic.Basic\n\nexample : ∀ a b : Nat, a = b → b = a := by\n  ",
+  "import Mathlib.Tactic.Basic\n\nset_option trace.Elab.info true\n\nexample : ∀ a b : Nat, a = b → b = a := by\n  ",
   "_type": "text"},
  {"messages": [],
   "goals":

test/dep/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2021-12-26
+leanprover/lean4:nightly-2022-01-06

test/playground/Function.lean.leanInk.expected

@@ -62,5 +62,5 @@
   "_type": "sentence"},
  {"messages": [], "goals": [], "contents": "]", "_type": "sentence"},
  {"contents":
-  "\n\ntheorem injective_id : injective (@id α) := id\n\ntheorem surjective_id : surjective (@id α) := λ a => ⟨a, rfl⟩\n\ntheorem bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩\n\nend Function\n\nnamespace Function\n\nvariable {α : Type u₁} {β : Type u₂} {φ : Type u₃}\n\n/-- Interpret a function on `α × β` as a function with two arguments. -/\n@[inline] def curry : (α × β → φ) → α → β → φ :=\nλ f a b => f (a, b)\n\n/-- Interpret a function with two arguments as a function on `α × β` -/\n@[inline] def",
+  "\n\ntheorem injective_id : injective (@id α) := id\n\ntheorem surjective_id : surjective (@id α) := λ a => ⟨a, rfl⟩\n\ntheorem bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩\n\nend Function\n\nnamespace Function\n\nvariable {α : Type u₁} {β : Type u₂} {φ : Type u₃}\n\n/-- Interpret a function on `α × β` as a function with two arguments. -/\n@[inline] def curry : (α × β → φ) → α → β → φ :=\nλ f a b => f (a, b)\n\n/-- Interpret a function with two arguments as a function on `α × β` -/\n@[inline] def uncurry : (α → β → φ) → α × β → φ :=\nλ f a => f a.1 a.2\n\n@[simp] theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=\nrfl\n\n@[simp] theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=\nfunext (λ ⟨a, b⟩ => rfl)\n\nprotected theorem left_inverse.id {g : β → α} {f : α → β} (h : left_inverse g f) : g ∘ f = id :=\nfunext h\n\nprotected theorem right_inverse.id {g : β → α} {f : α → β} (h : right_inverse g f) : f ∘ g = id :=\nfunext h\n\nend Function\n",
   "_type": "text"}]

test/playground/infoTree.lean.leanInk.expected

@@ -11,4 +11,4 @@
   "goals": [],
   "contents": "#print",
   "_type": "sentence"},
- {"contents": " xor\ninstance : Inhabited", "_type": "text"}]
+ {"contents": " xor\ninstance : Inhabited Nat where\n\nmacro", "_type": "text"}]

test/test.sh

@@ -43,10 +43,10 @@ run_leanink () {
     # If the folder in which the file resides contains a lakefile we will use it to resolve any dependencies for the file
     if [[ -f "$directory/lakefile.lean" ]]; then
         echo "Running LeanInk with lakefile.lean - $file"
-        (cd $directory && $LEANINK analyze $filename --lake lakefile.lean) || error "LeanInk failed - $file"
+        (cd $directory && $LEANINK analyze $filename --lake lakefile.lean --verbose) || error "LeanInk failed - $file"
     else
         echo "Running LeanInk - $file"
-        (cd $directory && $LEANINK analyze $filename) || error "LeanInk failed - $file"
+        (cd $directory && $LEANINK analyze $filename --verbose) || error "LeanInk failed - $file"
     fi
 }
 

test/theorem_proving/005.lean.leanInk.expected

@@ -33,4 +33,4 @@
   "goals": [],
   "contents": "#check",
   "_type": "sentence"},
- {"contents": "", "_type": "text"}]
+ {"contents": " And", "_type": "text"}]

test/theorem_proving/007.lean.leanInk.expected

@@ -44,4 +44,4 @@
  {"messages": [], "goals": [], "contents": "exact hp", "_type": "sentence"},
  {"contents": "\n  case left => ", "_type": "text"},
  {"messages": [], "goals": [], "contents": "exact hp", "_type": "sentence"},
- {"contents": "", "_type": "text"}]
+ {"contents": "\n", "_type": "text"}]