Documentation

Lean.Util.Path

source
partial def Lean.forEachModuleInDir {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] (dir : System.FilePath) (f : Name → m PUnit) :
m PUnit

Executes f with the corresponding module name for each .lean file contained in dir.

For example, if dir contains A/B/C.lean, f is called with A.B.C.

source
def Lean.realPathNormalized (p : System.FilePath) :
IO System.FilePath
Equations
source
def Lean.modToFilePath (base : System.FilePath) (mod : Name) (ext : String) :
System.FilePath
Equations
source
def Lean.modToFilePath.go (base : System.FilePath) :
Name → System.FilePath
Equations
source
@[reducible, inline]
abbrev Lean.SearchPath :
Type

A `.olean' search path.

Equations
source
def Lean.SearchPath.findWithExt (sp : SearchPath) (ext : String) (mod : Name) :
IO (Option System.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.
source
def Lean.SearchPath.findModuleWithExt (sp : SearchPath) (ext : String) (mod : Name) :
IO (Option System.FilePath)

Like findWithExt, but ensures the returned path exists.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.SearchPath.findAllWithExt (sp : SearchPath) (ext : String) :
IO (Array System.FilePath)
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.searchPathRef :
IO.Ref SearchPath
source
@[export lean_get_prefix]
def Lean.getBuildDir :
IO System.FilePath
Equations
source
@[export lean_get_libdir]
def Lean.getLibDir (leanSysroot : System.FilePath) :
IO System.FilePath
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.getBuiltinSearchPath (leanSysroot : System.FilePath) :
IO SearchPath
Equations
source
def Lean.addSearchPathFromEnv (sp : SearchPath) :
IO SearchPath
Equations
source
def Lean.initSearchPath (leanSysroot : System.FilePath) (sp : 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.
source
def Lean.findOLean (mod : Name) :
IO System.FilePath

Find the compiled .olean of a module in the LEAN_PATH search path.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.findLean (sp : SearchPath) (mod : Name) :
IO System.FilePath

Find the .lean source of a module in a LEAN_SRC_PATH search path.

Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_module_name_of_file]
def Lean.moduleNameOfFileName (fname : System.FilePath) (rootDir : Option System.FilePath) :
IO Name

Infer module name of source file name.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.searchModuleNameOfFileName (fname : System.FilePath) (rootDirs : SearchPath) :
IO (Option Name)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.findSysroot (lean : String := "lean") :
IO System.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.