Skip to content

feat: introduce Std.Internal.SSL.Session - #14065

Open
algebraic-dev wants to merge 45 commits into
sofia/openssl-socket-contextfrom
sofia/openssl-socket-session
Open

feat: introduce Std.Internal.SSL.Session#14065
algebraic-dev wants to merge 45 commits into
sofia/openssl-socket-contextfrom
sofia/openssl-socket-session

Conversation

@algebraic-dev

@algebraic-dev algebraic-dev commented Jun 16, 2026

Copy link
Copy Markdown
Member

This PR adds Session.Server and Server.Client types for managing an in memory TLS state machine backed by OpenSSL BIOs on the Lean side.

@algebraic-dev algebraic-dev self-assigned this Jun 16, 2026
@algebraic-dev
algebraic-dev requested a review from TwoFX as a code owner June 16, 2026 04:28
@algebraic-dev algebraic-dev changed the title feat: SSL Session feat: introduce Std.Internal.SSL.Session Jun 16, 2026
@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 16, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jun 16, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-16 05:09:47)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 24c48fe0fdbf4bca5b6f907e638732c871dcd2db. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-16 10:43:55)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 10:25:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 0758b1d2e33c65ccea578abb0c668aab1f811608. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-27 23:19:08)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 068011713f00d41059c2346d97fbb41ec4daf576 --onto 41b2fe837a74f3d3449816e58dd6219eac034ff7. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-04 14:01:11)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-15 19:04:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 875b6b5bcf293b6ce17ea6a1a977363f1b51d66b --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 00:38:49)
  • ✅ Mathlib branch lean-pr-testing-14065 has successfully built against this PR. (2026-09-02 18:38:36) View Log
  • ✅ Mathlib branch lean-pr-testing-14065 has successfully built against this PR. (2026-09-02 22:36:11) View Log

@leanprover-bot

leanprover-bot commented Jun 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-16 05:09:48)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto 84b251f7390c20a0a00a221050ab4a6e6c46a191. You can force reference manual CI using the force-manual-ci label. (2026-06-27 23:19:09)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 068011713f00d41059c2346d97fbb41ec4daf576 --onto e281ba87c2c967b1662ee28bd201046956d0494a. You can force reference manual CI using the force-manual-ci label. (2026-07-04 14:01:13)
  • ✅ Reference manual branch lean-pr-testing-14065 has successfully built against this PR. (2026-08-15 19:09:35) View Log
  • 🟡 Reference manual branch lean-pr-testing-14065 build against this PR didn't complete normally. (2026-08-15 19:10:48) View Log
  • ✅ Reference manual branch lean-pr-testing-14065 has successfully built against this PR. (2026-08-20 13:11:10) View Log
  • 🟡 Reference manual branch lean-pr-testing-14065 build against this PR didn't complete normally. (2026-08-20 13:13:18) View Log
  • ✅ Reference manual branch lean-pr-testing-14065 has successfully built against this PR. (2026-08-20 21:08:41) View Log
  • 🟡 Reference manual branch lean-pr-testing-14065 build against this PR didn't complete normally. (2026-08-20 21:09:50) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 875b6b5bcf293b6ce17ea6a1a977363f1b51d66b --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 00:38:50)
  • ✅ Reference manual branch lean-pr-testing-14065 has successfully built against this PR. (2026-09-02 17:12:38) View Log
  • 🟡 Reference manual branch lean-pr-testing-14065 build against this PR didn't complete normally. (2026-09-02 17:13:34) View Log
  • 💥 Reference manual branch lean-pr-testing-14065 build failed against this PR. (2026-09-02 21:41:00) View Log
  • 🟡 Reference manual branch lean-pr-testing-14065 build against this PR didn't complete normally. (2026-09-02 21:41:08) View Log

@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
b7782ae 
…-session
@algebraic-dev
fix: read 0 bug
1c628b6
@algebraic-dev
fix: add clear error in session functions
29dda2e
@algebraic-dev
fix: max size of recv?
38b1359
@algebraic-dev
feat: unespecified
a41fa06
@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
db48940 
…-session
@algebraic-dev
test: fix path of tests
ece36f9
@algebraic-dev
test: tempdir for tests
5ddc34d
@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
28e9f5f 
…-session
@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
bbdc510 
…-session
@algebraic-dev
fix: comments and set server name
23b638b
@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
63c4803 
…-session
@algebraic-dev
test: configure + mk
ee23663
@algebraic-dev
Merge branch 'sofia/openssl-socket-context' into sofia/openssl-socket…
d7a31de 
…-session
@algebraic-dev
test: make it not depend on openssl cli
08e9ae7
TwoFX
TwoFX reviewed Aug 12, 2026
View reviewed changes

@TwoFX TwoFX left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Here

Comment thread src/runtime/openssl/session.h Outdated
Comment thread src/runtime/openssl/session.cpp Outdated
Comment thread src/runtime/openssl/session.cpp Outdated
Comment thread src/runtime/openssl/session.cpp Outdated
Comment thread src/runtime/openssl/session.cpp Outdated
Comment thread tests/elab/async_ssl_session.lean Outdated
Comment thread src/Std/Internal/SSL/Session.lean Outdated
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 20, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14065
abc177d
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 20, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14065
a430c90
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Sep 2, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 2, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14065
4eee99d
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 2, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14065
eeaae9b
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 2, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14065
a1cec37
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 2, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14065
c7b7a39
@leanprover-bot leanprover-bot added breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. and removed builds-manual CI has verified that the Lean Language Reference builds against this PR labels Sep 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX left review comments

Assignees

@algebraic-dev algebraic-dev

Labels

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

3 participants

@algebraic-dev @leanprover-bot @TwoFX