Following #293, we would like a workflow that automates running lake update. What I would like ideally is:
- at some cron interval (day, week?) the bot runs
lake update and opens a PR
- if CI is a success, the bot places it on the merge queue
- on failure, the PR remains open so a maintainer can fix
This will need to be a little different from the Mathlib equivalent, as the bot will need to actually merge the PR versus leaving a bors comment.
Following #293, we would like a workflow that automates running
lake update. What I would like ideally is:lake updateand opens a PRThis will need to be a little different from the Mathlib equivalent, as the bot will need to actually merge the PR versus leaving a bors comment.