Closed austinletson closed 2 months ago
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.
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.)
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 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).
Proposal
Add a template to
lake new/init
to allow users to automatically include a default continuous integration workflow that uses lean-action.With the
auto-config
improvement introduced by leanprover/lean-action#61, a call tolean-action
with no inputs should be a reasonable default:Here are a few questions regarding implementation and user experience we need to align on:
lake new --lean-action-workflow
) instead of a template make sense? @tydeu I thought you might be the best person to answer this.Community Feedback
link to relevant Zulip discussion
Related to #3950
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.