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

[austinletson]

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 to lean-action with no inputs should be a reasonable default:

name: CI

on:
  push:
    branches: ["main"]
  pull_request:
    branches: ["main"]
  workflow_dispatch:

jobs:
  build:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v4
      # uses lean action with all default input values
      - uses: leanprover/lean-action@v1-beta

Here are a few questions regarding implementation and user experience we need to align on:

• How will the template interact with the existing templates and lake options? Currently, users must choose one main template (std, exe, lib, math) and one file format (.lean, .toml) for the lakefile. Does adding a long option (e.g. lake new --lean-action-workflow) instead of a template make sense? @tydeu I thought you might be the best person to answer this.
• How should the workflow triggers be configured by default? I was thinking pushes and pull requests to the main branch. Alternatively, we could keep it simple and trigger on a push it to any branch.

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.

[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.

[kim-em]

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.

[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).