New here? Start at leanprover/lp — the entry point for the lp / maximize tactics and the verified LP solver. This repository is one package of that family: the raw SoPlex FFI bindings.

Lean 4 FFI bindings for SoPlex, the linear programming solver from the SCIP optimization suite.

This repository contains the direct binding only: the vendored SoPlex build, the C++ bridge, Lean extern wrappers, marshalling, direct solve APIs, and MPS / LP file I/O. The verified Lean layer lives in leanprover/lp.

System dependencies:

git clone --recurse-submodules https://github.com/leanprover/soplex-ffi
cd soplex-ffi
lake exe ffi-check

If you cloned without submodules, Lake attempts to initialize the vendored SoPlex submodule automatically. If that fails, run git submodule update --init --recursive.

SoplexFFI.lean          # direct FFI package entry point
SoplexFFI/              # thin Lean API, types, and validation
ffi/                    # C++ bridge and C ABI entry points
vendor/soplex           # vendor submodule (scipopt/soplex, tag v8.0.2)
lakefile.lean           # Lake package and extern_lib build

SoplexFFI is licenced under the Apache License 2.0, matching SoPlex itself. The compiled binary's GMP runtime dependency (LGPL) is linked dynamically by default. SoPlex itself is linked into the Lean shared library from the vendored static archive.