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.

view this post on Zulip Karl Palmskog (Aug 11 2023 at 18:14):

the website is down for me again: https://coq.inria.fr https://coq.inria.fr/distrib etc.

Is this some Inria maintenance thing again?

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:14):

Not maintenance, still payment unfortunately...

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:15):

I reported the issue two hours ago, but it will probably take a miracle to be fixed before Wednesday (Monday & Tuesday are holidays).

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:16):

Last time, I was told again that the process would be improved, but I guess it hasn't happened.

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:17):

Incidentally, it blocked the second beta release of VsCoq 2 which was one click away.

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:19):

I'll try again (and harder) to have the process improved in September.

view this post on Zulip Karl Palmskog (Aug 11 2023 at 18:19):

oh damn, so Coq opam is down as well? ping @Michael Soegtrop this will affect the Platform

view this post on Zulip Maxime Dénès (Aug 11 2023 at 18:19):

Unfortunately, yes.

view this post on Zulip Karl Palmskog (Aug 11 2023 at 18:20):

conceivably, large parts of our automation infrastructure will be very affected (but not Coq dev, I guess)

view this post on Zulip Karl Palmskog (Aug 11 2023 at 18:24):

ping also @Erik Martin-Dorel this will likely break all dev Docker images (until Wednesday)

view this post on Zulip Erik Martin-Dorel (Aug 11 2023 at 18:35):

Ah OK; thanks @Karl Palmskog for letting me know

view this post on Zulip Michael Soegtrop (Aug 12 2023 at 12:53):

@Karl Palmskog : yes, all my CI failed, but I can live with that for a day or two.

view this post on Zulip Jason Gross (Aug 12 2023 at 19:24):

opam update is hanging on downloading https://coq.inria.fr/opam/core-dev/index.tar.gz, I guess this is related?

view this post on Zulip Karl Palmskog (Aug 12 2023 at 19:41):

yes, no Coq opam repos will work until the website is up again (they are hosted in the same virtual server)

view this post on Zulip Paolo Giarrusso (Aug 12 2023 at 20:39):

FWIW one can clone the opam repository from github, add the checkout and disable the original.

view this post on Zulip Michael Soegtrop (Aug 14 2023 at 08:20):

I planned to do the Coq Platform release today (next slot would be Friday), but can't really do this with coq opam down. I wonder if I should build the work around into Coq Platform, but cloning and keeping it like this is not a good option IMHO. One can also reference git repos as in opam repo add --dont-select default-mingw 'https://github.com/ocaml-opam/opam-repository-mingw.git#sunset', but the coq repos are subfolders of a git repo. Is there some URL syntax for this opam supports?

view this post on Zulip Paolo Giarrusso (Aug 14 2023 at 09:37):

you can clone the repo locally and use opam's support for local folders as repos — IIRC, opam repo add --kind local coq-fork ./released/

view this post on Zulip Paolo Giarrusso (Aug 14 2023 at 09:38):

(that's in a checkout of https://github.com/coq/opam-coq-archive )

view this post on Zulip Paolo Giarrusso (Aug 14 2023 at 09:41):

Oh sorry, sounds like you don't like it — I see why that's annoying in automation (since one must update the checkout explicitly)

view this post on Zulip Karl Palmskog (Aug 14 2023 at 09:42):

I don't think we will have any updates in the Coq opam archive until Wednesday, at least I will not merge any PRs until then

view this post on Zulip Michael Soegtrop (Aug 14 2023 at 11:51):

My point is if I implement an alternative in the scripts, the opam setup would likely stay like this - so either we need scripts to normalise it later or it should be a configuration which is long time viable. I don't see a reason why one shouldn't link to github instead of the inria repo (is it slower?), but I have the issue that I don't see how to link subfolders.

view this post on Zulip Michael Soegtrop (Aug 14 2023 at 11:52):

I don't want to create a release with scripts I can't commit.

view this post on Zulip Karl Palmskog (Aug 14 2023 at 13:45):

I think that an ad-hoc Git-based directory will be slower, since from what I remember the deployment to the Coq website saves a compressed version of the whole repo

view this post on Zulip Michael Soegtrop (Aug 14 2023 at 15:20):

Anyway - I hope the servers are up again on Friday. Let's hope that there are no further examples of Murphy's law in this Coq Platform release ...

view this post on Zulip Michael Soegtrop (Aug 16 2023 at 07:25):

Even in the vacation period I find > two working days a bit long ...

Can we discuss solutions to alternatively linking the github repo directly? The main obstacle is that there are 3 opam repos in one git repo - which opam does not support (as far as I can tell). Which is the preferred solution:

This way I could check if the usual repo is available, and if not use the github repo in Coq Platform automatically (I would add a script to check and change the repo URLs later easily in either direction).

view this post on Zulip Karl Palmskog (Aug 16 2023 at 07:31):

as per above, there is/was compounding of: general vacation time + 2 days of French public holidays (Mon, Tue this week). I'd prefer to wait at least until end of today before discussing/making any opam-related decisions

view this post on Zulip Michael Soegtrop (Aug 16 2023 at 09:51):

My comment was more in general than for this specific situation. I anyway won't have time before Friday and I hope it does work by then. What I wanted to say is that if it can in general take > 2 working days to fix the INRIA web site, we should discuss a fallback mechanism.

view this post on Zulip Maxime Dénès (Aug 16 2023 at 11:40):

FYI I'm trying to have the problem fixed, but it is not easy as it is the worst week of the year in terms of people being available.

view this post on Zulip Maxime Dénès (Aug 16 2023 at 14:47):

Ok, I got it up again. I'll perform a few operations, expect some degraded service for ~1h.

view this post on Zulip Jason Gross (Aug 16 2023 at 18:28):

enhance opam to support subfolders in git repos as opam repo

Does opam repo add --kind local coq-fork ./released/ not work on arbitrary folders, whether in or out of a git repo?

view this post on Zulip Jason Gross (Aug 16 2023 at 18:29):

(Another option, btw, would be to clone the same repo three times into three folders)

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 18:42):

