bug: run `lake update` and `lean-action` gets an error

[leanprover]

bug: run `lake update` and `lean-action` gets an error

[austinletson]

This could definitely be an issue with lean-action.

Note, currently the functional tests for lean-action use Lean 4.8.0, so it is possible for issues with new releases to slip through. However, we definitely want to support the latest release candidates of Lean as much as possible. I created #63 to allow for testing on any version of Lean.

Have you tried running this workflow with the lean-action@v1-beta instead of lean-action@main?

[austinletson]

If the issue is the GitHub cache of the .lake directory, we could try using the use-github-cache: false input of lean-action. This input hasn't been included in a release yet, but it is available in the main branch.

[digama0]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ltar.20error.20aften.20lean.234402/near/444803915 . This is a "one time issue" regarding upgrading from 4.8.0-* to 4.9.0-* series, and the fix is to manually delete the .lake directory.

[Seasawher]

@austinletson

It's caused by GitHub cache! The following workflow did work. (see: https://github.com/lean-ja/lean-by-example/actions/runs/9556334719/workflow)

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
        shell: bash

      - name: Update dependencies of ${{ github.repository }}
        run: lake update
        shell: bash

      - name: build lean
        uses: leanprover/lean-action@main
        with:
          test: false
          use-github-cache: false

I think this issue is also temporary. Let us ignore this issue until it occurs again.

[Seasawher]

Yes. I think this issue is resolved.

[Seasawher]

this workflow doesn't raise an error: https://github.com/lean-ja/lean-by-example/actions/runs/9530454158/workflow

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
        shell: bash

      - name: Update dependencies of ${{ github.repository }}
        run: lake update
        shell: bash

      - name: cache
        run: lake exe cache get

      - name: build
        run: lake build --quiet

so this is maybe caused by a bug of lean-action.

[Seasawher]

v1-beta also raise an error.

workflow file: https://github.com/lean-ja/lean-by-example/actions/runs/9535628209/workflow
error detail: https://github.com/lean-ja/lean-by-example/actions/runs/9535628209/job/26281586503

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
        shell: bash

      - name: Update dependencies of ${{ github.repository }}
        run: lake update
        shell: bash

      - name: build lean
        uses: leanprover/lean-action@v1-beta
        with:
          test: false

error message is the same.

▼ Run echo "::group::Mathlib Cache"
  echo "::group::Mathlib Cache"
  lake exe cache get
  echo "::endgroup::"
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
▼ Mathlib Cache
  info: mdgen: updating repository '././.lake/packages/mdgen' to revision '6a6a412465e82572f6e30385592eac52ab055c83'
  info: mathlib: updating repository '././.lake/packages/mathlib' to revision '895010aa7d965a703e0061d0acc992066[44](https://github.com/lean-ja/lean-by-example/actions/runs/9535628209/job/26281586503#step:5:50)11a70'
  error: external command 'git' exited with code 1
  Error: Process completed with exit code 1.

[Seasawher]

I wonder getting cache causes this error.

[Seasawher]

I have found that this error probably occurs in the following situation: (There is as yet no solid evidence to support this conclusion.)

1. mathlib relies on an out-of-date Lean such as v4.8.0
2. there is still a .lake cache
3. trying to bring the Lean version up to date

This error also occurs locally. The local solution is to delete the .lake directory.
"If lean-toolchain has been updated, not using cache" might be a solution.

It is strange that .lake has to be deleted manually in the first place. This may be a bug in lake.

[Seasawher]

@digama0 Thank you!

[Seasawher]

Is this really a "one time issue"? I have got an error in https://github.com/Seasawher/mathlib4-tactics when update Mathlib from v4.9.0-rc2 to v4.9.0-rc2. (see: log ) Doesn't the fact that the error occurs even when the Lean version is up-to-date imply that this is not a temporary problem?

（It is not lean-action but lean-update that is used in mathlib4-tactics, but I have confirmed that it is the github-cache of lean-action that is the cause...!）

[Seasawher]

Cache modification #64 (comment) would solve this issue?

[Seasawher]

This problem also occurred when updating from v4.9.0-rc2 to v4.9.0-rc3.

[austinletson]

I created #70 to implement the change to the caching keys to try and address this issue.

@Seasawher does using use-github-cache: false still work as a temporary fix? I know this is not ideal. I am asking to make sure I still understand the problem.

[Seasawher]

does using use-github-cache: false still work as a temporary fix?

Yes. if I don't use cache, I don't see same error. This issue is caused by remaining .lake directory. On local, the way to fix this issue is removing .lake directory.

[Seasawher]

by the way, this lake's error message is not easy to understand

error: external command 'git' exited with code 1

actually the reason of issue is .lake, not git.

[austinletson]

I think with the improvements to the caching keys in #71 we shouldn't run into this again. @Seasawher do you agree?

[austinletson]

Sounds good. Thank you for raising this!