Auto-discover libpython via python3 sysconfig

The Python-in-Lean bridge previously only tried (a) libpython already
loaded into the host process, (b) LEANPY_LIBPYTHON, and (c) common
sonames via the dyld search path. On a typical pyenv / uv / framework
install, none of those find anything, so opening Main.lean in VS Code
and #eval'ing a function that calls into the bridge would fail with
'could not load libpython'.

Add step (3.5): popen("python3 -c '<sysconfig snippet>'") and dlopen
the printed path. Falls through to the soname list if python3 isn't
on PATH or returns nothing useful.

This means the typed-numpy example now works in #eval inside VS Code
with no env var fiddling, as long as python3 on PATH has numpy
importable.

Author: kiranandcode

LeanPy/native/python_bridge.c

@@ -263,21 +263,57 @@ static const char *const PY_CANDIDATES[] = {
     NULL
 };
 
+/* Ask `python3` (or `python`) on PATH where its own libpython lives.
+ * This handles pyenv / uv-managed / framework Pythons whose libdir
+ * isn't on the dyld search path. The call is one-shot and only runs
+ * during the first `LeanPy.Python.init`. */
+static int try_python_subprocess(const char *python_exe) {
+    char cmd[512];
+    int n = snprintf(cmd, sizeof(cmd),
+        "%s -c 'import os, sysconfig; "
+        "libdir = sysconfig.get_config_var(\"LIBDIR\"); "
+        "soname = sysconfig.get_config_var(\"INSTSONAME\") "
+                 "or sysconfig.get_config_var(\"LDLIBRARY\"); "
+        "print(os.path.join(libdir, soname) "
+              "if libdir and soname else \"\")' 2>/dev/null",
+        python_exe);
+    if (n <= 0 || (size_t)n >= sizeof(cmd)) return 0;
+    FILE *fp = popen(cmd, "r");
+    if (!fp) return 0;
+    char buf[4096];
+    char *line = fgets(buf, sizeof(buf), fp);
+    pclose(fp);
+    if (!line) return 0;
+    size_t len = strlen(line);
+    while (len > 0 && (line[len-1] == '\n' || line[len-1] == '\r')) line[--len] = '\0';
+    if (len == 0) return 0;
+    py_handle = dlopen(line, RTLD_NOW | RTLD_GLOBAL);
+    return py_handle != NULL;
+}
+
 static int try_load_python(void) {
-    /* First, prefer libpython already loaded into the process (this is
-     * the typical case when LeanPy runs inside a Python host — using a
-     * different libpython would cause two independent CPython VMs and
-     * immediate crashes). */
+    /* 1. Prefer libpython already loaded into the process (this is
+     *    the typical case when LeanPy runs inside a Python host —
+     *    using a different libpython would cause two independent
+     *    CPython VMs and immediate crashes). */
     py_handle = dlopen(NULL, RTLD_LAZY);
     if (py_handle && dlsym(py_handle, "Py_Initialize")) return 1;
     py_handle = NULL;
 
-    /* Honour LEANPY_LIBPYTHON if set. */
+    /* 2. Honour LEANPY_LIBPYTHON if set. */
     const char *override = getenv("LEANPY_LIBPYTHON");
     if (override && *override) {
         py_handle = dlopen(override, RTLD_NOW | RTLD_GLOBAL);
         if (py_handle) return 1;
     }
+
+    /* 3. Ask python3 / python on PATH for its libpython. Catches
+     *    pyenv, uv, and framework installs whose lib dir isn't in
+     *    the dyld search path. */
+    if (try_python_subprocess("python3")) return 1;
+    if (try_python_subprocess("python")) return 1;
+
+    /* 4. Fall back to common sonames (relies on dyld search path). */
     for (int i = 0; PY_CANDIDATES[i]; i++) {
         py_handle = dlopen(PY_CANDIDATES[i], RTLD_NOW | RTLD_GLOBAL);
         if (py_handle) return 1;

examples/03_numpy_typed/README.md

@@ -27,9 +27,16 @@ Storage and arithmetic are forwarded to numpy via `LeanPy.Python` —
 the phantom types are erased at runtime.
 
 There is no Python driver. `lake build` produces a binary at
-`lean/.lake/build/bin/demo`; the `run` wrapper at the example root
-just sets `LEANPY_LIBPYTHON` to a `libpython3.X` and runs the binary
-with `uv run` so numpy from the local venv is on `sys.path`.
+`lean/.lake/build/bin/demo`. The bridge auto-discovers `libpython` by
+asking `python3` on PATH for its sysconfig, so the binary runs as long
+as a `python3` with `numpy` is on PATH. The `run` wrapper at the
+example root just runs the binary under `uv run` so the local venv's
+numpy is picked up.
+
+You can also load `Main.lean` in VS Code and `#eval runDemo` directly
+— the same auto-discovery kicks in inside the Lean LSP. (If you're on
+a setup where `python3` on PATH doesn't have numpy installed, set
+`LEANPY_LIBPYTHON` and `PYTHONPATH` in your shell to override.)
 
 ## Layout
 

examples/03_numpy_typed/run

@@ -1,18 +1,9 @@
 #!/usr/bin/env bash
-# Build and run the typed-numpy Lean executable, picking up libpython
-# and numpy from the local uv venv.
+# Build and run the typed-numpy Lean executable, with the local uv venv
+# active so numpy is on python3's sys.path. The bridge now discovers
+# libpython itself by asking python3 — no env var needed in most cases.
 set -euo pipefail
 
 cd "$(dirname "$0")"
 (cd lean && lake build)
-
-# `uv run` activates the venv (so numpy is on sys.path); PYTHONHOME
-# stays unset on purpose — letting libpython use the venv's prefix.
-export LEANPY_LIBPYTHON=$(uv run -- python -c '
-import os, sysconfig
-libdir = sysconfig.get_config_var("LIBDIR")
-soname = sysconfig.get_config_var("INSTSONAME") or sysconfig.get_config_var("LDLIBRARY")
-print(os.path.join(libdir, soname) if soname else "")
-')
-
 exec uv run -- ./lean/.lake/build/bin/demo "$@"