LPBackendSoplexFFI

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 SoPlex FFI backend adapter (priority 10, the default).

LPBackend adapter for the SoPlex FFI binding. Wraps the synchronous LP.solveExact from leanprover/soplex-ffi into the abstract LPBackend record defined in leanprover/lp-core, and self-registers with the leanprover/lp-tactic registry under priority 10 ("FFI band") on import.

This is the production-grade native backend for the by lp tactic — what the meta-package leanprover/lp defaults to when no set_option lp.backend or per-call argument overrides it. Depend on this repo directly only when you want the SoPlex FFI specifically without the full leanprover/lp tactic surface (e.g. to register the backend in your own Lake project that wires the verifier and tactic differently).

This is the only package in the leanprover/lp family besides soplex-ffi itself that carries moreLinkArgs: the SoPlex C++ runtime link args propagate to anything that links this library.

Quickstart

require LPBackendSoplexFFI from git
  "https://github.com/leanprover/lp-backend-soplex-ffi" @ "main"

import LPBackendSoplexFFI  -- self-registers "soplex-ffi" at priority 10
import LPTactic            -- the `by lp` tactic

example (a b : Rat) (_ : 2 * a + b ≤ 5) (_ : a - b ≤ 1) :
    3 * a ≤ 6 := by lp

Build

System dependencies (same as leanprover/soplex-ffi):

Layout

LPBackendSoplexFFI.lean        # top-level import
LPBackendSoplexFFI/Adapter.lean
                               # def backend : LPBackend + initialize registerBackend
LPBackendSoplexFFI/Driver.lean # LP.solveVerified (synchronous verified-solve driver)
LPBackendSoplexFFITest/        # `lake test` smoke + driver-parity suite

The adapter lives under namespace LP.Backend.SoplexFFI, matching the namespace used before the split. Consumers writing LP.Backend.SoplexFFI.backend resolve to the same value regardless of which package owns it.

Licence

Apache License 2.0.