partial def Lean.forEachModuleInDir {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Name → m PUnit) (ext : optParam String "lean") : m PUnit

def Lean.realPathNormalized (p : Lake.FilePath) : IO Lake.FilePath

Equations

• Lean.realPathNormalized p = do let __do_lift ← IO.FS.realPath p pure (System.FilePath.normalize __do_lift)

def Lean.modToFilePath (base : Lake.FilePath) (mod : Lake.Name) (ext : String) : Lake.FilePath

Equations

• Lean.modToFilePath base mod ext = System.FilePath.addExtension (Lean.modToFilePath.go base mod) ext

def Lean.modToFilePath.go (base : Lake.FilePath) : Lake.Name → Lake.FilePath

Equations

• Lean.modToFilePath.go base (Lean.Name.str p h) = Lean.modToFilePath.go base p / { toString := h }
• Lean.modToFilePath.go base Lean.Name.anonymous = base
• Lean.modToFilePath.go base (Lean.Name.num pre i) = panicWithPosWithDecl "Lean.Util.Path" "Lean.modToFilePath.go" 38 20 "ill-formed import"

@[inline, reducible]

abbrev Lean.SearchPath : Type

A `.olean' search path.

Equations

• Lean.SearchPath = Lake.SearchPath

def Lean.SearchPath.findWithExt (sp : Lean.SearchPath) (ext : String) (mod : Lake.Name) : IO (Option Lake.FilePath)

If the package of mod can be found in sp, return the path with extension ext (lean or olean) corresponding to mod. Otherwise, return none. Does not check whether the returned path exists.

Equations

• One or more equations did not get rendered due to their size.

def Lean.SearchPath.findModuleWithExt (sp : Lean.SearchPath) (ext : String) (mod : Lake.Name) : IO (Option Lake.FilePath)

Like findWithExt, but ensures the returned path exists.

Equations

• One or more equations did not get rendered due to their size.

def Lean.SearchPath.findAllWithExt (sp : Lean.SearchPath) (ext : String) : IO (Array Lake.FilePath)

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.searchPathRef : IO.Ref Lean.SearchPath

@[export lean_get_prefix]

def Lean.getBuildDir : IO Lake.FilePath

Equations

• Lean.getBuildDir = do let __do_lift ← IO.appDir pure (Option.get! (System.FilePath.parent __do_lift))

@[export lean_get_libdir]

def Lean.getLibDir (leanSysroot : Lake.FilePath) : IO Lake.FilePath

Equations

• One or more equations did not get rendered due to their size.

def Lean.getBuiltinSearchPath (leanSysroot : Lake.FilePath) : IO Lean.SearchPath

Equations

• Lean.getBuiltinSearchPath leanSysroot = do let __do_lift ← Lean.getLibDir leanSysroot pure [__do_lift]

def Lean.addSearchPathFromEnv (sp : Lean.SearchPath) : IO Lean.SearchPath

Equations

• Lean.addSearchPathFromEnv sp = do let val ← liftM (IO.getEnv "LEAN_PATH") match val with | none => pure sp | some val => pure (System.SearchPath.parse val ++ sp)

def Lean.initSearchPath (leanSysroot : Lake.FilePath) (sp : optParam Lean.SearchPath ∅) : IO Unit

Initialize Lean's search path given Lean's system root and an initial search path. The system root can be obtained via getBuildDir (for internal use) or findSysroot (for external users).

Equations

• One or more equations did not get rendered due to their size.

def Lean.findOLean (mod : Lake.Name) : IO Lake.FilePath

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.findOLean.maybeThisOne (pkg : Lake.FilePath) (dir : Lake.FilePath) : IO (Option String)

@[export lean_module_name_of_file]

def Lean.moduleNameOfFileName (fname : Lake.FilePath) (rootDir : Option Lake.FilePath) : IO Lake.Name

Infer module name of source file name.

Equations

• One or more equations did not get rendered due to their size.

def Lean.searchModuleNameOfFileName (fname : Lake.FilePath) (rootDirs : Lean.SearchPath) : IO (Option Lake.Name)

Equations

• One or more equations did not get rendered due to their size.

def Lean.findSysroot (lean : optParam String "lean") : IO Lake.FilePath

Find the system root of the given lean command by calling lean --print-prefix and returning the path it prints. Defaults to trying the lean in PATH. If set, the LEAN_SYSROOT environment variable takes precedence. Note that the called lean binary might not be part of the system root, e.g. in the case of elan's proxy binary. Users internal to Lean should use Lean.getBuildDir instead.

Equations

• One or more equations did not get rendered due to their size.