Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
79 changes: 36 additions & 43 deletions src/Std/Internal/Async/Signal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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.
Expand All @@ -83,39 +85,34 @@ inductive Signal
| sigterm

/--
Urgent condition on socket.
-/
| sigurg

/--
Stop typed at tty.
Child status has changed.
-/
| sigtstp
| sigchld

/--
Continue after stop.
-/
| sigcont

/--
Child status has changed.
Stop typed at terminal.
-/
| sigchld
| sigtstp

/--
Background read attempted from control terminal.
-/
| 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.
Expand Down Expand Up @@ -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.
Expand Down
26 changes: 26 additions & 0 deletions src/runtime/uv/signal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion tests/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
Expand Down
20 changes: 12 additions & 8 deletions tests/pkg/signal/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
38 changes: 18 additions & 20 deletions tests/pkg/signal/run_test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading