Skip to content

Conversation

@algebraic-dev
Copy link
Member

This PR adds a function called lean_setup_libuv that initializes required LIBUV components. It needs to be outside of lean_initialize_runtime_module because it requires argv and argc to work correctly.

@algebraic-dev algebraic-dev self-assigned this Jun 4, 2025
@algebraic-dev algebraic-dev added the changelog-compiler Compiler, runtime, and FFI label Jun 4, 2025
@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 Jun 4, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jun 4, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e08b2a1f62238f7f817c719e4fffcfef14243338 --onto c12159b51982221bdd66f0c5997f85e1f9d91772. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-04 23:23:00)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e08b2a1f62238f7f817c719e4fffcfef14243338 --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 16:00:12)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e08b2a1f62238f7f817c719e4fffcfef14243338 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-20 23:13:14)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e08b2a1f62238f7f817c719e4fffcfef14243338 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-26 13:02:30)

@algebraic-dev algebraic-dev marked this pull request as ready for review June 5, 2025 01:38
@eric-wieser
Copy link
Contributor

This presumably makes progress on #5819 ?

@algebraic-dev
Copy link
Member Author

This presumably makes progress on #5819 ?

Not exactly, LibUV provides some functions like uv_exepath that can get the executable path but it's not exactly the same as argv[0]

Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FFI changes LGTM except for the documentation comments. I didn't check the compiler changes.

Co-authored-by: Eric Wieser <[email protected]>
@algebraic-dev algebraic-dev added this pull request to the merge queue Jun 27, 2025
Merged via the queue into master with commit 0f2cb91 Jun 27, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI 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.

6 participants