How to change current working directory in Lean 4?

Question

In Lean 4, we have IO.currentDir which returns the cwd. Is it possible to set the cwd though?

Answer 1

Short answer: No

Long answer: Yes, but probably not in a nice way that you would ever want to use in practice.

If you dig into the IO source, you will see IO.currentDir is defined as an opaque reference to the underlying lean_io_current_dir. If we look at lean_io_current_dir we see it just queries the C function getcwd. getcwd has no problem getting a new path as long as we can tell the OS to set it somehow. Doing this in Lean4 is the hard part since we need to somehow call chdir on ourselves, and to my knowledge the Lean developers have not given us a nice way to do this. However, something like this can be implemented in a hacky system dependent way. The following is an example of a hacky Linux solution based on gdb I've gotten to work. This solution is based off this post.

def chdir (newdir : System.FilePath) : IO UInt32 := do
  let PID <- IO.Process.getPID
  let cmd :=
    "gdb -q <<EOF\nattach " ++ toString PID ++
    "\ncall (int) chdir(\"" ++ newdir.toString ++
    "\")\ndetach\nquit\nEOF"
  let proc <- IO.Process.spawn {
    cmd := "bash"
    args := #["-c", cmd]
    stdout := IO.Process.Stdio.null
    stderr := IO.Process.Stdio.null
  }
  IO.Process.Child.wait proc

def main : IO Unit := do
  let cwd <- IO.currentDir
  IO.println cwd
  IO.FS.createDir "subdir"
  let _ <- chdir "subdir"
  --We are now in subdir
  let cwd <- IO.currentDir
  IO.println cwd
  let _ <- chdir ".."
  --We are now back in the starting directory
  let cwd <- IO.currentDir
  IO.println cwd
  IO.FS.removeDir "subdir"

The solution works by using gdb to attach to the main lean process via its PID and forcing it to run the chdir syscall.