feat: introduce `Std.Internal.SSL.Context` by algebraic-dev · Pull Request #14064 · leanprover/lean4

algebraic-dev · 2026-06-16T04:25:29Z

This PR adds the Context type for managing SSL_CTX on the Lean side.

mathlib-lean-pr-testing · 2026-06-16T05:05:28Z

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:05:27)
❗ 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:36:03)
❗ 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:24:23)
❗ 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-26 11:28:06)
❗ 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 15:04:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0d9dae19efbf6e9be542ef39d96bb86981837e1e --onto 41b2fe837a74f3d3449816e58dd6219eac034ff7. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-05 03:40:57)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e8a9ebad99e0a41dbd7655f5a4e9993d4dc07f1 --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-21 14:36:56)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a2c74ef85a8212503551663871b90d0d51b7417f --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-24 22:17:48)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a39eab69e1eee9ad38f4efe507907b1026a77808 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-28 17:04:49)
❗ 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-11 18:01:07)
❗ 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-20 22:11:05)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 875b6b5bcf293b6ce17ea6a1a977363f1b51d66b --onto 138ca9f20763523c4093baa092cf371e89535098. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-01 00:05:06)

leanprover-bot · 2026-06-16T05:05:29Z

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:05:29)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9566c798d09abdf266a00eae67a9b1188c6df36e --onto c500da3e893f814e54e3392d5d637085fac8bc37. You can force reference manual CI using the force-manual-ci label. (2026-06-26 11:28:07)
❗ 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 17:25:46)
❗ 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 15:04:52)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0d9dae19efbf6e9be542ef39d96bb86981837e1e --onto e281ba87c2c967b1662ee28bd201046956d0494a. You can force reference manual CI using the force-manual-ci label. (2026-07-05 03:40:59)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0e8a9ebad99e0a41dbd7655f5a4e9993d4dc07f1 --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-21 14:36:58)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a2c74ef85a8212503551663871b90d0d51b7417f --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-24 22:17:50)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a2c74ef85a8212503551663871b90d0d51b7417f --onto fed67d987430595cddf0ee209f0b12dc69f182b5. You can force reference manual CI using the force-manual-ci label. (2026-07-25 13:18:19)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a39eab69e1eee9ad38f4efe507907b1026a77808 --onto aa89d2777fb4342ff3084502e8f2d5a01aa17222. You can force reference manual CI using the force-manual-ci label. (2026-07-28 17:04:50)
✅ Reference manual branch lean-pr-testing-14064 has successfully built against this PR. (2026-08-11 18:07:36) View Log
🟡 Reference manual branch lean-pr-testing-14064 build against this PR didn't complete normally. (2026-08-11 18:09:11) View Log
✅ Reference manual branch lean-pr-testing-14064 has successfully built against this PR. (2026-08-12 00:09:44) View Log
🟡 Reference manual branch lean-pr-testing-14064 build against this PR didn't complete normally. (2026-08-12 00:10:24) View Log
✅ Reference manual branch lean-pr-testing-14064 has successfully built against this PR. (2026-08-13 00:20:48) View Log
🟡 Reference manual branch lean-pr-testing-14064 build against this PR didn't complete normally. (2026-08-13 00:21:19) 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-20 22:11:07)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 875b6b5bcf293b6ce17ea6a1a977363f1b51d66b --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force reference manual CI using the force-manual-ci label. (2026-09-01 00:05:08)

TwoFX

Just a superficial pass, I'll need to read this again on Monday.

…ia/openssl-socket-context

TwoFX

Looks good, though I'd like to see a test for the error message for the ill-formed certFile/keyFile/caFile errors.

After that, feel free to merge.

…ia/openssl-socket-context

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…ia/openssl-socket-context

algebraic-dev added 2 commits June 16, 2026 01:20

feat: openssl context

48b4e4a

style: remove useless comment

bd5ac47

algebraic-dev self-assigned this Jun 16, 2026

algebraic-dev requested a review from TwoFX as a code owner June 16, 2026 04:25

algebraic-dev added the changelog-library Library label Jun 16, 2026

algebraic-dev changed the title ~~feat: SSL Context~~ feat: introduce Std.Internal.SSL.Session Jun 16, 2026

