Lake: allow buildO to take arguments before the injected ones

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The current buildO function of Lake DSL takes the compiler as argument, and then injects it's own args before other ones. This causes an issue when using zig to compile i.e. zig cc or zig cpp.

Context

I'm trying to call some C code from Lean, similar to this. Instead of using cc or c++ to compile the code, I'm trying to use zig's compiler, as it provides a lot of benefits. Unfortunately, to compile C with zig it's done through an argument to zig i.e. zig cc.

I think this use case should be covered, and buildO should allow for it, either by an explicit argument, or by programatically splitting the compiler argument and passing the arguments before its own.

Steps to Reproduce

Internally, buildO calls IO.Process.output using zig cc as cmd which produces an error.

file.lean

import Lake
def main : IO Unit := do
  let res ← IO.Process.output { cmd := "zig", args := #["cc --help"] }
  -- let res ← IO.Process.output { cmd := "zig cc", args := #["--help"] } -- Error
  IO.println res.exitCode

Run with lean --run file.lean.

Expected behavior: zig cc should be a valid compiler to buildO

Actual behavior: zig cc is not a valid compiler to buildO

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by locating the Lake DSL implementation of buildO and inspect how it constructs the IO.Process command and argument list. Reproduce the issue with the file.lean example and zig cc; the change is complete when a compiler command requiring a subcommand can be passed to buildO successfully.