refactor: pos at time_task::time_task was a dead field

src/Lean/Elab/Frontend.lean

@@ -52,7 +52,7 @@ def processCommand : FrontendM Bool := do
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let pos := ictx.fileMap.toPosition pstate.pos
-  match profileit "parsing" scope.opts pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
+  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
   | (cmd, ps, messages) =>
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
@@ -60,7 +60,7 @@ def processCommand : FrontendM Bool := do
     if Parser.isEOI cmd || Parser.isExitCommand cmd then
       pure true -- Done
     else
-      profileitM IO.Error "elaboration" scope.opts pos $ elabCommandAtFrontend cmd
+      profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
       pure false
 
 partial def processCommands : FrontendM Unit := do

src/Lean/Environment.lean

@@ -543,7 +543,7 @@ structure ImportState where
   regions       : Array CompactedRegion := #[]
 
 @[export lean_import_modules]
-partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts ⟨0, 0⟩ do
+partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts do
   let (_, s) ← importMods imports |>.run {}
   -- (moduleNames, mods, regions)
   let mut modIdx : Nat := 0

src/Lean/Meta/SynthInstance.lean

@@ -555,7 +555,7 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
-def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) ⟨0, 0⟩ do
+def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   let inputConfig ← getConfig

src/Lean/Util/Profile.lean

@@ -9,18 +9,18 @@ namespace Lean
 
 /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/
 @[extern "lean_profileit"]
-def profileit {α : Type} (category : @& String) (opts : @& Options) (pos : @& Position) (fn : Unit → α) : α := fn ()
+def profileit {α : Type} (category : @& String) (opts : @& Options) (fn : Unit → α) : α := fn ()
 
-unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α :=
-  match profileit category opts pos fun _ => unsafeEIO act with
+unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α :=
+  match profileit category opts fun _ => unsafeEIO act with
   | Except.ok a    => pure a
   | Except.error e => throw e
 
 @[implementedBy profileitIOUnsafe]
-def profileitIO {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α := act
+def profileitIO {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α := act
 
 -- impossible to infer `ε`
-def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (pos : Position) (act : m α) : m α :=
-  monadMap (fun {β} => @profileitIO ε β category opts pos) act
+def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (act : m α) : m α :=
+  monadMap (fun {β} => profileitIO (ε := ε) (α := β) category opts) act
 
 end Lean

src/library/time_task.cpp

@@ -38,7 +38,7 @@ void finalize_time_task() {
     delete g_cum_times_mutex;
 }
 
-time_task::time_task(std::string const & category, options const & opts, pos_info pos, name decl) :
+time_task::time_task(std::string const & category, options const & opts, name decl) :
         m_category(category) {
     if (get_profiler(opts)) {
         m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable {
@@ -63,12 +63,10 @@ time_task::~time_task() {
     }
 }
 
-/* profileit {α : Type} (category : String) (opts : Options) (pos : Position) (fn : Unit → α) : α */
-extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, b_obj_arg pos, obj_arg fn) {
+/* profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) : α */
+extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, obj_arg fn) {
     time_task t(string_to_std(category),
-                TO_REF(options, opts),
-                pos_info(nat(cnstr_get(pos, 0), true).get_small_value(),
-                         nat(cnstr_get(pos, 1), true).get_small_value()));
+                TO_REF(options, opts));
     return apply_1(fn, box(0));
 }
 }

src/library/time_task.h

@@ -20,7 +20,7 @@ class time_task {
     optional<xtimeit> m_timeit;
     time_task *     m_parent_task;
 public:
-    time_task(std::string const & category, options const & opts, pos_info pos = pos_info(), name decl = name());
+    time_task(std::string const & category, options const & opts, name decl = name());
     ~time_task();
 };