The feature request was to support that on remote kinds

view this post on Zulip Paolo Giarrusso (Aug 16 2023 at 18:43):

so that no local checkout is needed

view this post on Zulip Michael Soegtrop (Aug 16 2023 at 19:54):

@Jason Gross : the reason I want to link to remote repos is that I can't ask users to take care of updating the folder. If I put this into Coq Platform, it should work in a reasonable way. Git acces basically works - I am using it e.g. for the Opam MinGW repo, but not for subfolders of a git repo.

view this post on Zulip Maxime Dénès (Aug 17 2023 at 15:18):

FYI, in order to fix this recurring issue, we are going to try to migrate the website to github pages. The plan would be:

view this post on Zulip Michael Soegtrop (Aug 18 2023 at 07:09):

@Maxime Dénès : I actually would prefer a solution with a fallback. Github is also down from time to time. As an example: the repo of homebrew is broken since 2 months or so.

view this post on Zulip Karl Palmskog (Aug 18 2023 at 07:10):

if GitHub is down, then most of the opam packages won't work anyway

view this post on Zulip Maxime Dénès (Aug 18 2023 at 07:17):

I'm not familiar with the homebrew situation. Are they being impacted by a Github problem?

view this post on Zulip Michael Soegtrop (Aug 18 2023 at 07:43):

Essentially the repo is broken and Github didn't manage to find out how and why and to fix it (at least this was the status between June and July - I implemented a work around and didn't check since then). The effect is that git commands sometimes say that the repo is inconsistent (happens pretty much always at some point if homebrew is setup fresh).

For a discussion: https://github.com/orgs/Homebrew/discussions/4612#discussioncomment-6351357
The Coq Platform hack: https://github.com/coq/platform/commit/cf283e2f89c6961a27c77b6625299e028a46370c

view this post on Zulip Maxime Dénès (Aug 18 2023 at 07:45):

I see. But then for us the main risk is probably for the Coq repository itself, not so much for the small github pages website.

view this post on Zulip Paolo Giarrusso (Aug 18 2023 at 08:38):

Homebrew is also reported to be an extreme case, because of the amount of devs/users/changes

view this post on Zulip Paolo Giarrusso (Aug 18 2023 at 08:39):

(I can't find the original comment from brew devs; they linked to a github blog post, it might have been https://github.blog/2021-04-29-scaling-monorepo-maintenance/ — which does mention homebrew)

view this post on Zulip Maxime Dénès (Aug 19 2023 at 09:00):

Maxime Dénès said:

FYI, in order to fix this recurring issue, we are going to try to migrate the website to github pages. The plan would be:

First step done, I'll now rename www to coq.github.io and opam-coq-archive to opam and adjust their deployment. The impact should be minimal because github automatically puts redirections in place.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 18:54):

it seems the renaming to opam (perhaps not the best name, I'd have preferred opam-repository/opam-archive or similar) has killed off the GitLab CI, we got no CI here: https://github.com/coq/opam/pull/2675

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:05):

The name opam is constrained by the path, otherwise I wouldn't have touched it, personally. I can have a look at the CI setup, is the github <-> gitlab sync documented somewhere?

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:06):

