feat(library/init/lean/util): Lean API for profiler

library/init/lean/util.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2019 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sebastian Ullrich
+-/
+prelude
+import init.lean.position init.io
+
+namespace lean
+
+/-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/
+@[extern 5 "lean_lean_profileit"]
+constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α
+def profileit_pure {α : Type} (category : string) (pos : position) (fn : unit → α) : io α :=
+profileit category pos $ io.lazy_pure fn
+
+end lean

src/frontends/lean/vm_elaborator.cpp

@@ -523,8 +523,6 @@ extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_
         type_context_old tc(env, options);
         scope_trace_env scope(env, options, tc);
         scope_traces_as_messages scope2(filename, pos);
-        simple_pos_info_provider pip(filename.c_str());
-        scope_pos_info_provider scope4(pip);
 
         parser p(env, ios, in, filename);
         auto s = p.mk_snapshot();

src/library/time_task.cpp

@@ -63,4 +63,14 @@ time_task::~time_task() {
             report_profiling_time(m_parent_task->m_category, -time);
     }
 }
+
+/* profileit {α : Type} (category : string) (pos : position) (act : io α) : io α */
+extern "C" obj_res lean_lean_profileit(obj_arg, b_obj_arg category, b_obj_arg pos, obj_arg fn, obj_arg w) {
+    time_task t(string_to_std(category),
+                message_builder(environment(), get_global_ios(), get_pos_info_provider()->get_file_name(),
+                        pos_info(nat(cnstr_get(pos, 0), true).get_small_value(),
+                                 nat(cnstr_get(pos, 1), true).get_small_value()),
+                        message_severity::INFORMATION));
+    return apply_1(fn, w);
+}
 }

src/shell/lean.cpp

@@ -470,6 +470,8 @@ int main(int argc, char ** argv) {
     }
     try {
         scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0});
+        simple_pos_info_provider pip(mod_fn.c_str());
+        scope_pos_info_provider scope_pip(pip);
 
         // TODO(Sebastian): parse imports using new frontend
         std::vector<rel_module_name> rel_imports;
@@ -496,6 +498,10 @@ int main(int argc, char ** argv) {
 
         bool ok;
         if (new_frontend) {
+            // Some C++ parts like profiling need a global message log. We may want to refactor them into a
+            // message_log-passing state monad in the future.
+            message_log l;
+            scope_message_log scope_log(l);
             object_ref res { lean_process_file(mk_string(mod_fn), mk_string(contents), static_cast<uint8>(json_output), box(0)) };
             ok = static_cast<bool>(unbox(cnstr_get_ref(res, 0).raw()));
         } else {