getPackageDir

Mathlib.Tactic.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.getPackageDir

Lean4

/-- Returns the root directory which contains the package root file, e.g. `Mathlib.lean`. -/
def getPackageDir (pkg : String) : IO System.FilePath := do
  let sp ← getSrcSearchPath
  let root? ← sp.findM? fun p => (p / pkg).isDir <||> ((p / pkg).withExtension "lean").pathExists
  if let some root := root? then
    return root
  throw <|
      IO.userError
        s! "Could not find {pkg} directory. \
              Make sure the LEAN_SRC_PATH environment variable is set correctly."

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru