From 943576264361cfa3bb04d8f59e1586496c30ae7b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 4 Jan 2017 19:48:01 +0100
Subject: [PATCH] fix(compiler/vm_compiler): only compile computable
 non-builtin definitions

---
 src/frontends/lean/definition_cmds.cpp  |  9 +++------
 src/library/compiler/vm_compiler.cpp    |  5 ++++-
 src/library/equations_compiler/util.cpp | 15 ++++++---------
 3 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 0e06dd2ac2..518455959c 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -319,13 +319,10 @@ static void check_noncomputable(bool ignore_noncomputable, environment const & e
     }
 }
 
-static environment compile_decl(parser & p, environment const & env, def_cmd_kind kind, bool is_noncomputable,
+static environment compile_decl(parser & p, environment const & env,
                                 name const & c_name, name const & c_real_name, pos_info const & pos) {
-    if (is_noncomputable || kind == Theorem || kind == Example || is_vm_builtin_function(c_real_name))
-        return env;
     try {
-        declaration d = env.get(c_real_name);
-        return vm_compile(env, d);
+        return vm_compile(env, env.get(c_real_name));
     } catch (exception & ex) {
         if (p.found_errors())
             return env;
@@ -379,7 +376,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
     }
 
     new_env = attrs.apply(new_env, p.ios(), c_real_name);
-    new_env = compile_decl(p, new_env, kind, modifiers.m_is_noncomputable, c_name, c_real_name, pos);
+    new_env = compile_decl(p, new_env, c_name, c_real_name, pos);
     if (doc_string) {
         new_env = add_doc_string(new_env, c_real_name, *doc_string);
     }
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 6fb373bb3b..00a1e73eba 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/noncomputable.h"
 #include "util/fresh_name.h"
 #include "util/sstream.h"
 #include "kernel/instantiate.h"
@@ -399,7 +400,9 @@ static environment vm_compile(environment const & env, buffer<procedure> const &
 }
 
 environment vm_compile(environment const & env, declaration const & d) {
-    if (!d.is_definition()) return env;
+    if (!d.is_definition() || d.is_theorem() || is_noncomputable(env, d.get_name()) || is_vm_builtin_function(d.get_name()))
+        return env;
+
     buffer<procedure> procs;
     preprocess(env, d, procs);
     return vm_compile(env, procs);
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 56b4ce21f0..66e46f1b34 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -292,15 +292,12 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
     } catch (exception & ex) {
         throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
     }
-    if (!header.m_is_lemma && !header.m_is_noncomputable) {
-        try {
-            declaration d = new_env.get(new_c);
-            new_env = vm_compile(new_env, d);
-        } catch (exception & ex) {
-            if (!header.m_prev_errors) {
-                throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
-                                       << "auxiliary declaration '" << c << "'", ex);
-            }
+    try {
+        new_env = vm_compile(new_env, new_env.get(new_c));
+    } catch (exception & ex) {
+        if (!header.m_prev_errors) {
+            throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
+                                   << "auxiliary declaration '" << c << "'", ex);
         }
     }
     return mk_pair(new_env, r);