lake target path

Stream: lean4

[Chris Lovett]

Is there a way for a lakefile.lean test script to find the target path for the lean_exe defaultTarget?

[Mac]

Use let exe <- findLeanExe? <name> to get the lean_exe object and exe.file to get the path.

[Chris Lovett]

Calling this in lake script run install yeilds:

error: .\lakefile.lean:17:20: error: failed to synthesize instance
  MonadWorkspace IO

How do I fix that?

[Chris Lovett]

Never mind I figured it out by looking at Actions.lean def exe:

script install (args) do
  let ws ← Lake.getWorkspace
  if let some exe := ws.findLeanExe? `leanInk then
    println exe.file
  return 0