lean_action_ci.yml

Stream: new members

[mars0i]

I hadn't used lake new or lake init in a while; today I made a new to explore some ideas. It appears that lake v. 5.0.0-6d22e0e automatically puts a CI config file in .github/workflows, causing github to send me a series of emails about failed CI runs. I contributed to repos that use CI, and it's a good thing for those repos, but I've never set it up myself and know very little about it. I certainly don't want it for this new repo at this time.

The last time I used lake new or lake init perhaps it was different version? Or github has changed its default operation, but the last Lean repo I created before today doesn't have a .github directory. (I know that github has been telling me about upcoming changes that I didn't understand and didn't care about, as far as I could tell. Maybe this is one of them.)

I deleted lean_action_ci.yml from .github/workflows and committed the change. Is that the right thing to do? Could that create trouble? Are there other changes I should make? Is there an option I should pass to lake to tell it not to set up CI?

[Yicheng Tao]

I think you can just keep that file and disable the workflow on GitHub.

To my knowledge, I think that workflow only build the project when push or pull request. If you are contributing to a public project, this would be helpful to let others know your code can compile.

[Yicheng Tao]

You may find more information in https://github.com/leanprover/lean-action.

[mars0i]

Thanks @Yicheng Tao. I didn't know anything about workflows or lean-action. Those pointers are extremely helpful. I found the github docs page for disabling workflows, but oddly, there are no workflows listed in my repo. :shrug: Anyway, I can figure out now what I want to do. (This is for a private, exploratory project, and there's no good reason for me to use CI.)

[mars0i]

Ah, the reason there were no workflows was that I'd deleted the lake init-provided .yml file. Makes sense. Disabled it.