Why is github-ci creating releases

Stream: general

[Shreyas Srinivas]

Hi,
I just setup a new repo and the CI reported failure because it could not create a new release. Why is the CI trying to do this in the first place?

[Shreyas Srinivas]

This is not a feature that I believe we want in most project repos or workshop demo repos. I claim that we just need the CI green check to show the project builds.

[Yury G. Kudryashov]

What command did you use to create the repo? What's in .github/workflows/*?

[Shreyas Srinivas]

lake new <project name> math. There was a create-release.yml in the workflows. I just pushed a commit to delete it

[Yury G. Kudryashov]

Here is the contents of the autogenerated file:

name: Create Release

on:
  push:
    branches:
      - 'main'
      - 'master'
    paths:
      - 'lean-toolchain'

jobs:
  lean-release-tag:
    name: Add Lean release tag
    runs-on: ubuntu-latest
    permissions:
      contents: write
    steps:
    - name: lean-release-tag action
      uses: leanprover-community/lean-release-tag@v1
      with:
        do-release: true
        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

It looks like the intent is to create a new release whenever you update your lean-toolchain.

[Shreyas Srinivas]

It also runs when a new toolchain project is created

[Shreyas Srinivas]

In any case it also fails without some permissions on github, for which no instructions are provided in the auto-generated README.md.

[Kim Morrison]

Could you point to a failure example? Or suggest instructions to add?

[Shreyas Srinivas]

in DM

[Kim Morrison :bot:]

https://github.com/leanprover-community/lean-release-tag/pull/2