deadlock in l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2

Prerequisites

Please put an X between the brackets as you perform the following steps:

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[ ] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.

Description

When running our lean-mlir tool, I found a testcase that was close to impossible to reduce. My code seems to finish the tactic evaluation, but hangs in the kernel. set_option debug.skipKernelTC true allows lean to terminate.

The stacktrace I obtain is:

* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGSTOP
  * frame #0: 0x000000018b59c5ec libsystem_kernel.dylib`__psynch_cvwait + 8
    frame #1: 0x000000018b5da55c libsystem_pthread.dylib`_pthread_cond_wait + 1228
    frame #2: 0x000000018b4ffb14 libc++.1.dylib`std::__1::condition_variable::wait(std::__1::unique_lock<std::__1::mutex>&) + 28
    frame #3: 0x00000001087f3da4 libleanshared.dylib`lean_task_get + 144
    frame #4: 0x0000000106e67508 libleanshared.dylib`l_Lean_Language_SnapshotTask_get___rarg + 76
    frame #5: 0x0000000106e73a64 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 228
    frame #6: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #7: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #8: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #9: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #10: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #11: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #12: 0x0000000106e73a94 libleanshared.dylib`l_Array_foldlMUnsafe_fold___at_Lean_Language_SnapshotTree_runAndReport___spec__2 + 276
    frame #13: 0x0000000105f55e28 libleanshared.dylib`lean_run_frontend + 1420
    frame #14: 0x0000000104efe684 libleanshared.dylib`lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>> const&, unsigned char) + 248
    frame #15: 0x0000000104f00f88 libleanshared.dylib`lean_main + 8412
    frame #16: 0x000000018b24f154 dyld`start + 2476

The bug first appeared in the lean nightly 2024-10-19 (https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2024-10-19). A potential guess is that https://github.com/leanprover/lean4/pull/5763 might potentially have introduced or exposed the bug in our particular setup.

The test case can be reproduced in this file:

https://github.com/opencompl/lean-mlir/blob/cc021f606793e86e8dcd469e21d365233fc16030/SSA/Projects/InstCombine/tests/LLVM/gaddhmaskhnegtobias.lean#L24

Steps to Reproduce

Try to compile dec_mask_neg_i32_proof
See lean hanging

git clone git@github.com:opencompl/lean-mlir.git
cd lean-mlir
git checkout lean-deadlock
lake exe cache get
lake build
lake build SSA.Projects.InstCombine.tests.LLVM.gaddhmaskhnegtobias

Observe the last command to hang.

Expected

Lean should not hang

Versions

Lean 4.12.0-nightly-2024-10-30 Target: arm64-apple-darwin23.6.0 macOS

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4