`lean-action` template for `lake new/init`

[austinletson]

`lean-action` template for `lake new/init`

[semorrison]

I propose that we actually just include this file regardless of which template the user has asked for. (Possibly with a switch to disable, but I'd very much like this on by default.)

[austinletson]

I propose that we actually just include this file regardless of which template the user has asked for. (Possibly with a switch to disable, but I'd very much like this on by default.)

This makes sense to me. Now that lean-action automatically decides which CI steps to run based on check-test and check-lint users should be able to benefit from the default setup without touching the workflow file, i.e., they add a test driver or lint driver to their lake file and lake test and lake lint automatically get run by lean-action in CI. We could mention the automatic behavior in the documentation for @[test_driver] and @[lint_driver].

If we always include the workflow file, the template / CLI option question above becomes irrelevant and I believe #4608 should be close to what we want. However if we do want to give users the option to disable the inclusion of the workflow file, the template / CLI option question still stands. The long option, something like --no-lean-action-workflow still seems reasonable to me, however I defer to Mac here.

[austinletson]

I created #4608 to get started on this. I am waiting for additional input before adding a way for the user to specify if the lake init/new should create the ci workflow.

[tydeu]

@austinletson Yep, #4608 seems exactly like what we want here! I left a code review with a few suggested tweaks over there. Also, mentioning the default workflow behavior in the documentation of test and lint drivers sounds like a good idea (though I think we can leave it for a follow-up PR).