Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: link LibUV #4963

Merged
merged 17 commits into from
Aug 12, 2024
Merged

feat: link LibUV #4963

merged 17 commits into from
Aug 12, 2024

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Aug 8, 2024

No description provided.

@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 Aug 8, 2024
@ydewit
Copy link
Contributor

ydewit commented Aug 8, 2024

It is great to see libuv being integrated into the runtime! May I ask what is the goal? Cross-platform file/network/time IO? Or also non-blocking IO?

@TwoFX
Copy link
Member Author

TwoFX commented Aug 9, 2024

@ydewit Yes, the ultimate goal is support for non-blocking IO. Note however that this PR only links against LibUV and it might take a very long time until we actually start building anything on top of it, so if you have need for asynchronous IO right now then it probably makes sense to explore alternatives such as lean-libuv for now.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 07:16 Inactive
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Aug 9, 2024

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bcbd7299e94f481c2691c3d4d74f427b44f70968 --onto 7776852d227d4269e34fe30eb51ba0adef90838e. (2024-08-09 07:18:47)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a52b794a39256361050c52fe0e41bbff91bc8d --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 15:38:33)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 07:45 Inactive
Copy link
Contributor

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

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

We should probably add to the docs page on building Lean that you need to have libuv installed right? Alternatively we could do something similar to the CaDiCal PR and declare libuv as an external project that gets downloaded and compiled by our build system directly.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 08:42 Inactive
@TwoFX
Copy link
Member Author

TwoFX commented Aug 9, 2024

We should probably add to the docs page on building Lean that you need to have libuv installed right? Alternatively we could do something similar to the CaDiCal PR and declare libuv as an external project that gets downloaded and compiled by our build system directly.

Thanks, I've updated the build instructions. We don't want to build libuv as part of our build system, but use either system libraries (when building manually) or take static libraries from Nix (when creating release versions via CI), just as we do it with GMP.

@TwoFX TwoFX marked this pull request as ready for review August 9, 2024 08:49
@TwoFX TwoFX requested review from Kha and kim-em as code owners August 9, 2024 08:49
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 08:51 Inactive
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Aug 9, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:03 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:09 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:17 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:26 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:55 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 14:00 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 14:52 Inactive
@TwoFX TwoFX requested a review from Kha August 9, 2024 16:14
@TwoFX TwoFX added the will-merge-soon …unless someone speaks up label Aug 12, 2024
@TwoFX TwoFX added this pull request to the merge queue Aug 12, 2024
Merged via the queue into master with commit c237c1f Aug 12, 2024
25 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants