Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[CI] Coq release download broken? #1909

Closed
m-yac opened this issue Aug 15, 2023 · 5 comments
Closed

[CI] Coq release download broken? #1909

m-yac opened this issue Aug 15, 2023 · 5 comments
Labels
tooling: CI Issues involving CI/CD scripts or processes

Comments

@m-yac
Copy link
Contributor

m-yac commented Aug 15, 2023

Just noticed that it looks like the way we're installing Coq on CI for the heapster-tests is broken. The command opam repo add coq-released https://coq.inria.fr/opam/released seems to be consistently giving the error:

[ERROR] Could not update repository "coq-released": OpamDownload.Download_fail(_, "Curl failed: \"/usr/bin/curl --write-out %{http_code}\\\\n --retry 3 --retry-delay 2 --user-agent opam/2.1.5 -L -o /tmp/opam-3475-f7f9de/index.tar.gz.part -- [https://coq.inria.fr/opam/released/index.tar.gz\](https://coq.inria.fr/opam/released/index.tar.gz/)" exited with code 28")
[ERROR] Initial repository fetch failed
'opam repo add coq-released https://coq.inria.fr/opam/released' failed.
Error: Process completed with exit code 40.

For example, here's the failure from a scheduled CI run on master: https://github.com/GaloisInc/saw-script/actions/runs/5854373290/job/15871358448#step:7:23

@m-yac m-yac added the tooling: CI Issues involving CI/CD scripts or processes label Aug 15, 2023
@RyanGlScott
Copy link
Contributor

I suspect this is a server-side thing, as https://downforeveryoneorjustme.com/coq.inria.fr?proto=https suggests that https://coq.inria.fr is down (temporarily, I hope).

@m-yac
Copy link
Contributor Author

m-yac commented Aug 15, 2023

Ah, yes. Checked the Coq mailing list and it looks like the server is just down: https://sympa.inria.fr/sympa/arc/coq-club/2023-08/msg00013.html

Apparently there are some holidays in France at the moment, so this might not get fixed for a few days. From this discussion on Zulip, it seems like other folks are just deciding to live with their CI being messed up for a couple days: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Website.20down.3F

@RyanGlScott
Copy link
Contributor

If you need to temporarily disable the Heapster Coq tests to get the CI green, something like this should suffice:

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 57f7d3454..583bad0f7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -251,10 +251,11 @@ jobs:
   heapster-tests:
     needs: [build]
     strategy:
       fail-fast: false
       matrix:
+        continue-on-error: [true]
         os: [ubuntu-22.04, macos-12]
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v2
         with:

@eddywestbrook
Copy link
Contributor

Funny, I saw the email thread go by on the Coq list about the Coq server being down, and I thought to myself "I'm glad this doesn't affect me." Silly me.

@m-yac
Copy link
Contributor Author

m-yac commented Aug 16, 2023

@m-yac m-yac closed this as completed Aug 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
tooling: CI Issues involving CI/CD scripts or processes
Projects
None yet
Development

No branches or pull requests

3 participants