vcgen test

src/Lean/Environment.lean

@@ -194,6 +194,7 @@ structure EnvironmentHeader where
   importAllModules : Array EffectiveImport := modules.filter (·.importAll)
   /-- Module data for all imported modules. -/
   moduleData   : Array ModuleData := #[]
+  cmdLineOptions : Options  := {}
   deriving Nonempty
 
 /--
@@ -318,6 +319,10 @@ private def isQuotInit (env : Environment) : Bool :=
 opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
   (cancelTk? : @& Option IO.CancelToken) : Except Exception Environment
 
+@[export lean_environment_get_opts]
+def getOpts (env : Environment) : Options :=
+  env.header.cmdLineOptions
+
 /--
 Add declaration to kernel without type checking it.
 
@@ -2255,6 +2260,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
       trustLevel, imports, moduleData, isModule
       modules      := modules.map (·.toEffectiveImport)
       regions      := modules.flatMap (·.parts.map (·.2)) ++ modules.filterMap (·.irData?.map (·.2))
+      cmdLineOptions := opts
     }
   }
   let publicConstants : ConstMap := SMap.fromHashMap publicConstantMap false

src/kernel/environment.cpp

@@ -16,10 +16,12 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker.h"
 #include "kernel/quot.h"
+#include "library/time_task.h"
 
 namespace lean {
 extern "C" object* lean_environment_add(object*, object*);
 extern "C" object* lean_environment_find(object*, object*);
+extern "C" object* lean_environment_get_opts(object*);
 extern "C" object* lean_environment_mark_quot_init(object*);
 extern "C" uint8 lean_environment_quot_init(object*);
 extern "C" object* lean_kernel_record_unfold (object*, object*);
@@ -75,6 +77,10 @@ optional<constant_info> environment::find(name const & n) const {
     return to_optional<constant_info>(lean_environment_find(to_obj_arg(), n.to_obj_arg()));
 }
 
+options environment::get_opts() const {
+    return options(lean_environment_get_opts(to_obj_arg()));
+}
+
 constant_info environment::get(name const & n) const {
     object * o = lean_environment_find(to_obj_arg(), n.to_obj_arg());
     if (is_scalar(o))
@@ -190,6 +196,7 @@ environment environment::add_definition(declaration const & d, bool check) const
 }
 
 environment environment::add_theorem(declaration const & d, bool check) const {
+    time_task task("add_theorem", options());
     scoped_diagnostics diag(*this, check);
     theorem_val const & v = d.to_theorem_val();
     if (check) {

src/kernel/environment.h

@@ -84,6 +84,7 @@ public:
 
     diagnostics get_diag() const;
     environment set_diag(diagnostics const & diag) const;
+    options get_opts() const;
 
     bool is_quot_initialized() const;
 

src/kernel/type_checker.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/quot.h"
 #include "kernel/inductive.h"
+#include "library/time_task.h"
 
 namespace lean {
 static name * g_kernel_fresh = nullptr;
@@ -160,21 +161,41 @@ static bool is_eager_reduce(expr const & e) {
     return is_const(get_app_fn(e), *g_eager_reduce) && get_app_num_args(e) == 2;
 }
 
-expr type_checker::infer_app(expr const & e, bool infer_only) {
-    if (!infer_only) {
-        expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), e);
-        expr a_type = infer_type_core(app_arg(e), infer_only);
-        expr d_type = binding_domain(f_type);
-        if (is_eager_reduce(app_arg(e))) {
-            // If argument is of the form `eagerReduce`, set m_eager_reduction mode
-            flet<bool> scope(m_eager_reduce, true);
-            if (!is_def_eq(a_type, d_type)) {
-                throw app_type_mismatch_exception(env(), m_lctx, e, f_type, a_type);
-            }
-        } else if (!is_def_eq(a_type, d_type)) {
+expr type_checker::infer_app_core(expr const & e) {
+    bool infer_only = false;
+    if (!is_app(e)) return infer_type_core(e, infer_only);
+    expr f_type = ensure_pi_core(infer_app_core(app_fn(e)), e);
+    expr a_type = infer_type_core(app_arg(e), infer_only);
+    expr d_type = binding_domain(f_type);
+    if (is_eager_reduce(app_arg(e))) {
+        // If argument is of the form `eagerReduce`, set m_eager_reduction mode
+        flet<bool> scope(m_eager_reduce, true);
+        if (!is_def_eq(a_type, d_type)) {
             throw app_type_mismatch_exception(env(), m_lctx, e, f_type, a_type);
         }
-        return instantiate(binding_body(f_type), app_arg(e));
+    } else if (!is_def_eq(a_type, d_type)) {
+        throw app_type_mismatch_exception(env(), m_lctx, e, f_type, a_type);
+    }
+    return instantiate(binding_body(f_type), app_arg(e));
+}
+
+expr type_checker::infer_app(expr const & e, bool infer_only) {
+    if (!infer_only) {
+        std::string label = "kernel.infer_app";
+        auto f = e;
+        while (true) {
+            f = get_app_fn(f);
+            if (is_lambda(f))
+                f = binding_body(f);
+            else
+                break;
+        }
+        if (is_const(f)) label += "." + const_name(f).to_string();
+        if (is_proj(f)) label += "._prof." + proj_sname(f).to_string() + "." + std::to_string(proj_idx(f).get_small_value());
+        if (is_fvar(f)) label += "._fvar";
+        if (is_lambda(f)) label += "._lam";
+        time_task task(label, env().get_opts());
+        return infer_app_core(e);
     } else {
         buffer<expr> args;
         expr const & f = get_app_args(e, args);
@@ -272,6 +293,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
         throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it");
 
     check_system("type checker", /* do_check_interrupted */ true);
+    time_task task("kernel.infer_other", env().get_opts());
 
     auto it = m_st->m_infer_type[infer_only].find(e);
     if (it != m_st->m_infer_type[infer_only].end())

src/kernel/type_checker.h

@@ -63,6 +63,7 @@ private:
     expr infer_constant(expr const & e, bool infer_only);
     expr infer_lambda(expr const & e, bool infer_only);
     expr infer_pi(expr const & e, bool infer_only);
+    expr infer_app_core(expr const & e);
     expr infer_app(expr const & e, bool infer_only);
     expr infer_proj(expr const & e, bool infer_only);
     expr infer_let(expr const & e, bool infer_only);

src/library/time_task.cpp

@@ -33,7 +33,8 @@ void display_cumulative_profiling_times(std::ostream & out) {
     sstream ss;
     ss << "cumulative profiling times:\n";
     for (auto const & p : *g_cum_times)
-        ss << "\t" << p.first << " " << display_profiling_time{p.second} << "\n";
+        if (p.second > std::chrono::milliseconds(1))
+            ss << "\t" << p.first << " " << display_profiling_time{p.second} << "\n";
     // output atomically, like IO.print
     out << ss.str();
 }

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -482,3 +482,23 @@ example :
   mvcgen'
   grind
 -/
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  set (s + v)
+  let s ← get
+  set (s - v)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+set_option maxRecDepth 100000
+set_option maxHeartbeats 10000000
+
+example : ∀ post, ⦃post⦄ loop 100 ⦃⇓_ => post⦄ := by
+  intro post
+  simp only [loop, step]
+  mvcgen'
+  sorry