algebraic-dev changed the title ~~feat: introduce Std.Internal.SSL.Session~~ feat: introduce Std.Internal.SSL.Context Jun 16, 2026

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

algebraic-dev added 4 commits June 16, 2026 07:03

refactor: remove CRL related functions

03ce4e3

feat: enable verifyPeer, it doesnt add system rots when it's not empty

6328596

test: fix path of tests

7ca2c14

test: tempdir for tests

7827493

TwoFX reviewed Jun 25, 2026

View reviewed changes

Comment thread src/runtime/openssl/context.cpp Outdated

Comment thread src/runtime/openssl/context.cpp Outdated

Comment thread src/runtime/openssl/context.h Outdated

algebraic-dev added 2 commits June 26, 2026 07:53

fix: suggesitions and more clear error queue

68ebe80

fix: read system certificate instead of OpenSSL bundle

76dea57

algebraic-dev added the release-ci Enable all CI checks for a PR, like is done for releases label Jun 26, 2026

algebraic-dev requested a review from TwoFX June 26, 2026 19:06

algebraic-dev added 11 commits June 26, 2026 18:39

fix: cmake for windows and macos security

861455f

feat: add extra macos security flags

52e05aa

feat: copy MacOS frameworks

af0c518

fix: disable cache on server and client contexts

68dbe1e

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

14d4713

…ia/openssl-socket-context

feat: join mk and configure

2d035fc

test: make it not depend on openssl cli

bcf7317

test: make a folder to all tests to avoid calling openssl cli

2eb9f5b

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

c1c204d

…ia/openssl-socket-context

fix: borrowing issue

d5aa8d3

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

c7365db

…ia/openssl-socket-context

algebraic-dev added release-ci Enable all CI checks for a PR, like is done for releases merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. and removed release-ci Enable all CI checks for a PR, like is done for releases labels Jul 28, 2026

TwoFX reviewed Aug 11, 2026

View reviewed changes

Comment thread src/runtime/openssl/context.cpp Outdated

Comment thread src/runtime/openssl/context.cpp Outdated

Comment thread src/runtime/openssl/context.cpp

Comment thread src/runtime/openssl/context.cpp Outdated

fix: null check, error messages and emscripten

8dceee7

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Aug 11, 2026

algebraic-dev requested a review from TwoFX August 11, 2026 23:26

chore: comment

485d297

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 12, 2026

Update lean-toolchain for leanprover/lean4#14064

602e2e9

TwoFX approved these changes Aug 12, 2026

View reviewed changes

algebraic-dev added 2 commits August 12, 2026 20:30

test: add tests for each one of the possible errors

daf29d8

style: linebreaks

e2dca67

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 13, 2026

Update lean-toolchain for leanprover/lean4#14064

4774319

algebraic-dev added 4 commits August 15, 2026 13:35

fix: client_from_pem possible misusage

923b981

fix: winstore

82a2fe9

feat: empty pw key test

33a7fb9

fix: reject encrypted PEM before it can prompt on the terminal

718e0a2

TwoFX reviewed Aug 17, 2026

View reviewed changes

Comment thread src/runtime/openssl/context.cpp Outdated

algebraic-dev and others added 11 commits August 18, 2026 20:43

fix: add trust_store that caches the certificates for TLS

b4b9997

fix: remove dot

1593807

fix: change call_once

7f2ca15

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

b70101e

…ia/openssl-socket-context

fix: remove unexistent import

acab160

fix: move keychain anchor globals into the Apple branch

6829a53

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

fix: remove stray test

076f694

fix: trust system roots while loading ca

51ec8ee

fix: load certificate from path or text

2e83967

feat: allow partial chain

6520b05

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

00e991d

…ia/openssl-socket-context

Navigation Menu

Uh oh!

feat: introduce `Std.Internal.SSL.Context` - #14064

feat: introduce `Std.Internal.SSL.Context`#14064
algebraic-dev wants to merge 43 commits into
masterfrom
sofia/openssl-socket-context

algebraic-dev commented Jun 16, 2026

Uh oh!

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

edited

Loading

Uh oh!

leanprover-bot commented Jun 16, 2026 •

edited

Loading

Uh oh!

TwoFX left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

algebraic-dev commented Jun 16, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

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

edited

Loading

leanprover-bot commented Jun 16, 2026 •

edited

Loading