revert: int cast

Co-authored-by: Markus Himmel <markus@lean-fro.org>

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

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
+  }

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

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

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

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); });

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"

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
+
+}

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 <lean/lean.h>
+#include "runtime/uv/event_loop.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+#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 */);
+
+}

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

tests/pkg/signal/lakefile.toml

@@ -0,0 +1,5 @@
+name = "debug"
+
+[[lean_exe]]
+name = "release"
+root = "Main"

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