feat: add build-args input

[austinletson]

Pass a new build-args input to lake build in the build step.

closes #15

[austinletson]

I have tested this on a test repo. Here is the usage on the input and here is the corresponding build where lean-action ran lake build --quiet.

[oliver-butterley]

I should explain that I am not an expert at all, here's just a comment that came to mind in case it might be useful.

There is a recommended way to avoid script injection in actions: https://docs.github.com/en/actions/security-guides/security-hardening-for-github-actions#good-practices-for-mitigating-script-injection-attacks

Probably this isn't a problem with the current code because it only takes an input that should be trusted in the repo which uses the action. Also I don't think the mathlib world is much a target. The main concern is that github sometimes automatically flags actions as security risks if it finds something which might worry users.

Anyway, I'm not so knowledgeable about this so might be talking nonsense!

[austinletson]

I should explain that I am not an expert at all, here's just a comment that came to mind in case it might be useful.

There is a recommended way to avoid script injection in actions: https://docs.github.com/en/actions/security-guides/security-hardening-for-github-actions#good-practices-for-mitigating-script-injection-attacks

Probably this isn't a problem with the current code because it only takes an input that should be trusted in the repo which uses the action. Also I don't think the mathlib world is much a target. The main concern is that github sometimes automatically flags actions as security risks if it finds something which might worry users.

Anyway, I'm not so knowledgeable about this so might be talking nonsense!

I think this is spot on. Thanks for the the suggestion.