From 2018dc09592c07671b2c097d04e0170076c81f48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Jun 2021 14:38:55 -0700 Subject: [PATCH] fix: disable panic messages during initialization This is a temporary workaround until we implement #467. Fixes #534 --- src/Lean/Compiler/IR/EmitC.lean | 4 ++++ tests/compiler/534.lean | 12 ++++++++++++ tests/compiler/534.lean.expected.out | 1 + 3 files changed, 17 insertions(+) create mode 100644 tests/compiler/534.lean create mode 100644 tests/compiler/534.lean.expected.out diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 98c2d5823e..81f40e17d9 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -158,7 +158,11 @@ def emitMainFn : M Unit := do else emitLn "lean_initialize_runtime_module();" let modName ← getModName + /- We disable panic messages because they do not mesh well with extracted closed terms. + See issue #534. We can remove this workaround after we implement issue #467. -/ + emitLn "lean_set_panic_messages(false);" emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(lean_io_mk_world());") + emitLn "lean_set_panic_messages(true);" emitLns ["lean_io_mark_end_initialization();", "if (lean_io_result_is_ok(res)) {", "lean_dec_ref(res);", diff --git a/tests/compiler/534.lean b/tests/compiler/534.lean new file mode 100644 index 0000000000..4dad681ac2 --- /dev/null +++ b/tests/compiler/534.lean @@ -0,0 +1,12 @@ +def foo (array : Array Nat) : Nat -> Nat + | 0 => 0 + | n + 1 => + let array := array.filter (!.==5) + if array.isEmpty then + 0 + else + let arrayOfLast := #[array.back] + foo arrayOfLast n + +def main : IO Unit := + IO.println ("hi") diff --git a/tests/compiler/534.lean.expected.out b/tests/compiler/534.lean.expected.out new file mode 100644 index 0000000000..45b983be36 --- /dev/null +++ b/tests/compiler/534.lean.expected.out @@ -0,0 +1 @@ +hi