diff --git a/src/Std/Internal/Async/Signal.lean b/src/Std/Internal/Async/Signal.lean index 19490ea97d6c..e34f5853ec11 100644 --- a/src/Std/Internal/Async/Signal.lean +++ b/src/Std/Internal/Async/Signal.lean @@ -18,25 +18,27 @@ namespace IO namespace Async /-- -Unix style signals for Unix and Windows. SIGKILL and SIGSTOP are missing because they cannot be caught. +Unix style signals for Unix and Windows. +SIGKILL and SIGSTOP are missing because they cannot be caught. +SIGBUS, SIGFPE, SIGILL, and SIGSEGV are missing because they cannot be caught safely by libuv. SIGPIPE is not present because the runtime ignores the signal. -/ inductive Signal /-- - Hangup detected on controlling terminal or death of controlling process. SIGHUP is not - generated when terminal raw mode is enabled. + Hangup detected on controlling terminal or death of controlling process. On Windows: - * SIGHUP is generated when the user closes the console window. The program is given ~10 seconds to - cleanup before Windows unconditionally terminates it. + - SIGHUP is generated when the user closes the console window. The program is given ~10 seconds to + perform cleanup before Windows unconditionally terminates it. -/ | sighup /-- Interrupt program. - * Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled (like Unix). + Notes: + - Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled. -/ | sigint @@ -60,14 +62,14 @@ inductive Signal | sigabrt /-- - Emulate instruction executed + User-defined signal 1. -/ - | sigemt + | sigusr1 /-- - Bad system call. + User-defined signal 2. -/ - | sigsys + | sigusr2 /-- Real-time timer expired. @@ -83,14 +85,9 @@ inductive Signal | sigterm /-- - Urgent condition on socket. - -/ - | sigurg - - /-- - Stop typed at tty. + Child status has changed. -/ - | sigtstp + | sigchld /-- Continue after stop. @@ -98,9 +95,9 @@ inductive Signal | sigcont /-- - Child status has changed. + Stop typed at terminal. -/ - | sigchld + | sigtstp /-- Background read attempted from control terminal. @@ -108,14 +105,14 @@ inductive Signal | sigttin /-- - Background write attempted to control terminal + Background write attempted to control terminal. -/ | sigttou /-- - I/O now possible. + Urgent condition on socket. -/ - | sigio + | sigurg /-- CPU time limit exceeded. @@ -148,52 +145,48 @@ inductive Signal | sigwinch /-- - Status request from keyboard. - -/ - | siginfo - - /-- - User-defined signal 1. + I/O now possible. -/ - | sigusr1 + | sigio /-- - User-defined signal 2. + Bad system call. -/ - | sigusr2 + | sigsys deriving Repr, DecidableEq, BEq namespace Signal /-- -Converts a `Signal` to its corresponding `Int32` value as defined in the libc `signal.h`. +Converts a `Signal` to its corresponding `Int32` value as defined in `man 7 signal`. + +These values are then mapped to the underlying architecture's values in runtime/uv/signal.cpp, +so make sure to update that whenever you update this code. -/ -def toInt32 : Signal → Int32 +private def toInt32 : Signal → Int32 | .sighup => 1 | .sigint => 2 | .sigquit => 3 | .sigtrap => 5 | .sigabrt => 6 - | .sigemt => 7 - | .sigsys => 12 + | .sigusr1 => 10 + | .sigusr2 => 12 | .sigalrm => 14 | .sigterm => 15 - | .sigurg => 16 - | .sigtstp => 18 - | .sigcont => 19 - | .sigchld => 20 + | .sigchld => 17 + | .sigcont => 18 + | .sigtstp => 20 | .sigttin => 21 | .sigttou => 22 - | .sigio => 23 + | .sigurg => 23 | .sigxcpu => 24 | .sigxfsz => 25 | .sigvtalrm => 26 | .sigprof => 27 | .sigwinch => 28 - | .siginfo => 29 - | .sigusr1 => 30 - | .sigusr2 => 31 + | .sigio => 29 + | .sigsys => 31 /-- `Signal.Waiter` can be used to handle a specific signal once. diff --git a/src/runtime/uv/signal.cpp b/src/runtime/uv/signal.cpp index e75faa5ba89a..1eb0f40384ba 100644 --- a/src/runtime/uv/signal.cpp +++ b/src/runtime/uv/signal.cpp @@ -70,6 +70,32 @@ void handle_signal_event(uv_signal_t* handle, int signum) { extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating) { int signum = (int)(int32_t)signum_obj; + // See toInt32 in Std.Internal.IO.Async.Signal + switch (signum) { + case 1: signum = SIGHUP; break; + case 2: signum = SIGINT; break; + case 3: signum = SIGQUIT; break; + case 5: signum = SIGTRAP; break; + case 6: signum = SIGABRT; break; + case 10: signum = SIGUSR1; break; + case 12: signum = SIGUSR2; break; + case 14: signum = SIGALRM; break; + case 15: signum = SIGTERM; break; + case 17: signum = SIGCHLD; break; + case 18: signum = SIGCONT; break; + case 20: signum = SIGTSTP; break; + case 21: signum = SIGTTIN; break; + case 22: signum = SIGTTOU; break; + case 23: signum = SIGURG; break; + case 24: signum = SIGXCPU; break; + case 25: signum = SIGXFSZ; break; + case 26: signum = SIGVTALRM; break; + case 27: signum = SIGPROF; break; + case 28: signum = SIGWINCH; break; + case 29: signum = SIGIO; break; + case 31: signum = SIGSYS; break; + } + lean_uv_signal_object * signal = (lean_uv_signal_object*)malloc(sizeof(lean_uv_signal_object)); signal->m_signum = signum; signal->m_repeating = repeating; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index d0a43a6c9069..6263a2180365 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -309,7 +309,7 @@ add_dir_of_test_dirs(misc_dir) add_dir_of_test_dirs( pkg EXCEPT - signal # Test appears to be broken + signal # Flaky test_extern # Flaky user_ext # Test started being nondeterministic ) diff --git a/tests/pkg/signal/Main.lean b/tests/pkg/signal/Main.lean index ddca27980623..ca3d1b2c7aa8 100644 --- a/tests/pkg/signal/Main.lean +++ b/tests/pkg/signal/Main.lean @@ -10,17 +10,19 @@ def assertBEq [BEq α] [Repr α] (actual expected : α) : IO Unit := do s!"expected '{repr expected}', got '{repr actual}'" def select (signal1 signal2 signal3 signal4 : Signal.Waiter) : Async Signal := do + IO.println s!"Waiting for a signal" + IO.FS.Stream.flush (← IO.getStdout) let t ← Selectable.one #[ - .case (← signal1.selector) (fun _ => pure (Task.pure (.ok Signal.sigint))), - .case (← signal2.selector) (fun _ => pure (Task.pure (.ok Signal.sighup))), - .case (← signal3.selector) (fun _ => pure (Task.pure (.ok Signal.sigquit))), - .case (← signal4.selector) (fun _ => pure (Task.pure (.ok Signal.sigusr1))), + .case signal1.selector (fun _ => pure (Task.pure Signal.sigint)), + .case signal2.selector (fun _ => pure (Task.pure Signal.sighup)), + .case signal3.selector (fun _ => pure (Task.pure Signal.sigquit)), + .case signal4.selector (fun _ => pure (Task.pure Signal.sigusr1)), ] let signal ← await t - IO.println s!"received {repr signal}" + IO.eprintln s!"Received {repr signal}" pure signal def asyncMain : Async Unit := do @@ -29,13 +31,15 @@ def asyncMain : Async Unit := do let signal3 ← Signal.Waiter.mk Signal.sigquit true let signal4 ← Signal.Waiter.mk Signal.sigusr1 true + let _ ← signal1.wait + let _ ← signal2.wait + let _ ← signal3.wait + let _ ← signal4.wait + assertBEq (← select signal1 signal2 signal3 signal4) Signal.sigusr1 assertBEq (← select signal1 signal2 signal3 signal4) Signal.sighup assertBEq (← select signal1 signal2 signal3 signal4) Signal.sigquit assertBEq (← select signal1 signal2 signal3 signal4) Signal.sigint def main : IO Unit := do - IO.println s!"Waiting for a signal" - IO.FS.Stream.flush (← IO.getStdout) - asyncMain.wait diff --git a/tests/pkg/signal/run_test.sh b/tests/pkg/signal/run_test.sh index e99ea33b6df6..4ae064d55f52 100644 --- a/tests/pkg/signal/run_test.sh +++ b/tests/pkg/signal/run_test.sh @@ -8,36 +8,34 @@ mkfifo "$PIPE" # Run release in the background, redirect stdout to the pipe .lake/build/bin/release > "$PIPE" & PID=$! - echo "Started process with PID: $PID" -# Read the first line from the pipe -{ - if read -r first_line < "$PIPE"; then - echo "Received first line: $first_line" - - sleep 1 +function await_line(){ + read -r line < "$PIPE" + echo "Received line: $line" + sleep 1 +} - echo "Sending USR1 signal..." - kill -USR1 "$PID" 2>/dev/null || echo "Failed to send USR1" +await_line +echo "Sending USR1 signal..." +kill -USR1 "$PID" 2>/dev/null || fail "Failed to send USR1" - echo "Sending HUP signal..." - kill -HUP "$PID" 2>/dev/null || echo "Failed to send HUP" +await_line +echo "Sending HUP signal..." +kill -HUP "$PID" 2>/dev/null || fail "Failed to send HUP" - echo "Sending QUIT signal..." - kill -QUIT "$PID" 2>/dev/null || echo "Failed to send QUIT" +await_line +echo "Sending QUIT signal..." +kill -QUIT "$PID" 2>/dev/null || fail "Failed to send QUIT" - echo "Sending INT signal..." - kill -INT "$PID" 2>/dev/null || echo "Failed to send INT" - else - echo "Failed to read first line" - fi -} +await_line +echo "Sending INT signal..." +kill -INT "$PID" 2>/dev/null || fail "Failed to send INT" # Wait for process to finish echo "Waiting for process $PID to finish..." if wait "$PID"; then echo "Process completed successfully" else - echo "Process exited with code $?" + fail "Process exited with code $?" fi