diff --git a/src/Lean.lean b/src/Lean.lean
index a7e59d1d71..b86c848302 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -32,3 +32,4 @@ import Lean.DeclarationRange
 import Lean.LazyInitExtension
 import Lean.LoadDynlib
 import Lean.Widget
+import Lean.Log
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index dedf72fbc1..b32d62cee1 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -3,10 +3,10 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Log
 import Lean.Parser.Command
 import Lean.ResolveName
 import Lean.Meta.Reduce
-import Lean.Elab.Log
 import Lean.Elab.Term
 import Lean.Elab.Tactic.Cache
 import Lean.Elab.Binders
diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean
index 8d11137fd8..9c403828ee 100644
--- a/src/Lean/Elab/DeclarationRange.lean
+++ b/src/Lean/Elab/DeclarationRange.lean
@@ -3,8 +3,9 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Log
+import Lean.Parser.Command
 import Lean.DeclarationRange
-import Lean.Elab.Log
 import Lean.Data.Lsp.Utf16
 
 namespace Lean.Elab
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 23bb7ca3b0..48677b4572 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -3,8 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Log
+import Lean.Parser.Level
 import Lean.Elab.Exception
-import Lean.Elab.Log
 import Lean.Elab.AutoBound
 
 namespace Lean.Elab.Level
diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean
index b473180cfc..62a2bf21ef 100644
--- a/src/Lean/Elab/Open.lean
+++ b/src/Lean/Elab/Open.lean
@@ -3,7 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Elab.Log
+import Lean.Log
+import Lean.Elab.Util
 
 namespace Lean.Elab
 namespace OpenDecl
diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean
index b41cafda7c..5116ff4f4e 100644
--- a/src/Lean/Elab/SetOption.lean
+++ b/src/Lean/Elab/SetOption.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Elab.Log
+import Lean.Log
 import Lean.Elab.InfoTree
 namespace Lean.Elab
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 254224903b..0259cbbcef 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.ResolveName
+import Lean.Log
 import Lean.Util.Sorry
 import Lean.Util.ReplaceExpr
 import Lean.Structure
@@ -13,7 +14,6 @@ import Lean.Meta.Coe
 import Lean.Hygiene
 import Lean.Util.RecDepth
 
-import Lean.Elab.Log
 import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.Attributes
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 5dac434519..b489094361 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -11,6 +11,7 @@ import Lean.Elab.Exception
 import Lean.DocString
 import Lean.DeclarationRange
 import Lean.Compiler.InitAttr
+import Lean.Log
 
 namespace Lean
 
@@ -195,6 +196,21 @@ partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
   else
     return baseName
 
+def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadLiftT IO m] (ex : Exception) : m Unit := do
+  match ex with
+  | Exception.error ref msg => logErrorAt ref msg
+  | Exception.internal id _ =>
+    unless isAbortExceptionId id do
+      let name ← id.getName
+      logError m!"internal exception: {name}"
+
+@[inline] def trace [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
+  if checkTraceOption (← getOptions) cls then
+    logTrace cls (msg ())
+
+def logDbgTrace [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (msg : MessageData) : m Unit := do
+  trace `Elab.debug fun _ => msg
+
 builtin_initialize
   registerTraceClass `Elab
   registerTraceClass `Elab.step
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Log.lean
similarity index 79%
rename from src/Lean/Elab/Log.lean
rename to src/Lean/Log.lean
index a35c9c6cdd..51aff999bf 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Log.lean
@@ -3,11 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Elab.Util
 import Lean.Util.Sorry
-import Lean.Elab.Exception
 
-namespace Lean.Elab
+namespace Lean
 
 class MonadLog (m : Type → Type) extends MonadFileMap m where
   getRef       : m Syntax
@@ -63,25 +61,10 @@ def logWarning (msgData : MessageData) : m Unit :=
 def logInfo (msgData : MessageData) : m Unit :=
   log msgData MessageSeverity.information
 
-def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do
-  match ex with
-  | Exception.error ref msg => logErrorAt ref msg
-  | Exception.internal id _ =>
-    unless isAbortExceptionId id do
-      let name ← id.getName
-      logError m!"internal exception: {name}"
-
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
   logInfo (MessageData.tagged cls m!"[{cls}] {msgData}")
 
-@[inline] def trace [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
-  if checkTraceOption (← getOptions) cls then
-    logTrace cls (msg ())
-
-def logDbgTrace [MonadOptions m] (msg : MessageData) : m Unit := do
-  trace `Elab.debug fun _ => msg
-
 def logUnknownDecl (declName : Name) : m Unit :=
   logError m!"unknown declaration '{declName}'"
 
-end Lean.Elab
+end Lean