Lake build file

Stream: lean4

[Marcus Rossel]

I'm trying to replace a test script I have with lake test. I created an executable test driver for this:

-- in lakefile.lean
@[test_driver]
lean_exe TestDriver where
  srcDir := ...

-- TestDriver.lean
def main (args : List String) : IO Unit := do
  ...

What I'm stuck on is: If I have a given System.FilePath for a .lean file, how can I build it? I was considering spawning a process and calling lake build, but then I might as well keep my script. I tried digging through Lake's source, but didn't find anything that looked like I would be able to call it.

[Kim Morrison]

I don't think this is possible, but you would need to ask Mac to be sure.

(It's still nice to have your test in lake test even if that test has to spawn lake processes!)