feat: link OpenSSL by algebraic-dev · Pull Request #12030 · leanprover/lean4

algebraic-dev · 2026-01-16T21:56:01Z

This PR links OpenSSL

ghost · 2026-01-16T23:17:00Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b994cb4497aed84187e8208e388888ec140ff935 --onto 3dfd125337305c9de6ddcc7c0330c50f0e39fb8e. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-16 23:16:59)

leanprover-bot · 2026-01-16T23:17:01Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b994cb4497aed84187e8208e388888ec140ff935 --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force reference manual CI using the force-manual-ci label. (2026-01-16 23:17:01)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a3cb39eac9e2d1f633fcd0b8561e6cd955f3c604 --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-07 00:12:10)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d2907b5c965e1865288ec2013a0c5e31d38f1c4e --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 04:53:43)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 13f8ce84929789d98b8e954d952b95869b4292f8 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-22 10:11:24)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 86175bea00f2d963a8c1367ac8ae67dd70ab32ea --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-23 22:29:29)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 337f1c455b3355fb9c4d50e55ab7ee4a875af6a1 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-28 17:53:25)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase da91aed2e2cc13d8c9463511b2f1833f7c961cc4 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-04 01:18:55)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cae4decead7dae180b50b25f2225419a1ed4280e --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-23 18:57:20)

mathlib-lean-pr-testing · 2026-03-07T00:12:09Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a3cb39eac9e2d1f633fcd0b8561e6cd955f3c604 --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-07 00:12:09)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d2907b5c965e1865288ec2013a0c5e31d38f1c4e --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 04:53:42)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 13f8ce84929789d98b8e954d952b95869b4292f8 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-22 10:11:23)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 13f8ce84929789d98b8e954d952b95869b4292f8 --onto 90b5e3185b3b948ce1c75281d3e95f370c8493a6. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-22 23:14:21)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 13f8ce84929789d98b8e954d952b95869b4292f8 --onto 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-23 14:22:44)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86175bea00f2d963a8c1367ac8ae67dd70ab32ea --onto 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-23 22:29:28)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86175bea00f2d963a8c1367ac8ae67dd70ab32ea --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-24 15:27:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 337f1c455b3355fb9c4d50e55ab7ee4a875af6a1 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-28 17:53:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase da91aed2e2cc13d8c9463511b2f1833f7c961cc4 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-04 01:18:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cae4decead7dae180b50b25f2225419a1ed4280e --onto 30a3fde8aa2968acce441fa37436e51acf55f376. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-23 18:57:18)

… works

TwoFX · 2026-05-04T12:14:12Z

+if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath,\\$$ORIGIN")
+endif()


What is going on here?

TwoFX · 2026-05-04T12:15:01Z

+if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  if(NOT LEAN_STANDALONE)
+    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  endif()
+endif()


Why do we need special handling for Windows? Does OPENSSL_LIBRARIES_STR not contain -lcrypt32 -lgdi32 on Windows?

TwoFX · 2026-05-04T12:18:08Z

 # and apparently since Sonoma does not do so implicitly either
 install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLEAN_STANDALONE=ON"
+echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"


I think we discussed that this should be removed in prepare-llvm-linux.sh, and I believe the same applies here.

algebraic-dev self-assigned this Jan 16, 2026

algebraic-dev marked this pull request as draft January 16, 2026 21:56

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 16, 2026

algebraic-dev force-pushed the sofia/openssl branch from 9e27f77 to bb745f8 Compare March 6, 2026 22:17

algebraic-dev marked this pull request as ready for review March 17, 2026 17:10

algebraic-dev requested a review from kim-em as a code owner March 17, 2026 17:10

algebraic-dev added changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases labels Mar 17, 2026

algebraic-dev requested a review from TwoFX March 17, 2026 17:12

algebraic-dev added release-ci Enable all CI checks for a PR, like is done for releases and removed release-ci Enable all CI checks for a PR, like is done for releases labels Mar 20, 2026

TwoFX reviewed Mar 30, 2026

View reviewed changes

Comment thread script/prepare-llvm-linux.sh Outdated

Comment thread script/prepare-llvm-macos.sh Outdated

Comment thread src/CMakeLists.txt Outdated

TwoFX reviewed Apr 13, 2026

View reviewed changes

Comment thread src/CMakeLists.txt Outdated

Comment thread script/prepare-llvm-linux.sh Outdated

algebraic-dev added 12 commits April 23, 2026 10:59

feat: start openssl

ef39c71

fix: remove tls

4a45aa9

feat: openssl nix

e882359

feat: add openssl to the guide

fb82174

feat: initialize openssl

67d015b

fix: openssl once

75646d7

fix: prepare

8bb1d8c

feat: openssl package

37fed7e

feat: openssl package

32f5e84

feat: openssl package

44f742b

fix: linux release

68f7c5b

fix: dev package

37ab265

algebraic-dev added 12 commits April 23, 2026 10:59

fix: linux release

085da27

fix: linux release

d499d80

fix: linux is statically linked now

a07c8b4

fix: linux is statically linked now

e9e3140

fix: openssl flake

c000da6

fix: patch shebangs

a3e01a0

fix: remove lean_extra_linker_flags to check if the stage2 and stage3…

6bf6932

… works

refactor: clean cmake

0ca4966

fix: remove check for openssl < 3

d223d6b

fix: comments

867c8b3

fix: move openssl linker flags after libc++ link

152acec

fix: components and test to check for path in nix env

8920478

algebraic-dev force-pushed the sofia/openssl branch from 9a4bf51 to 8920478 Compare April 23, 2026 14:20

algebraic-dev added 2 commits April 23, 2026 11:57

build: test

21e26e7

chore: remove useless change

7676ede

algebraic-dev requested a review from TwoFX April 24, 2026 16:26

TwoFX reviewed May 4, 2026

View reviewed changes

algebraic-dev requested a review from TwoFX May 4, 2026 12:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: link OpenSSL#12030

feat: link OpenSSL#12030
algebraic-dev wants to merge 26 commits intomasterfrom
sofia/openssl

algebraic-dev commented Jan 16, 2026

Uh oh!

ghost commented Jan 16, 2026

Uh oh!

leanprover-bot commented Jan 16, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Mar 7, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX May 4, 2026

Uh oh!

TwoFX May 4, 2026

Uh oh!

TwoFX May 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

algebraic-dev commented Jan 16, 2026

Uh oh!

ghost commented Jan 16, 2026

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX May 4, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX May 4, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX May 4, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-bot commented Jan 16, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Mar 7, 2026 •

edited

Loading