Add input to support passing parameters to `lake build`

[austinletson]

Add input to support passing parameters to `lake build`

[Kha]

It might be simpler to just support any arguments, such as --wfail

[oliver-butterley]

Within the action lake is run on different occasions:

• lake exe cache get
• lake build
• lake test
• lake exe runLinter
  Do I understand correctly that there will be cases where each of these require different arguments? Consequently it would be fine to support passing any arguments but the action needs 4 different inputs to correspond to each of the different occasions when lake runs?

[austinletson]

It might be simpler to just support any arguments, such as --wfail

👍 I agree this is much simpler and more flexible. I think a build-options input which allows for lake build {build-options} should do the trick.

Do I understand correctly that there will be cases where each of these require different arguments? Consequently it would be fine to support passing any arguments but the action needs 4 different inputs to correspond to each of the different occasions when lake runs?

Hmm, this is a good point. It seems feasible that users would arguments, such as --wfail, in any of these instances.

Another potential use case would be if a user wants to run all lake commands with certain arguments such as --wfail.

Do others know of existing projects which pass parameters to the other lake commands in their CI? For instance does lake exe cache get ever get called with args? For the sake of simplicity, we might should limit the input interface to support args for the commands which have known use cases and expand as needed.

[oliver-butterley]

🤔 Small survey of uses:

• lake -R -Kenv=dev build is used in many projects for building the project docs. E.g., FLT
• lake build -Kwerror used in batteries
• lake -Kenv=dev exe cache get is used in LeanAPAP

[austinletson]

I created #27 which adds this functionality specifically for lake build so we can support the use case in `batteries.