Split StrataMain.lean into importable library and thin executable root

[MikaelMayer]

Fixes #1163

Summary

Splits StrataMain.lean into an importable library (StrataMainLib.lean) and a thin executable root, enabling downstream packages to reuse and customize the CLI command definitions without copying code.

Changes

• StrataMainLib.lean (new lean_lib): Contains all command definitions, helpers, commandGroups, commandList, commandMap, and a shared runCommandMap dispatcher.
• StrataMain.lean: Now a 3-line executable root that imports StrataMainLib and calls runCommandMap.
• lakefile.toml: Adds StrataMainLib as a lean_lib and to defaultTargets.
• verifyCommand and pyAnalyzeLaurelCommand are parameterized with mkDischarge (defaulting to Core.mkDischargeFn), allowing downstream executables to plug in a custom solver backend.

This is a pure refactor — no behavioral changes.

Downstream usage

import StrataMainLib
import MySolver

def myCommandMap : Std.HashMap String Command :=
  commandMap
    |>.insert "verify" (verifyCommand (mkDischarge := myDischargeFn))
    |>.insert "pyAnalyzeLaurel" (pyAnalyzeLaurelCommand (mkDischarge := myDischargeFn))

def main (args : List String) : IO Unit :=
  runCommandMap myCommandMap commandGroups args

No code duplication, stays in sync automatically.

Testing

All existing tests pass unchanged.

[MikaelMayer]

Note: I changed the upstream because the original issue specifically mentioned functions that were not in main yet so you can't just solve this by updating main.

[MikaelMayer]

🔍 Clean refactoring. The split is well-structured: a thin executable root importing a reusable library, with moreFns parameterized for downstream customization.

One behavioral change to confirm: pyAnalyzeLaurelCommand now receives moreFns (which is Strata.Python.ReFactory in the default executable), whereas on main it called Strata.verifyCore with the default Lambda.Factory.default. If this is intentional (making the Laurel pipeline consistent with the direct Python pipeline), it's a good improvement — but it should be called out in the PR description since it's not a pure refactor.

[MikaelMayer]

🔍 Behavioral change: on main, verifyCore was called here without moreFns (using the default Lambda.Factory.default). Now it receives the parameterized moreFns, which in the default executable is Strata.Python.ReFactory. This means the Laurel verification pipeline now uses the Python solver factory instead of the default. Is this intentional? If so, please mention it in the PR description — it's not a pure refactor.

[MikaelMayer]

🤖 No code change needed. After the merge with the base branch (issue-1045-feature-request-parallel-solving), the pyAnalyzeLaurelCommand no longer takes a parameterized moreFns — it hardcodes Strata.Python.ReFactory directly, which matches what the base branch already does. The original concern about the parameterization introducing a behavioral change is moot since the merge resolved it: the code now simply moves the same Core.verifyProgram coreProgram options (moreFns := Strata.Python.ReFactory) call from StrataMain.lean into StrataMainLib.lean without any semantic difference relative to the base branch.

[MikaelMayer]

🤖 Acknowledged — the base branch is issue-1045-feature-request-parallel-solving because the functions referenced in issue #1163 (like Core.verifyProgram, pyAnalyzeLaurelCommand with the new flags, etc.) only exist on that branch. The PR diff is relative to that upstream.

[MikaelMayer]

The split looks great — thanks for the quick turnaround.

One follow-up request: could you also parameterize verifyCommand and pyAnalyzeLaurelCommand with mkDischarge? This is the last piece needed for a downstream exe to plug in a custom solver backend without copying any command code.

The change is 4 lines:

-def pyAnalyzeLaurelCommand : Command where
+def pyAnalyzeLaurelCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where

and inside its callback, at the Core.verifyProgram call (line ~750):

                 (keepAllFilesPrefix := keepPrefix)
+                (mkDischarge := mkDischarge)
                 |>.toBaseIO with

-def verifyCommand : Command where
+def verifyCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where

and inside its callback (line ~1340):

-          verify pgm inputCtx proceduresToVerify opts
+          verify pgm inputCtx proceduresToVerify opts (mkDischarge := mkDischarge)

With this, a downstream exe becomes:

import StrataMainLib
import MySolver

def myCommandMap : Std.HashMap String Command :=
  commandMap
    |>.insert "verify" (verifyCommand (mkDischarge := myDischargeFn))
    |>.insert "pyAnalyzeLaurel" (pyAnalyzeLaurelCommand (mkDischarge := myDischargeFn))

def main (args : List String) : IO Unit :=
  runCommandMap myCommandMap commandGroups args

No code duplication, stays in sync automatically.

[MikaelMayer]

🤖 Done in 4586b49 — both verifyCommand and pyAnalyzeLaurelCommand now accept an optional mkDischarge parameter (defaulting to Core.mkDischargeFn), threaded through to the underlying verify/Core.verifyProgram calls.