Skip to content

fix: use process signal numbers from correct architecture#12900

Merged
Garmelon merged 3 commits intomasterfrom
joscha/fix-signal-numbers
Mar 17, 2026
Merged

fix: use process signal numbers from correct architecture#12900
Garmelon merged 3 commits intomasterfrom
joscha/fix-signal-numbers

Conversation

@Garmelon
Copy link
Copy Markdown
Contributor

@Garmelon Garmelon commented Mar 12, 2026

This PR fixes some process signals that were incorrectly numbered.

From what I can tell, the code used signals and signal numbers for Alpha/SPARC, not x86/ARM. The test was also broken and always green, hiding the mistake.

@Garmelon Garmelon requested a review from algebraic-dev March 12, 2026 18:14
@Garmelon Garmelon requested a review from TwoFX as a code owner March 12, 2026 18:14
@Garmelon Garmelon added the changelog-library Library label Mar 12, 2026
@Garmelon Garmelon marked this pull request as draft March 12, 2026 18:26
@Garmelon Garmelon force-pushed the joscha/fix-signal-numbers branch 2 times, most recently from 6699672 to 18bf81a Compare March 12, 2026 18:31
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 12, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 12, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47833725eaded4cec8cc7944ab656eaf05208da7 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-12 19:21:19)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 49715fe63cf9181114c3dafc94f1b8490af41276 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-16 18:41:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 49715fe63cf9181114c3dafc94f1b8490af41276 --onto 6714601ee4a123fef0f6ff3e44f01086ba78dfce. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-17 14:02:20)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 12, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 47833725eaded4cec8cc7944ab656eaf05208da7 --onto 24acf2b895670fdeeafc64c4f606e7a0ebc19e6d. You can force reference manual CI using the force-manual-ci label. (2026-03-12 19:21:21)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 49715fe63cf9181114c3dafc94f1b8490af41276 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-16 18:41:19)

@Garmelon Garmelon marked this pull request as ready for review March 13, 2026 08:34
@algebraic-dev
Copy link
Copy Markdown
Member

algebraic-dev commented Mar 16, 2026

Maybe we should remove the toInt32 function and perform the translation on the C++ side using the constants, since the code needs to run on multiple operating systems and architectures, just to make sure it works correctly every time. What do you think? I also think that the behavior between your branch and the master branch differs on MacOS for this code:

def main : IO Unit := Async.block do
  let waiter ← Signal.Waiter.mk .sigusr1 false
  IO.println "Waiting for SIGUSR1..."
  discard <| await (← waiter.wait)
  IO.println "Received SIGUSR1!"

In macOS the master branch captures the signal, in your branch it just kills the process.

@Garmelon Garmelon force-pushed the joscha/fix-signal-numbers branch from 18bf81a to 5713082 Compare March 16, 2026 17:48
@Garmelon
Copy link
Copy Markdown
Contributor Author

Garmelon commented Mar 16, 2026

Would something like this work? I don't have a mac to test against.

@algebraic-dev
Copy link
Copy Markdown
Member

It works on macOS now.

@Garmelon Garmelon added this pull request to the merge queue Mar 16, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 16, 2026
@Garmelon
Copy link
Copy Markdown
Contributor Author

I think the test is flaky when other tests are running in parallel

@Garmelon Garmelon force-pushed the joscha/fix-signal-numbers branch from f0e2251 to f011392 Compare March 17, 2026 13:15
@Garmelon Garmelon enabled auto-merge March 17, 2026 13:19
@Garmelon Garmelon added this pull request to the merge queue Mar 17, 2026
Merged via the queue into master with commit 7c011aa Mar 17, 2026
15 checks passed
@Garmelon Garmelon deleted the joscha/fix-signal-numbers branch March 17, 2026 14:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants