From 076fe302e47e6a5f7e34796ceb63e94347e09d3e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 27 Dec 2024 17:19:52 +0100 Subject: [PATCH] fix compilation skip on kernel error --- src/Lean/CoreM.lean | 4 ++-- src/library/compiler/ir_interpreter.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 0d727307ffa1..42416898a2a9 100644 --- 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 index 2f32ef862150..17f0742eac56 100644 --- 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 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(); }