Ralf Jung (Nov 12 2020 at 17:28): 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)
Ralf Jung (Nov 12 2020 at 17:29):tried a few machines via SSH and curl, same result
Ralf Jung (Nov 12 2020 at 17:30):ping coq.inria.fr fails both via IPv4 and IPv6
Paolo Giarrusso (Nov 12 2020 at 17:31):Same here (also Germany)
Karl Palmskog (Nov 12 2020 at 17:33):same, Sweden
Pierre-Marie Pédrot (Nov 12 2020 at 17:34):Same here (France)...
Théo Zimmermann (Nov 12 2020 at 17:40):Damn! Who at Inria do we need to contact?
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/
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...
Théo Zimmermann (Nov 12 2020 at 17:42):[FWIW, I can still connect to the server.]
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.
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.)
Paolo Giarrusso (Nov 12 2020 at 18:24):not just the manual, but I hear opam’s also down
Paolo Giarrusso (Nov 12 2020 at 18:34):opam update fails on coq-released
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)
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
Théo Zimmermann (Nov 12 2020 at 19:50):No, the two are on the same server.
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.
Théo Zimmermann (Nov 12 2020 at 19:53):I tested the old Inria server.
Théo Zimmermann (Nov 12 2020 at 19:53):But the new (OVH) server is actually unresponsive when trying to log in SSH.
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.
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.
Maxime Dénès (Nov 13 2020 at 08:24):Hi guys! Sorry I just noticed this. I'll investigate now. Will report here.
Maxime Dénès (Nov 13 2020 at 09:07):It should be back in a few minutes.
Maxime Dénès (Nov 13 2020 at 09:13):It's back! Apologies for the inconvenience.
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.
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?
Maxime Dénès (Aug 11 2023 at 18:14):Not maintenance, still payment unfortunately...
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).
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.
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.
Maxime Dénès (Aug 11 2023 at 18:19):I'll try again (and harder) to have the process improved in September.
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
Maxime Dénès (Aug 11 2023 at 18:19):Unfortunately, yes.
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)
Karl Palmskog (Aug 11 2023 at 18:24):ping also @Erik Martin-Dorel this will likely break all dev Docker images (until Wednesday)
Erik Martin-Dorel (Aug 11 2023 at 18:35):Ah OK; thanks @Karl Palmskog for letting me know
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.
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?
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)
Paolo Giarrusso (Aug 12 2023 at 20:39):FWIW one can clone the opam repository from github, add the checkout and disable the original.
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?
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/
Paolo Giarrusso (Aug 14 2023 at 09:38):(that's in a checkout of https://github.com/coq/opam-coq-archive )
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)
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
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.
Michael Soegtrop (Aug 14 2023 at 11:52):I don't want to create a release with scripts I can't commit.
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
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 ...
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).
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
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.
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.
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.
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?
Jason Gross (Aug 16 2023 at 18:29):(Another option, btw, would be to clone the same repo three times into three folders)
Paolo Giarrusso (Aug 16 2023 at 18:42):The feature request was to support that on remote kinds
Paolo Giarrusso (Aug 16 2023 at 18:43):so that no local checkout is needed
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.
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:
/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/coqcoq.github.io to coq.inria.fr 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.
Karl Palmskog (Aug 18 2023 at 07:10):if GitHub is down, then most of the opam packages won't work anyway
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?
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
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.
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
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)
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:
- Move the old
/distribbinary 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.iotocoq.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.
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
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?
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.
Maxime Dénès (Aug 19 2023 at 19:07):Could it be that the repo was created by coqbot?
Maxime Dénès (Aug 19 2023 at 19:08):The CI for 2675 landed there.
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.
Maxime Dénès (Aug 19 2023 at 19:11):I'll delete it and rename the existing one, it should help.
Maxime Dénès (Aug 19 2023 at 19:12):Argh! It seems it takes one week to get it actually deleted.
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
Karl Palmskog (Aug 19 2023 at 19:13):maybe just rename it then? or is that blocked too?
Maxime Dénès (Aug 19 2023 at 19:13):Yep, I'll try
Maxime Dénès (Aug 19 2023 at 19:15):Renaming seems to have worked. Maybe you can close / reopen the PR?
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.
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
Karl Palmskog (Aug 19 2023 at 19:36):hmm, some GitLab CI jobs are actually successful
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
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?
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.
Maxime Dénès (Aug 20 2023 at 07:52):@Karl Palmskog Clearing the cache seems to have fixed the CI pb.
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
Maxime Dénès (Aug 20 2023 at 10:15):I don't know, because I'm working on it :)
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).
Maxime Dénès (Aug 20 2023 at 10:59):@Karl Palmskog All green now
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
Maxime Dénès (Aug 20 2023 at 11:01):It is deploying to Github pages
Karl Palmskog (Aug 20 2023 at 11:01):I thought the "CI deploy" action did that
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.
Maxime Dénès (Aug 20 2023 at 11:03):I guess it makes sense to check that CI is ok post merge.
Karl Palmskog (Aug 20 2023 at 11:07):oh OK, I guess the GitLab CI finished quickly
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
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.
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