https://coq.inria.fr/refman/addendum/type-classes.html times out here right now (trying from a German DSL connection)
tried a few machines via SSH and curl
, same result
ping coq.inria.fr
fails both via IPv4 and IPv6
Same here (also Germany)
same, Sweden
Same here (France)...
Damn! Who at Inria do we need to contact?
BTW, as a workaround: you can access the manual at https://coq.github.io/doc/V8.12.0/refman/
I hope it's not another spam submission like the time the website was down for days...
[FWIW, I can still connect to the server.]
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.
(At that time, the Inria IT staff had overreacted to something posted in our bug tracker.)
not just the manual, but I hear opam’s also down
opam update
fails on coq-released
(The actual data is on https://github.com/coq/opam-coq-archive/tree/master/released, so probably one can adapt the repo URL)
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
No, the two are on the same server.
Actually, I was wrong when I said the server was up. I had forgotten that we had moved to a server hosted outside Inria.
I tested the old Inria server.
But the new (OVH) server is actually unresponsive when trying to log in SSH.
So we need to contact OVH and I think our only point of contact is @Maxime Dénès.
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.
Hi guys! Sorry I just noticed this. I'll investigate now. Will report here.
It should be back in a few minutes.
It's back! Apologies for the inconvenience.
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.
the website is down for me again: https://coq.inria.fr https://coq.inria.fr/distrib etc.
Is this some Inria maintenance thing again?
Not maintenance, still payment unfortunately...
I reported the issue two hours ago, but it will probably take a miracle to be fixed before Wednesday (Monday & Tuesday are holidays).
Last time, I was told again that the process would be improved, but I guess it hasn't happened.
Incidentally, it blocked the second beta release of VsCoq 2 which was one click away.
I'll try again (and harder) to have the process improved in September.
oh damn, so Coq opam is down as well? ping @Michael Soegtrop this will affect the Platform
Unfortunately, yes.
conceivably, large parts of our automation infrastructure will be very affected (but not Coq dev, I guess)
ping also @Erik Martin-Dorel this will likely break all dev
Docker images (until Wednesday)
Ah OK; thanks @Karl Palmskog for letting me know
@Karl Palmskog : yes, all my CI failed, but I can live with that for a day or two.
opam update
is hanging on downloading https://coq.inria.fr/opam/core-dev/index.tar.gz
, I guess this is related?
yes, no Coq opam repos will work until the website is up again (they are hosted in the same virtual server)
FWIW one can clone the opam repository from github, add the checkout and disable the original.
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?
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/
(that's in a checkout of https://github.com/coq/opam-coq-archive )
Oh sorry, sounds like you don't like it — I see why that's annoying in automation (since one must update the checkout explicitly)
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
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.
I don't want to create a release with scripts I can't commit.
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
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 ...
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).
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
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.
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.
Ok, I got it up again. I'll perform a few operations, expect some degraded service for ~1h.
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?
(Another option, btw, would be to clone the same repo three times into three folders)
The feature request was to support that on remote kinds
so that no local checkout is needed
@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.
FYI, in order to fix this recurring issue, we are going to try to migrate the website to github pages. The plan would be:
/distrib
binary artifacts to a bucket, with redirections from the old paths to the new onescoq.github.io
(as a organization-level github pages repo)coq.github.io/coq
coq.github.io
to coq.inria.fr
@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.
if GitHub is down, then most of the opam packages won't work anyway
I'm not familiar with the homebrew situation. Are they being impacted by a Github problem?
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
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.
Homebrew is also reported to be an extreme case, because of the amount of devs/users/changes
(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)
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:
- Move the old
/distrib
binary artifacts to a bucket, with redirections from the old paths to the new ones- Have the website and the opam repo be deployed to
coq.github.io
(as a organization-level github pages repo)- Keep the deployment of the doc repo to
coq.github.io/doc
- Switch the domain from
coq.github.io
tocoq.inria.fr
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.
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
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?
It is strange, there's now an opam
repo on gitlab (created 5h ago), but I don't remember doing it.
Could it be that the repo was created by coqbot?
The CI for 2675 landed there.
Hmmm exactly at the same time the PR was opened, so coqbot probably did create a repo.
I'll delete it and rename the existing one, it should help.
Argh! It seems it takes one week to get it actually deleted.
I can create a new PR to test with, if you give the go I will open
maybe just rename it then? or is that blocked too?
Yep, I'll try
Renaming seems to have worked. Maybe you can close / reopen the PR?
OK, let's try that with the existing one, I have my doubts that will work. I'll try a completely new one afterwards.
CI apparently starts, but it doesn't have opam initialized. Maybe caching issue? https://github.com/coq/opam/pull/2675/checks
hmm, some GitLab CI jobs are actually successful
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
While test -e $OPAM_ROOT_CACHE || scripts/opam-coq-init
will run opam init
if no cache tarball is found?
*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.
@Karl Palmskog Clearing the cache seems to have fixed the CI pb.
the new opam archive deployment is giving errors, will this be fixed by the new PR? https://github.com/coq/opam/pull/2679
I don't know, because I'm working on it :)
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).
@Karl Palmskog All green now
@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
It is deploying to Github pages
I thought the "CI deploy" action did that
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.
I guess it makes sense to check that CI is ok post merge.
oh OK, I guess the GitLab CI finished quickly
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
FWIW, it would have been possible to not rename the GitLab repo, by using coqbot support for synchronizing repositories with differing names.
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