Stream: Coq devs & plugin devs

Topic: Website down?


view this post on Zulip Ralf Jung (Nov 12 2020 at 17:28):

https://coq.inria.fr/refman/addendum/type-classes.html times out here right now (trying from a German DSL connection)

view this post on Zulip Ralf Jung (Nov 12 2020 at 17:29):

tried a few machines via SSH and curl, same result

view this post on Zulip Ralf Jung (Nov 12 2020 at 17:30):

ping coq.inria.fr fails both via IPv4 and IPv6

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 17:31):

Same here (also Germany)

view this post on Zulip Karl Palmskog (Nov 12 2020 at 17:33):

same, Sweden

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 17:34):

Same here (France)...

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 17:40):

Damn! Who at Inria do we need to contact?

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 17:41):

BTW, as a workaround: you can access the manual at https://coq.github.io/doc/V8.12.0/refman/

view this post on Zulip Karl Palmskog (Nov 12 2020 at 17:42):

I hope it's not another spam submission like the time the website was down for days...

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 17:42):

[FWIW, I can still connect to the server.]

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 17:42):

Karl Palmskog said:

I hope it's not another spam submission like the time the website was down for days...

That cannot happen anymore since now the website is fully static.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 17:42):

(At that time, the Inria IT staff had overreacted to something posted in our bug tracker.)

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 18:24):

not just the manual, but I hear opam’s also down

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 18:34):

opam update fails on coq-released

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 18:49):

(The actual data is on https://github.com/coq/opam-coq-archive/tree/master/released, so probably one can adapt the repo URL)

view this post on Zulip Karl Palmskog (Nov 12 2020 at 19:11):

from my understanding, the opam repo is anyway hosted separely from the Coq web server. @Maxime Dénès could perhaps comment on whether there is some alternative URL or hosting options as long as coq.inria.fr is down

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 19:50):

No, the two are on the same server.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 19:53):

Actually, I was wrong when I said the server was up. I had forgotten that we had moved to a server hosted outside Inria.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 19:53):

I tested the old Inria server.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 19:53):

But the new (OVH) server is actually unresponsive when trying to log in SSH.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 19:54):

So we need to contact OVH and I think our only point of contact is @Maxime Dénès.

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 21:33):

for opam workarounds I created https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Subdirectories.20of.20git.20repos.20as.20opam.20repos, we have two ways.

view this post on Zulip Maxime Dénès (Nov 13 2020 at 08:24):

Hi guys! Sorry I just noticed this. I'll investigate now. Will report here.

view this post on Zulip Maxime Dénès (Nov 13 2020 at 09:07):

It should be back in a few minutes.

view this post on Zulip Maxime Dénès (Nov 13 2020 at 09:13):

It's back! Apologies for the inconvenience.

view this post on Zulip Maxime Dénès (Nov 13 2020 at 09:14):

Our payment process for OVH is fragile, we hope to improve that soon but so far no solution was suggested to us. We'll debrief this internally, to avoid having this problem again.


Last updated: Oct 16 2021 at 01:03 UTC