diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean index e1df8ac208..05627b599f 100644 --- a/src/Std/Internal/Async.lean +++ b/src/Std/Internal/Async.lean @@ -14,5 +14,6 @@ public import Std.Internal.Async.DNS public import Std.Internal.Async.Select public import Std.Internal.Async.Process public import Std.Internal.Async.System +public import Std.Internal.Async.Signal public section diff --git a/src/Std/Internal/Async/Signal.lean b/src/Std/Internal/Async/Signal.lean new file mode 100644 index 0000000000..d2b5fad085 --- /dev/null +++ b/src/Std/Internal/Async/Signal.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Time +public import Std.Internal.UV.Signal +public import Std.Internal.Async.Select + +public section + +namespace Std +namespace Internal +namespace IO +namespace Async + +/-- +Unix style signals for Unix and Windows. SIGKILL and SIGSTOP are missing because they cannot be caught. +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. + + 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 + + /-- + Interrupt program. + + * Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled (like Unix). + -/ + | sigint + + /-- + Quit program. + -/ + | sigquit + + /-- + Trace/breakpoint trap. + -/ + | sigtrap + + /-- + Abort signal. + + Notes: + - SIGABRT is not catchable if generated by certain runtime functions, such as abort or assertion failure. + - On Windows, watchers can be created for SIGABRT, but they never receive the signal. + -/ + | sigabrt + + /-- + Emulate instruction executed + -/ + | sigemt + + /-- + Bad system call. + -/ + | sigsys + + /-- + Real-time timer expired. + -/ + | sigalrm + + /-- + Termination signal. + + Notes: + - On Windows, watchers can be created for SIGTERM, but they never receive the signal. + -/ + | sigterm + + /-- + Urgent condition on socket. + -/ + | sigurg + + /-- + Stop typed at tty. + -/ + | sigtstp + + /-- + Continue after stop. + -/ + | sigcont + + /-- + Child status has changed. + -/ + | sigchld + + /-- + Background read attempted from control terminal. + -/ + | sigttin + + /-- + Background write attempted to control terminal + -/ + | sigttou + + /-- + I/O now possible. + -/ + | sigio + + /-- + CPU time limit exceeded. + -/ + | sigxcpu + + /-- + File size limit exceeded. + -/ + | sigxfsz + + /-- + Virtual alarm clock. + -/ + | sigvtalrm + + /-- + Profiling timer expired. + -/ + | sigprof + + /-- + Window size change. + + Notes: + - SIGWINCH is raised whenever the runtime detects the console has been resized. + - Under console emulators, or on 32-bit apps on 64-bit systems, SIGWINCH is emulated. + - In these cases, signals may not be delivered timely. + -/ + | sigwinch + + /-- + Status request from keyboard. + -/ + | siginfo + + /-- + User-defined signal 1. + -/ + | sigusr1 + + /-- + User-defined signal 2. + -/ + | sigusr2 + +deriving Repr, DecidableEq, BEq + +namespace Signal + +/-- +Converts a `Signal` to its corresponding `Int32` value as defined in the libc `signal.h`. +-/ +def toInt32 : Signal → Int32 + | .sighup => 1 + | .sigint => 2 + | .sigquit => 3 + | .sigtrap => 5 + | .sigabrt => 6 + | .sigemt => 7 + | .sigsys => 12 + | .sigalrm => 14 + | .sigterm => 15 + | .sigurg => 16 + | .sigtstp => 18 + | .sigcont => 19 + | .sigchld => 20 + | .sigttin => 21 + | .sigttou => 22 + | .sigio => 23 + | .sigxcpu => 24 + | .sigxfsz => 25 + | .sigvtalrm => 26 + | .sigprof => 27 + | .sigwinch => 28 + | .siginfo => 29 + | .sigusr1 => 30 + | .sigusr2 => 31 + +/-- +`Signal.Waiter` can be used to handle a specific signal once. +-/ +structure Waiter where + private ofNative :: + native : Internal.UV.Signal + +namespace Waiter + +/-- +Set up a `Signal.Waiter` that waits for the specified `signum`. +This function only initializes but does not yet start listening for the signal. +-/ +@[inline] +def mk (signum : Signal) (repeating : Bool) : IO Signal.Waiter := do + let native ← Internal.UV.Signal.mk signum.toInt32 repeating + return .ofNative native + +/-- +If: +- `s` is not yet running start listening and return an `AsyncTask` that will resolve once the + previously configured signal is received. +- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`. + +The resolved `AsyncTask` contains the signal number that was received. +-/ +@[inline] +def wait (s : Signal.Waiter) : IO (AsyncTask Int) := do + let promise ← s.native.next + return .ofPurePromise promise + +/-- +If: +- `s` is still running this stops `s` without resolving any remaining `AsyncTask`s that were created + through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang + forever without further intervention. +- `s` is not yet or not anymore running this is a no-op. +-/ +@[inline] +def stop (s : Signal.Waiter) : IO Unit := + s.native.stop + +/-- +Create a `Selector` that resolves once `s` has received the signal. Note that calling this function starts `s` +if it hasn't already started. +-/ +def selector (s : Signal.Waiter) : IO (Selector Unit) := do + let signalWaiter ← s.wait + return { + tryFn := do + if ← IO.hasFinished signalWaiter then + return some () + else + return none + + registerFn waiter := do + discard <| AsyncTask.mapIO (x := signalWaiter) fun _ => do + let lose := return () + let win promise := promise.resolve (.ok ()) + waiter.race lose win + + unregisterFn := s.stop + } diff --git a/src/Std/Internal/UV.lean b/src/Std/Internal/UV.lean index a727a559d8..1b829426cf 100644 --- a/src/Std/Internal/UV.lean +++ b/src/Std/Internal/UV.lean @@ -15,5 +15,6 @@ public import Std.Internal.UV.TCP public import Std.Internal.UV.UDP public import Std.Internal.UV.System public import Std.Internal.UV.DNS +public import Std.Internal.UV.Signal @[expose] public section diff --git a/src/Std/Internal/UV/Signal.lean b/src/Std/Internal/UV/Signal.lean new file mode 100644 index 0000000000..c2b235053b --- /dev/null +++ b/src/Std/Internal/UV/Signal.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.System.IO +public import Init.System.Promise +public import Init.Data.SInt +public import Std.Net + +public section + +namespace Std +namespace Internal +namespace UV + +private opaque SignalImpl : NonemptyType.{0} + +/-- +`Signal`s are used to generate `IO.Promise`s that resolve when a specific signal is received. + +A `Signal` can be in one of 3 states: +- Right after construction it's initial. +- While it is listening for signals it's running. +- If it has stopped for some reason it's finished. + +This together with whether it was set up as `repeating` with `Signal.mk` determines the behavior +of all functions on `Signal`s. +-/ +def Signal : Type := SignalImpl.type + +instance : Nonempty Signal := by exact SignalImpl.property + +namespace Signal + +/-- +This creates a `Signal` in the initial state and doesn't start listening yet. +- If `repeating` is `false` this constructs a signal handler that resolves once when the specified + signal `signum` is received, then automatically stops listening. +- If `repeating` is `true` this constructs a signal handler that resolves each time the specified + signal `signum` is received and continues listening. A repeating signal handler will only be + freed after `Signal.stop` is called. +-/ +@[extern "lean_uv_signal_mk"] +opaque mk (signum : Int32) (repeating : Bool) : IO Signal + +/-- +This function has different behavior depending on the state and configuration of the `Signal`: +- if `repeating` is `false` and: + - it is initial, start listening and return a new `IO.Promise` that is set to resolve once + the signal `signum` is received. After this `IO.Promise` is resolved the `Signal` is finished. + - it is running or finished, return the same `IO.Promise` that the first call to `next` returned. +- if `repeating` is `true` and: + - it is initial, start listening and return a new `IO.Promise` that resolves when the next + signal `signum` is received. + - it is running, check whether the last returned `IO.Promise` is already resolved: + - If it is, return a new `IO.Promise` that resolves upon receiving the next signal + - If it is not, return the last `IO.Promise` + This ensures that the returned `IO.Promise` resolves at the next occurrence of the signal. + - if it is finished, return the last `IO.Promise` created by `next`. Notably this could be one + that never resolves if the signal handler was stopped before fulfilling the last one. + +The resolved `IO.Promise` contains the signal number that was received. +-/ +@[extern "lean_uv_signal_next"] +opaque next (signal : @& Signal) : IO (IO.Promise Int) + +/-- +This function has different behavior depending on the state of the `Signal`: +- If it is initial or finished this is a no-op. +- If it is running the signal handler is stopped and it is put into the finished state. + Note that if the last `IO.Promise` generated by `next` is unresolved and being waited + on this creates a memory leak and the waiting task is not going to be awoken anymore. +-/ +@[extern "lean_uv_signal_stop"] +opaque stop (signal : @& Signal) : IO Unit + +end Signal + +end UV +end Internal +end Std diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 45a7f511c6..cf9255c80b 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -3,7 +3,7 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp byteslice.cpp platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp -uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp) +uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp uv/signal.cpp) if (USE_MIMALLOC) list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c) # Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir diff --git a/src/runtime/libuv.cpp b/src/runtime/libuv.cpp index 664eb3b996..656e53dbed 100644 --- a/src/runtime/libuv.cpp +++ b/src/runtime/libuv.cpp @@ -20,6 +20,7 @@ extern "C" void initialize_libuv() { initialize_libuv_timer(); initialize_libuv_tcp_socket(); initialize_libuv_udp_socket(); + initialize_libuv_signal(); initialize_libuv_loop(); lthread([]() { event_loop_run_loop(&global_ev); }); diff --git a/src/runtime/libuv.h b/src/runtime/libuv.h index d476e8e58f..87fbcabc30 100644 --- a/src/runtime/libuv.h +++ b/src/runtime/libuv.h @@ -11,6 +11,7 @@ Author: Markus Himmel, Sofia Rodrigues #include "runtime/uv/tcp.h" #include "runtime/uv/dns.h" #include "runtime/uv/udp.h" +#include "runtime/uv/signal.h" #include "runtime/alloc.h" #include "runtime/io.h" #include "runtime/utf8.h" diff --git a/src/runtime/uv/signal.cpp b/src/runtime/uv/signal.cpp new file mode 100644 index 0000000000..2b290a6473 --- /dev/null +++ b/src/runtime/uv/signal.cpp @@ -0,0 +1,240 @@ +/* +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Sofia Rodrigues +*/ +#include "runtime/uv/signal.h" + +namespace lean { +#ifndef LEAN_EMSCRIPTEN + +using namespace std; + +// The finalizer of the `Signal`. +void lean_uv_signal_finalizer(void* ptr) { + lean_uv_signal_object * signal = (lean_uv_signal_object*) ptr; + + if (signal->m_promise != NULL) { + lean_dec(signal->m_promise); + } + + event_loop_lock(&global_ev); + + uv_close((uv_handle_t*)signal->m_uv_signal, [](uv_handle_t* handle) { + free(handle); + }); + + event_loop_unlock(&global_ev); + + free(signal); +} + +void initialize_libuv_signal() { + g_uv_signal_external_class = lean_register_external_class(lean_uv_signal_finalizer, [](void* obj, lean_object* f) { + if (((lean_uv_signal_object*)obj)->m_promise != NULL) { + lean_inc(f); + lean_apply_1(f, ((lean_uv_signal_object*)obj)->m_promise); + } + }); +} + +static bool signal_promise_is_finished(lean_uv_signal_object * signal) { + return lean_io_get_task_state_core((lean_object *)lean_to_promise(signal->m_promise)->m_result) == 2; +} + +void handle_signal_event(uv_signal_t* handle, int signum) { + lean_object * obj = (lean_object*)handle->data; + lean_uv_signal_object * signal = lean_to_uv_signal(obj); + + lean_assert(signal->m_state == SIGNAL_STATE_RUNNING); + lean_assert(signal->m_promise != NULL); + + if (signal->m_repeating) { + if (!signal_promise_is_finished(signal)) { + lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world()); + lean_dec(res); + } + } else { + lean_assert(!signal_promise_is_finished(signal)); + uv_signal_stop(signal->m_uv_signal); + signal->m_state = SIGNAL_STATE_FINISHED; + + lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world()); + lean_dec(res); + + lean_dec(obj); + } +} + +/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) { + int signum = (int)(int32_t)signum_obj; + + lean_uv_signal_object * signal = (lean_uv_signal_object*)malloc(sizeof(lean_uv_signal_object)); + signal->m_signum = signum; + signal->m_repeating = repeating; + signal->m_state = SIGNAL_STATE_INITIAL; + signal->m_promise = NULL; + + uv_signal_t * uv_signal = (uv_signal_t*)malloc(sizeof(uv_signal_t)); + + event_loop_lock(&global_ev); + int result = uv_signal_init(global_ev.loop, uv_signal); + event_loop_unlock(&global_ev); + + if (result != 0) { + free(uv_signal); + free(signal); + return lean_io_result_mk_error(lean_decode_uv_error(result, NULL)); + } + + signal->m_uv_signal = uv_signal; + + lean_object * obj = lean_uv_signal_new(signal); + lean_mark_mt(obj); + signal->m_uv_signal->data = obj; + + return lean_io_result_mk_ok(obj); +} + +/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /* w */ ) { + lean_uv_signal_object * signal = lean_to_uv_signal(obj); + + auto create_promise = []() { + lean_object * prom_res = lean_io_promise_new(lean_io_mk_world()); + lean_object * promise = lean_ctor_get(prom_res, 0); + lean_inc(promise); + lean_dec(prom_res); + + return promise; + }; + + auto setup_signal = [create_promise, obj, signal]() { + lean_assert(signal->m_promise == NULL); + signal->m_promise = create_promise(); + signal->m_state = SIGNAL_STATE_RUNNING; + + // The event loop must keep the signal alive for the duration of the run time. + lean_inc(obj); + + event_loop_lock(&global_ev); + + int result; + if (signal->m_repeating) { + result = uv_signal_start( + signal->m_uv_signal, + handle_signal_event, + signal->m_signum + ); + } else { + result = uv_signal_start_oneshot( + signal->m_uv_signal, + handle_signal_event, + signal->m_signum + ); + } + + event_loop_unlock(&global_ev); + + if (result != 0) { + lean_dec(obj); + return lean_io_result_mk_error(lean_decode_uv_error(result, NULL)); + } else { + lean_inc(signal->m_promise); + return lean_io_result_mk_ok(signal->m_promise); + } + }; + + if (signal->m_repeating) { + switch (signal->m_state) { + case SIGNAL_STATE_INITIAL: + { + return setup_signal(); + } + case SIGNAL_STATE_RUNNING: + { + lean_assert(signal->m_promise != NULL); + // 2 indicates finished + if (signal_promise_is_finished(signal)) { + lean_dec(signal->m_promise); + signal->m_promise = create_promise(); + lean_inc(signal->m_promise); + return lean_io_result_mk_ok(signal->m_promise); + } else { + lean_inc(signal->m_promise); + return lean_io_result_mk_ok(signal->m_promise); + } + } + case SIGNAL_STATE_FINISHED: + { + lean_assert(signal->m_promise != NULL); + lean_inc(signal->m_promise); + return lean_io_result_mk_ok(signal->m_promise); + } + } + } else { + if (signal->m_state == SIGNAL_STATE_INITIAL) { + return setup_signal(); + } else { + lean_assert(signal->m_promise != NULL); + + lean_inc(signal->m_promise); + return lean_io_result_mk_ok(signal->m_promise); + } + } +} + +/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /* w */) { + lean_uv_signal_object * signal = lean_to_uv_signal(obj); + + if (signal->m_state == SIGNAL_STATE_RUNNING) { + lean_assert(signal->m_promise != NULL); + + event_loop_lock(&global_ev); + int result = uv_signal_stop(signal->m_uv_signal); + event_loop_unlock(&global_ev); + + signal->m_state = SIGNAL_STATE_FINISHED; + + // The loop does not need to keep the signal alive anymore. + lean_dec(obj); + + if (result != 0) { + return lean_io_result_mk_error(lean_decode_uv_error(result, NULL)); + } else { + return lean_io_result_mk_ok(lean_box(0)); + } + } else { + return lean_io_result_mk_ok(lean_box(0)); + } +} + + +#else + +/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */ +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */) { + lean_always_assert( + false && ("Please build a version of Lean4 with libuv to invoke this.") + ); +} + +#endif + +} \ No newline at end of file diff --git a/src/runtime/uv/signal.h b/src/runtime/uv/signal.h new file mode 100644 index 0000000000..5d3b782b69 --- /dev/null +++ b/src/runtime/uv/signal.h @@ -0,0 +1,55 @@ +/* +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sofia Rodrigues +*/ +#pragma once +#include +#include "runtime/uv/event_loop.h" + +#ifndef LEAN_EMSCRIPTEN +#include +#endif + +namespace lean { + +static lean_external_class * g_uv_signal_external_class = NULL; +void initialize_libuv_signal(); + +#ifndef LEAN_EMSCRIPTEN +using namespace std; + +enum uv_signal_state { + SIGNAL_STATE_INITIAL, + SIGNAL_STATE_RUNNING, + SIGNAL_STATE_FINISHED, +}; + +// Structure for managing a single UV signal object, including promise handling, signal number, and +// repeating behavior. The repeating behavior exists to "set" a handler and avoid it not getting signals +// between the creation of oneshot signal handlers. +typedef struct { + uv_signal_t * m_uv_signal; // LibUV signal handle. + lean_object * m_promise; // The associated promise for asynchronous results. + int m_signum; // Signal number to watch for. + bool m_repeating; // Flag indicating if the signal handler is repeating. + uv_signal_state m_state; // The state of the signal. Beyond the API description on the Lean + // side this state has the invariant: + // `m_state != SIGNAL_STATE_INITIAL` -> `m_promise != NULL` +} lean_uv_signal_object; + +// ======================================= +// Signal object manipulation functions. +static inline lean_object* lean_uv_signal_new(lean_uv_signal_object * s) { return lean_alloc_external(g_uv_signal_external_class, s); } +static inline lean_uv_signal_object* lean_to_uv_signal(lean_object * o) { return (lean_uv_signal_object*)(lean_get_external_data(o)); } + +#endif + +// ======================================= +// Signal manipulation functions +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */); +extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */); + +} diff --git a/tests/pkg/signal/Main.lean b/tests/pkg/signal/Main.lean new file mode 100644 index 0000000000..ddca279806 --- /dev/null +++ b/tests/pkg/signal/Main.lean @@ -0,0 +1,41 @@ +import Std.Internal.Async.Signal +import Std.Internal.Async.Select +import Std.Internal.Async + +open Std.Internal.IO.Async + +def assertBEq [BEq α] [Repr α] (actual expected : α) : IO Unit := do + unless actual == expected do + throw <| IO.userError <| + s!"expected '{repr expected}', got '{repr actual}'" + +def select (signal1 signal2 signal3 signal4 : Signal.Waiter) : Async Signal := do + + 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))), + ] + + let signal ← await t + + IO.println s!"received {repr signal}" + pure signal + +def asyncMain : Async Unit := do + let signal1 ← Signal.Waiter.mk Signal.sigint true + let signal2 ← Signal.Waiter.mk Signal.sighup true + let signal3 ← Signal.Waiter.mk Signal.sigquit true + let signal4 ← Signal.Waiter.mk Signal.sigusr1 true + + 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/lakefile.toml b/tests/pkg/signal/lakefile.toml new file mode 100644 index 0000000000..5d3a00e236 --- /dev/null +++ b/tests/pkg/signal/lakefile.toml @@ -0,0 +1,5 @@ +name = "debug" + +[[lean_exe]] +name = "release" +root = "Main" \ No newline at end of file diff --git a/tests/pkg/signal/test.sh b/tests/pkg/signal/test.sh new file mode 100755 index 0000000000..3360ede029 --- /dev/null +++ b/tests/pkg/signal/test.sh @@ -0,0 +1,48 @@ +#!/usr/bin/env bash + +rm -rf .lake/build +lake build release + +# Create a named pipe for communication +PIPE=$(mktemp -u) +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 + + echo "Sending USR1 signal..." + kill -USR1 "$PID" 2>/dev/null || echo "Failed to send USR1" + + echo "Sending HUP signal..." + kill -HUP "$PID" 2>/dev/null || echo "Failed to send HUP" + + echo "Sending QUIT signal..." + kill -QUIT "$PID" 2>/dev/null || echo "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 +} + +# Clean up the pipe +rm -f "$PIPE" + +# 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 $?" +fi \ No newline at end of file