mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
fix: use process signal numbers from correct architecture
This PR fixes some process signals that were incorrectly numbered.
This commit is contained in:
@@ -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.
|
||||
Child status has changed.
|
||||
-/
|
||||
| sigurg
|
||||
|
||||
/--
|
||||
Stop typed at tty.
|
||||
-/
|
||||
| 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,26 +145,21 @@ inductive Signal
|
||||
| sigwinch
|
||||
|
||||
/--
|
||||
Status request from keyboard.
|
||||
I/O now possible.
|
||||
-/
|
||||
| siginfo
|
||||
| sigio
|
||||
|
||||
/--
|
||||
User-defined signal 1.
|
||||
Bad system call.
|
||||
-/
|
||||
| sigusr1
|
||||
|
||||
/--
|
||||
User-defined signal 2.
|
||||
-/
|
||||
| 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 the libc `signal.h` or `man 7 signal`.
|
||||
-/
|
||||
def toInt32 : Signal → Int32
|
||||
| .sighup => 1
|
||||
@@ -175,25 +167,23 @@ def toInt32 : Signal → Int32
|
||||
| .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.
|
||||
|
||||
@@ -309,7 +309,6 @@ add_dir_of_test_dirs(misc_dir)
|
||||
add_dir_of_test_dirs(
|
||||
pkg
|
||||
EXCEPT
|
||||
signal # Test appears to be broken
|
||||
test_extern # Flaky
|
||||
user_ext # Test started being nondeterministic
|
||||
)
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
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
|
||||
function await_line(){
|
||||
read -r line < "$PIPE"
|
||||
echo "Received line: $line"
|
||||
sleep 1
|
||||
}
|
||||
|
||||
await_line
|
||||
echo "Sending USR1 signal..."
|
||||
kill -USR1 "$PID" 2>/dev/null || fail "Failed to send USR1"
|
||||
|
||||
await_line
|
||||
echo "Sending HUP signal..."
|
||||
kill -HUP "$PID" 2>/dev/null || fail "Failed to send HUP"
|
||||
|
||||
await_line
|
||||
echo "Sending QUIT signal..."
|
||||
kill -QUIT "$PID" 2>/dev/null || fail "Failed to send QUIT"
|
||||
|
||||
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
|
||||
|
||||
Reference in New Issue
Block a user