如何在Lean 4中更改当前工作目录？能否设置cwd？

• 当然可以设置当前工作目录，Lean 4 提供了IO.setCurrentDir函数专门用于修改当前工作目录（cwd）。
• 该函数接收一个FilePath类型的参数，传入你想要切换到的目标目录路径即可，调用成功后，后续所有IO操作都会基于新的工作目录执行。
• 简单示例代码：

import System.FilePath

def main : IO Unit := do
  -- 替换为你要切换的目标目录路径
  let targetDir := FilePath.mk "/home/user/my-project"
  IO.setCurrentDir targetDir
  -- 验证切换结果
  let updatedCwd ← IO.currentDir
  IO.println s!"已切换至工作目录：{updatedCwd}"

• 需要注意：如果指定的目录不存在、路径无效或者程序没有访问权限，IO.setCurrentDir会抛出IO异常，你可以通过try ... catch结构捕获并处理这类错误。

内容的提问来源于stack exchange，提问作者Tony Beta Lambda