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.

Sign up for GitHub

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

Jump to bottom

feat: Std.Net.Addr #6563

Merged
merged 10 commits into from
Jan 9, 2025
Merged

feat: Std.Net.Addr #6563

merged 10 commits into from
Jan 9, 2025

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Jan 7, 2025 •
edited
Loading

This PR implements Std.Net.Addr which contains structures around IP and socket addresses.

While we could implement our own parser instead of going through the addr_in/addr_in6 route we will need to implement these conversions to make proper system calls anyway. Hence this is likely the approach with the least amount of non trivial code overall. The only thing I am uncertain about is whether ofString should return Option or Except, unfortunately libuv doesn't hand out error messages on IP parsing.

@hargoniX hargoniX added release-ci Enable all CI checks for a PR, like is done for releases changelog-library Library labels Jan 7, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 7, 2025 13:02 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 7, 2025 13:22 Inactive
@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 Jan 7, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6563
9e7e518
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6563
901eea7
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 7, 2025 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 7, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 7, 2025 16:56 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
5c9b081
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
ecdef1c
@hargoniX hargoniX marked this pull request as ready for review January 7, 2025 20:10
@hargoniX hargoniX requested a review from TwoFX as a code owner January 7, 2025 20:10
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 7, 2025 20:21 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 7, 2025 21:17 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
086a2e4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 7, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
174df6d
kim-em
kim-em reviewed Jan 8, 2025
View reviewed changes
kim-em
kim-em reviewed Jan 8, 2025
View reviewed changes
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2025 08:45 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 8, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
669fbee
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
4e17822
TwoFX
TwoFX reviewed Jan 8, 2025
View reviewed changes
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2025 14:06 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 8, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
c950d61
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6563
b70bfaf
@hargoniX hargoniX added this pull request to the merge queue Jan 9, 2025
Merged via the queue into master with commit a6789a7 Jan 9, 2025
23 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@hargoniX @luisacicolini
feat: Std.Net.Addr (leanprover#6563)
d51a8c7 
This PR implements `Std.Net.Addr` which contains structures around IP
and socket addresses.

While we could implement our own parser instead of going through the
`addr_in`/`addr_in6` route we will need to implement these conversions
to make proper system calls anyway. Hence this is likely the approach
with the least amount of non trivial code overall. The only thing I am
uncertain about is whether `ofString` should return `Option` or
`Except`, unfortunately `libuv` doesn't hand out error messages on IP
parsing.
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@hargoniX @JovanGerb
feat: Std.Net.Addr (leanprover#6563)
7ad856a 
This PR implements `Std.Net.Addr` which contains structures around IP
and socket addresses.

While we could implement our own parser instead of going through the
`addr_in`/`addr_in6` route we will need to implement these conversions
to make proper system calls anyway. Hence this is likely the approach
with the least amount of non trivial code overall. The only thing I am
uncertain about is whether `ofString` should return `Option` or
`Except`, unfortunately `libuv` doesn't hand out error messages on IP
parsing.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@TwoFX TwoFX TwoFX approved these changes

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@hargoniX @leanprover-community-bot @kim-em @TwoFX