Changing `lean-action` to fail on lake warnings by default

Stream: general

[Austin Letson]

Kim Morrison said:

Actually, maybe this is really a question for Austin Letson --- could we change the default for lean-action to fail if there are warning during the build?

I moved this from the "Updating to 4.15.0" thread to avoid introducing extra noise.

While this is definitely an option, it seems to me there are some downsides to making lean-action fail on warnings. The fact that lean-action is a thin wrapper around lake build and inherits the default configuration of lake build comes with some advantages:

• it is easier to replicate CI locally
• changes to Lake flow down to lean-action more seamlessly

Furthermore, this change would have a backward compatibility impact in settings where warnings are acceptable.

Alternatively, could we change the default configuration of lean-action included with a lake new to include uses: build-args: "--wfail" instead of changing the default behavior for lean-action?

[Asei Inoue]

I think so too. Instead of changing the default behavior of lean action, the behavior of lake new should be modified.

I think default arguments should be "--log-level=warning --fail-level=warning". The reason is that there are few cases where you would want to check info-level logs in CI.