runLinter in github workflow not terminating

Stream: general

[Joseph Tooby-Smith]

Since yesterday I've been having problems with the workflows in PhysLean. The workflow in question is controlled by this yml file.

The problem I am having is that the following step does not terminate:

      - name: runLinter on PhysLean
        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
        id: lint
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean

In PhysLean#777 it worked (i.e. terminated) on one commit and then stopped working after that. On another PR it did not work yesterday, worked once this morning, and then didn't again.

Caveat: I did update the linters on PhysLean, but this was as done in reaction to this problem, and is not the cause of it.

I am pretty confused with what is happening here. Has anyone experienced anything similar? I think it is likely a github workflow problem, but it seems odd it is always happening on the same part of the workflow. Alternatively it could be something to do with the recent bump to Lean.

(I am aware of lean-action, and know we should really be using that, there are just a lot of custom things we want for PhysLean currently).

[Joseph Tooby-Smith]

Simplifying the above step to the following:

- name: runLinter on PhysLean
        run: |
          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean

Still leads to non-terminating runs. Locally everything runs fine.

[Joseph Tooby-Smith]

I have been doing some testing with this and the short conclusion of my results is:

I can't seem to get lake exe runLinter PhysLean to work consistently in a github workflow, no matter what I try. It always fluctuates from working on one run to not terminating on others.

Thus, I took an extreme option and made a new version of the runLinter script that is stripped down to the bare necessities. This can be found at this PR PhysLean#786. This stripped down version appears to run correctly every time, it does not have this problem where it doesn't terminate as described above. (Although I'm still holding my breath).

Comparing my stripped down version, with the actual runLinter script, the main differences appear to be down to reading json files and resolving the modules to lint. This is the limit of my investigation thus far.

[Bryan Gin-ge Chen]

Just linking #general > CI stuck at Lint project step which seems to be another instance of the same problem.