sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

Map signals on c++ side to actual values

Browse Source
This commit is contained in:
Joscha
2026-03-16 18:48:44 +01:00
parent e5b3a41247
commit 5713082070
2 changed files with 31 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
src/Std/Internal/Async/Signal.lean
View File

@@ -159,9 +159,12 @@ deriving Repr, DecidableEq, BEq
namespace Signal
/--
Converts a `Signal` to its corresponding `Int32` value as defined in the libc `signal.h` or `man 7 signal`.
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

26
src/runtime/uv/signal.cpp
View File

@@ -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;