fix compilation skip on kernel error

leanprover · Dec 28, 2024 · 9b36754 · 9b36754
1 parent b44a2ff
commit 9b36754
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
@@ -517,7 +517,7 @@ opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 def compileDecl (decl : Declaration) : CoreM Unit := do
   -- don't compile if kernel errored; should be converted into a task dependency when compilation
   -- is made async as well
-  if (← get).snapshotTasks.any (·.get.element.diagnostics.msgLog.hasErrors) then
+  if !decl.getNames.all (← getEnv).toKernelEnv.constants.contains then
     return
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
@@ -536,7 +536,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
 def compileDecls (decls : List Name) : CoreM Unit := do
   -- don't compile if kernel errored; should be converted into a task dependency when compilation
   -- is made async as well
-  if (← get).snapshotTasks.any (·.get.element.diagnostics.msgLog.hasErrors) then
+  if !decls.all (← getEnv).toKernelEnv.constants.contains then
     return
   let opts ← getOptions
   if compiler.enableNew.get opts then

diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
@@ -812,7 +812,7 @@ class interpreter {
     decl get_decl(name const & fn) {
         option_ref<decl> d = find_ir_decl(m_env, fn);
         if (!d) {
-            throw exception(sstream() << "unknown declaration '" << fn << "'");
+            throw exception(sstream() << "(interpreter) unknown declaration '" << fn << "'");
         }
         return d.get().value();
     }