Merge pull request #35 from abdoo8080/patch-1

Delete profile messages.

Auto/Tactic.lean

@@ -476,7 +476,6 @@ def runAuto
 @[tactic auto]
 def evalAuto : Tactic
 | `(auto | auto $instr $hints $[$uords]*) => withMainContext do
-  let startTime ← IO.monoMsNow
   -- Suppose the goal is `∀ (x₁ x₂ ⋯ xₙ), G`
   -- First, apply `intros` to put `x₁ x₂ ⋯ xₙ` into the local context,
   --   now the goal is just `G`
@@ -492,7 +491,6 @@ def evalAuto : Tactic
       let (lemmas, inhFacts) ← collectAllLemmas hints uords (goalBinders.push ngoal)
       let declName? ← Elab.Term.getDeclName?
       let proof ← runAuto declName? lemmas inhFacts
-      IO.println s!"Auto found proof. Time spent by auto : {(← IO.monoMsNow) - startTime}ms"
       absurd.assign proof
     | .useSorry =>
       let proof ← Meta.mkAppM ``sorryAx #[Expr.const ``False [], Expr.const ``false []]
@@ -562,7 +560,6 @@ def runNativeProverWithAuto
 @[tactic mononative]
 def evalMonoNative : Tactic
 | `(mononative | mononative $hints $[$uords]*) => withMainContext do
-  let startTime ← IO.monoMsNow
   -- Suppose the goal is `∀ (x₁ x₂ ⋯ xₙ), G`
   -- First, apply `intros` to put `x₁ x₂ ⋯ xₙ` into the local context,
   --   now the goal is just `G`
@@ -574,7 +571,6 @@ def evalMonoNative : Tactic
   withMainContext do
     let (lemmas, inhFacts) ← collectAllLemmas hints uords (goalBinders.push ngoal)
     let proof ← monoInterface lemmas inhFacts Solver.Native.queryNative
-    IO.println s!"Auto found proof. Time spent by auto : {(← IO.monoMsNow) - startTime}ms"
     absurd.assign proof
 | _ => throwUnsupportedSyntax