From a6c319a25c213cbf3aa3d2188b166f9bec71d9ac Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 11 Jan 2021 12:12:43 +0100 Subject: [PATCH] chore: remove message_builder from time_task --- src/Lean/Elab/Frontend.lean | 4 ++-- src/Lean/Environment.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 2 +- src/Lean/Util/Profile.lean | 12 ++++++------ src/library/compiler/compiler.cpp | 3 +-- src/library/compiler/ir_interpreter.cpp | 3 +-- src/library/time_task.cpp | 14 ++++++-------- src/library/time_task.h | 2 +- src/shell/lean.cpp | 8 ++------ 9 files changed, 21 insertions(+), 29 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index ebfe918b84..aec916031d 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/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" pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with + match profileit "parsing" scope.opts pos 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" pos $ elabCommandAtFrontend cmd + profileitM IO.Error "elaboration" scope.opts pos $ elabCommandAtFrontend cmd pure false partial def processCommands : FrontendM Unit := do diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 8dfd9dbec9..2997d4ffa2 100644 --- a/src/Lean/Environment.lean +++ b/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" ⟨0, 0⟩ do +partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts ⟨0, 0⟩ do let (_, s) ← importMods imports |>.run {} -- (moduleNames, mods, regions) let mut modIdx : Nat := 0 diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index bcabf3619d..a560e70553 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -541,7 +541,7 @@ private def getMaxSize (opts : Options) : Nat := 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) := profileitM Exception "typeclass inference" ⟨0, 0⟩ do +def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) ⟨0, 0⟩ do let opts ← getOptions let maxResultSize := maxResultSize?.getD (getMaxSize opts) let inputConfig ← getConfig diff --git a/src/Lean/Util/Profile.lean b/src/Lean/Util/Profile.lean index bac75f38c8..a0cd020ff1 100644 --- a/src/Lean/Util/Profile.lean +++ b/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) (pos : @& Position) (fn : Unit → α) : α := fn () +def profileit {α : Type} (category : @& String) (opts : @& Options) (pos : @& Position) (fn : Unit → α) : α := fn () -unsafe def profileitIOUnsafe {ε α : Type} (category : String) (pos : Position) (act : EIO ε α) : EIO ε α := - match profileit category pos fun _ => unsafeEIO act with +unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α := + match profileit category opts pos fun _ => unsafeEIO act with | Except.ok a => pure a | Except.error e => throw e @[implementedBy profileitIOUnsafe] -def profileitIO {ε α : Type} (category : String) (pos : Position) (act : EIO ε α) : EIO ε α := act +def profileitIO {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α := act -- impossible to infer `ε` -def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : @& String) (pos : @& Position) (act : m α) : m α := - monadMap (fun {β} => @profileitIO ε β category pos) act +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 end Lean diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 8408cc7aa3..5528a54562 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -193,8 +193,7 @@ environment compile(environment const & env, options const & opts, names cs) { if (has_synthetic_sorry(cinfo)) return env; } - time_task t("compilation", - message_builder(environment(), get_global_ios(), "foo", pos_info(), message_severity::INFORMATION)); + time_task t("compilation", opts); abstract_type_context trace_ctx(opts); scope_trace_env scope_trace(env, opts, trace_ctx); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 33161bc0d1..dc486c9840 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -357,8 +357,7 @@ public: return f(*g_interpreter); } else { // We changed threads or the closure was stored and called in a different context. - time_task t("interpretation", - message_builder(env, get_global_ios(), "foo", pos_info(), message_severity::INFORMATION)); + time_task t("interpretation", opts); abstract_type_context trace_ctx(opts); scope_trace_env scope_trace(env, opts, trace_ctx); // the caches contain data from the Environment, so we cannot reuse them when changing it diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp index cf2e944352..a7662be471 100644 --- a/src/library/time_task.cpp +++ b/src/library/time_task.cpp @@ -38,9 +38,8 @@ void finalize_time_task() { delete g_cum_times_mutex; } -time_task::time_task(std::string const & category, message_builder builder, name decl) : +time_task::time_task(std::string const & category, options const & opts, pos_info pos, name decl) : m_category(category) { - auto const & opts = builder.get_text_stream().get_options(); if (get_profiler(opts)) { m_timeit = optional(get_profiling_threshold(opts), [=](second_duration duration) mutable { tout() << m_category; @@ -64,13 +63,12 @@ time_task::~time_task() { } } -/* profileit {α : Type} (category : String) (pos : Position) (fn : Unit → α) : α */ -extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg pos, obj_arg fn) { +/* 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) { time_task t(string_to_std(category), - message_builder(environment(), get_global_ios(), "foo", - pos_info(nat(cnstr_get(pos, 0), true).get_small_value(), - nat(cnstr_get(pos, 1), true).get_small_value()), - message_severity::INFORMATION)); + TO_REF(options, opts), + pos_info(nat(cnstr_get(pos, 0), true).get_small_value(), + nat(cnstr_get(pos, 1), true).get_small_value())); return apply_1(fn, box(0)); } } diff --git a/src/library/time_task.h b/src/library/time_task.h index a43d62c98d..945f200c25 100644 --- a/src/library/time_task.h +++ b/src/library/time_task.h @@ -20,7 +20,7 @@ class time_task { optional m_timeit; time_task * m_parent_task; public: - time_task(std::string const & category, message_builder builder, name decl = name()); + time_task(std::string const & category, options const & opts, pos_info pos = pos_info(), name decl = name()); ~time_task(); }; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index c89a508943..860f78c15b 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -648,9 +648,7 @@ int main(int argc, char ** argv) { return ret; } if (olean_fn && ok) { - time_task t(".olean serialization", - message_builder(environment(), get_global_ios(), mod_fn, pos_info(), - message_severity::INFORMATION)); + time_task t(".olean serialization", opts); write_module(env, *olean_fn); } @@ -660,9 +658,7 @@ int main(int argc, char ** argv) { std::cerr << "failed to create '" << *c_output << "'\n"; return 1; } - time_task _("C code generation", - message_builder(environment(), get_global_ios(), mod_fn, pos_info(), - message_severity::INFORMATION)); + time_task _("C code generation", opts); out << lean::ir::emit_c(env, *main_module_name).data(); out.close(); }