Communicating Lean search paths between processes

structure Lean.LeanPaths : Type

• oleanPath : Lean.SearchPath
• srcPath : Lean.SearchPath
• loadDynlibPaths : Array Lake.FilePath

instance Lean.instToJsonLeanPaths : Lean.ToJson Lean.LeanPaths

instance Lean.instFromJsonLeanPaths : Lean.FromJson Lean.LeanPaths

def Lean.initSrcSearchPath (_leanSysroot : Lake.FilePath) (sp : optParam Lean.SearchPath ∅) : IO Lean.SearchPath