Equations
- Lean.realPathNormalized p = do let a ← IO.FS.realPath p pure (System.FilePath.normalize a)
Equations
- Lean.modToFilePath base mod ext = (fun go => System.FilePath.withExtension (go mod) ext) (Lean.modToFilePath.go base)
Equations
- Lean.modToFilePath.go base (Lean.Name.str p h x_1) = Lean.modToFilePath.go base p / { toString := h }
- Lean.modToFilePath.go base Lean.Name.anonymous = base
- Lean.modToFilePath.go base (Lean.Name.num p x_1 x_2) = panicWithPosWithDecl "Lean.Util.Path" "Lean.modToFilePath.go" 25 22 "ill-formed import"
Equations
- Lean.SearchPath.findWithExt sp ext mod = let pkg := Lean.Name.toString (Lean.Name.getRoot mod); do let root? ← List.findM? (fun p => liftM (System.FilePath.isDir (p / { toString := pkg })) <||> liftM (System.FilePath.pathExists (System.FilePath.withExtension (p / { toString := pkg }) ext))) sp pure (Option.map (fun a => Lean.modToFilePath a mod ext) root?)
Equations
- Lean.SearchPath.findModuleWithExt sp ext mod = do let a ← Lean.SearchPath.findWithExt sp ext mod let _do_jp : PUnit → IO (Option System.FilePath) := fun y => pure none match a with | some path => do let a ← liftM (System.FilePath.pathExists path) if a = true then pure (some path) else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.SearchPath.findAllWithExt sp ext = let paths := #[]; do let r ← forIn sp paths fun p r => let paths := r; do let a ← liftM (System.FilePath.isDir p) if a = true then do let a ← System.FilePath.walkDir p fun x => pure true let paths : Array System.FilePath := paths ++ Array.filter (fun a => System.FilePath.extension a == some ext) a 0 (Array.size a) pure PUnit.unit pure (ForInStep.yield paths) else do pure PUnit.unit pure (ForInStep.yield paths) let x : Array System.FilePath := r let paths : Array System.FilePath := x pure paths
Equations
- Lean.getBuildDir = do let a ← IO.appDir pure (Option.get! (System.FilePath.parent a))
Equations
- Lean.getLibDir leanSysroot = let buildDir := leanSysroot; let _do_jp := fun buildDir y => pure (buildDir / "lib" / "lean"); if Lean.isStage0 () = true then let buildDir := buildDir / { toString := ".." } / { toString := "stage1" }; do let y ← pure PUnit.unit _do_jp buildDir y else do let y ← pure PUnit.unit _do_jp buildDir y
Equations
- Lean.getBuiltinSearchPath leanSysroot = do let a ← Lean.getLibDir leanSysroot pure [a]
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)
Equations
- Lean.initSearchPath leanSysroot sp = do let a ← Lean.getBuiltinSearchPath leanSysroot let a ← Lean.addSearchPathFromEnv a let sp : optParam Lean.SearchPath ∅ := sp ++ a ST.Ref.set Lean.searchPathRef sp
Equations
- Lean.findOLean mod = do let sp ← ST.Ref.get Lean.searchPathRef let a ← Lean.SearchPath.findWithExt sp "olean" mod match a with | some fname => pure fname | x => let pkg := { toString := Lean.Name.toString (Lean.Name.getRoot mod) }; let msg := toString "unknown package '" ++ toString pkg ++ toString "'"; (fun maybeThisOne => do let a ← IO.currentDir let a ← maybeThisOne a let _do_jp : String → PUnit → IO System.FilePath := fun msg y => throw (IO.userError msg) match a with | some msg' => let msg := msg ++ msg'; do let y ← pure PUnit.unit _do_jp msg y | x => do let y ← pure PUnit.unit _do_jp msg y) (Lean.findOLean.maybeThisOne pkg)
Equations
- Lean.moduleNameOfFileName fname rootDir = do let fname ← IO.FS.realPath fname let _do_jp : System.FilePath → IO Lean.Name := fun rootDir => do let rootDir ← Lean.realPathNormalized rootDir let _do_jp : System.FilePath → PUnit → IO Lean.Name := fun rootDir y => let _do_jp := fun y => let fnameSuffix := String.drop fname.toString (String.length rootDir.toString); let modNameStr := System.FilePath.withExtension { toString := fnameSuffix } ""; let modName := List.foldl Lean.Name.mkStr Lean.Name.anonymous (System.FilePath.components modNameStr); pure modName; if (!String.isPrefixOf rootDir.toString (System.FilePath.normalize fname).toString) = true then do let y ← throw (IO.userError (toString "input file '" ++ toString fname ++ toString "' must be contained in root directory (" ++ toString rootDir ++ toString ")")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if (!String.endsWith rootDir.toString (Char.toString System.FilePath.pathSeparator)) = true then let rootDir := { toString := rootDir.toString ++ Char.toString System.FilePath.pathSeparator }; do let y ← pure PUnit.unit _do_jp rootDir y else do let y ← pure PUnit.unit _do_jp rootDir y match rootDir with | some rootDir => do let y ← pure rootDir _do_jp y | none => do let y ← IO.currentDir _do_jp y
Equations
- Lean.searchModuleNameOfFileName fname rootDirs = do let r ← forIn rootDirs { fst := none, snd := PUnit.unit } fun rootDir r => let r := r.snd; do let r ← tryCatch (do let a ← Lean.moduleNameOfFileName fname (some rootDir) pure (DoResultPR.return (some a) PUnit.unit)) fun ex => let e := ex; do let y ← pure () pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; do pure a pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | DoResultPR.return b u => let x := u; pure (ForInStep.done { fst := some b, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → IO (Option Lean.Name) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a
Equations
- Lean.findSysroot? lean = do let a ← liftM (IO.getEnv "LEAN_SYSROOT") let _do_jp : PUnit → IO System.FilePath := fun y => do let out ← IO.Process.run { toStdioConfig := { stdin := IO.Process.Stdio.inherit, stdout := IO.Process.Stdio.inherit, stderr := IO.Process.Stdio.inherit }, cmd := lean, args := #["--print-prefix"], cwd := none, env := #[] } pure { toString := String.trim out } match a with | some root => pure { toString := root } | x => do let y ← pure PUnit.unit _do_jp y