It is strange, there's now an opam repo on gitlab (created 5h ago), but I don't remember doing it.

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:07):

Could it be that the repo was created by coqbot?

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:08):

The CI for 2675 landed there.

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:10):

Hmmm exactly at the same time the PR was opened, so coqbot probably did create a repo.

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:11):

I'll delete it and rename the existing one, it should help.

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:12):

Argh! It seems it takes one week to get it actually deleted.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 19:12):

I can create a new PR to test with, if you give the go I will open

view this post on Zulip Karl Palmskog (Aug 19 2023 at 19:13):

maybe just rename it then? or is that blocked too?

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:13):

Yep, I'll try

view this post on Zulip Maxime Dénès (Aug 19 2023 at 19:15):

Renaming seems to have worked. Maybe you can close / reopen the PR?

view this post on Zulip Karl Palmskog (Aug 19 2023 at 19:17):

OK, let's try that with the existing one, I have my doubts that will work. I'll try a completely new one afterwards.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 19:26):

CI apparently starts, but it doesn't have opam initialized. Maybe caching issue? https://github.com/coq/opam/pull/2675/checks

view this post on Zulip Karl Palmskog (Aug 19 2023 at 19:36):

hmm, some GitLab CI jobs are actually successful

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:37):

Reading https://github.com/coq/opam/blob/master/scripts/opam-coq-setup-root , it seems tar xzf $CACHE -C / implies the cache tarball hardcodes the running folder. Which contains the gitlab repo name

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:38):

While test -e $OPAM_ROOT_CACHE || scripts/opam-coq-init will run opam init if no cache tarball is found?

view this post on Zulip Paolo Giarrusso (Aug 19 2023 at 19:39):

*re "running folder contains the gitlab repo name": that's at least the default we see on gitlab.com, dunno if you've customized that elsewhere.

view this post on Zulip Maxime Dénès (Aug 20 2023 at 07:52):

@Karl Palmskog Clearing the cache seems to have fixed the CI pb.

view this post on Zulip Karl Palmskog (Aug 20 2023 at 09:46):

the new opam archive deployment is giving errors, will this be fixed by the new PR? https://github.com/coq/opam/pull/2679

view this post on Zulip Maxime Dénès (Aug 20 2023 at 10:15):

I don't know, because I'm working on it :)

view this post on Zulip Maxime Dénès (Aug 20 2023 at 10:17):

But you can ignore this part of the CI checks for now (i.e. merging with errors there is fine, as long as the gitlab ci part is ok).

view this post on Zulip Maxime Dénès (Aug 20 2023 at 10:59):

@Karl Palmskog All green now

view this post on Zulip Karl Palmskog (Aug 20 2023 at 11:00):

@Maxime Dénès but I don't understand why a GitLab pipeline is run on push to master? What is it supposed to do? https://github.com/coq/opam/runs/16044780104

view this post on Zulip Maxime Dénès (Aug 20 2023 at 11:01):

It is deploying to Github pages

view this post on Zulip Karl Palmskog (Aug 20 2023 at 11:01):

I thought the "CI deploy" action did that

view this post on Zulip Maxime Dénès (Aug 20 2023 at 11:03):

Ah sorry, I misread. I don't know why a gitlab ci pipeline is run on push, but isn't that the usual setup? Anyway I didn't touch it.

view this post on Zulip Maxime Dénès (Aug 20 2023 at 11:03):

I guess it makes sense to check that CI is ok post merge.

view this post on Zulip Karl Palmskog (Aug 20 2023 at 11:07):

oh OK, I guess the GitLab CI finished quickly

view this post on Zulip Théo Zimmermann (Aug 20 2023 at 17:00):

Maxime Dénès said:

Could it be that the repo was created by coqbot?

Indeed, that's one long-standing coqbot issue: https://github.com/coq/bot/issues/127

view this post on Zulip Théo Zimmermann (Aug 20 2023 at 17:01):

FWIW, it would have been possible to not rename the GitLab repo, by using coqbot support for synchronizing repositories with differing names.

view this post on Zulip Théo Zimmermann (Aug 20 2023 at 17:02):

And BTW, we had some explicit mapping for the opam-coq-archive repository that we should update now (to opam -> opam IIUC): https://github.com/coq/bot/blob/master/coqbot-config.toml


Last updated: Nov 29 2023 at 05:01 UTC