Zulip Chat Archive

Stream: general

Topic: file could not be opened successfully

Yaël Dillies (Dec 13 2022 at 11:38):

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 (Dec 13 2022 at 11:55):

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 (Dec 13 2022 at 12:10):

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

Yaël Dillies (Dec 13 2022 at 12:12):

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

Last updated: Dec 20 2023 at 11:08 UTC