file could not be opened successfully

Stream: general

[Yaël Dillies]

I get a weird error trying to run leanproject on my LeanCamCombi project. It downloads cache, then errors with a cryptic https://github.com/YaelDillies/LeanCamCombi/actions/runs/3549861160/jobs/5962691270: https://github.com/YaelDillies/LeanCamCombi/actions/runs/3549861160/jobs/5962691270

Any idea?

[Alex J. Best]

No idea about this specific error, but when I had lean woes in CI recently I added

      - name: Setup tmate session
        uses: mxschmitt/action-tmate@v3

to the workflow, this stops the workflow at that point in time, opens a public ssh connection so you can drop right into the github runner and snoop around, try and run the next commands yourself and investigate

[Kevin Buzzard]

using leanproject to get the repo onto a local PC works fine for me BTW

[Yaël Dillies]

Yeah, I very much suspect I botched something, but I can't tell why and the error is being unhelpful.