Stream: Coq devs & plugin devs

Topic: coq.inria.fr website down?


view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 11:39):

Hi,
It seems the https://coq.inria.fr website is down currenty: in particular, doing opam update is now impossible and we get:

[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.0.5
        -L -o /tmp/opam-25581-9b8556/index.tar.gz.part https://coq.inria.fr/opam/released/index.tar.gz\"
        exited with code 35")

FWIW, error code 35 corresponds to:

CURLE_SSL_CONNECT_ERROR (35)

A problem occurred somewhere in the SSL/TLS handshake. You really want the error buffer and read the message there as it pinpoints the problem slightly more. Could be certificates (file formats, paths, permissions), passwords, and others.

Cc @Maxime Dénès FYI (I don't who I should Cc as well)

view this post on Zulip Karl Palmskog (Jul 26 2020 at 11:44):

@Erik Martin-Dorel it works fine for me now (both website and archive). From memory, the Coq opam archive is not even hosted on the same server as the Coq website. Can you try again and see if it was temporary?

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 12:48):

Thanks @Karl Palmskog for your feedback, I tried several different ways of accessing https://coq.inria.fr/opam/released and it seems the server is mostly OK indeed, but I still experience the issue in some cases: I believe the server may have a configuration issue w.r.t. IPv6.

To be more precise, here is an example session on a Debian 9 (oldstable) machine I've been using for these tests:

$ timeout -s SIGINT 10s ping coq.inria.fr
PING coq.inria.fr(2001:41d0:305:2100::8b43 (2001:41d0:305:2100::8b43)) 56 data bytes

--- coq.inria.fr ping statistics ---
10 packets transmitted, 0 received, 100% packet loss, time 9222ms

$ sudo docker run --rm -it debian

root@9d275163954e:/# timeout -s SIGINT 10s ping coq.inria.fr
PING coq.inria.fr (51.91.56.51) 56(84) bytes of data.
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=1 ttl=58 time=39.1 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=2 ttl=58 time=298 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=3 ttl=58 time=59.6 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=4 ttl=58 time=100 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=5 ttl=58 time=40.8 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=6 ttl=58 time=36.8 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=7 ttl=58 time=416 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=8 ttl=58 time=132 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=9 ttl=58 time=36.5 ms
64 bytes from 51.ip-51-91-56.eu (51.91.56.51): icmp_seq=10 ttl=58 time=42.3 ms

--- coq.inria.fr ping statistics ---
10 packets transmitted, 10 received, 0% packet loss, time 13ms
rtt min/avg/max/mdev = 36.528/120.106/415.658/124.943 ms
root@9d275163954e:/#

view this post on Zulip Maxime Dénès (Aug 31 2020 at 15:57):

I tried to fix the issue, waiting for confirmation that it is resolved


Last updated: Oct 16 2021 at 02:03 UTC