Guillaume Melquiond (Dec 07 2021 at 15:52): Guillaume Melquiond (Dec 07 2021 at 15:52):By the way, there is something terribly wrong with the changelog for 8.14.1 on the website: https://coq.github.io/doc/v8.14/refman/changes.html#changes-in-8-14-1 . It does not match the content of https://github.com/coq/coq/blob/v8.14/doc/sphinx/changes.rst#changes-in-8141
Guillaume Melquiond (Dec 07 2021 at 15:59):I guess this makes sense. But it also means we cannot refer to the documentation of a branch.
$ git push
Warning: Permanently added the RSA host key for IP address '140.82.113.3' to the list of known hosts.
To github.com:coq/doc.git
! [rejected] master -> master (fetch first)
error: failed to push some refs to 'git@github.com:coq/doc.git'
And actually, it seems someone at least was aware of this bug, since there is the following comment in the doc:refman:deploy job:
git push # TODO: rebase and retry on failure
So, retrying the job until it goes through successfully is enough to fix the issue. But I guess it could be written in the release manager checklist.
Théo Zimmermann (Dec 07 2021 at 16:27):Or else, use the tagged version: https://coq.github.io/doc/V8.14.1/refman/changes.html#changes-in-8-14-1 a.k.a. https://coq.inria.fr/distrib/V8.14.1/refman/.
Guillaume Melquiond (Dec 07 2021 at 16:29):This does not change the underlying issue. You still need to find a job that succeeded in doing git push to know which url to use. The push into the V8.14.1 directory could have failed just as well.
Guillaume Melquiond (Dec 07 2021 at 16:29):It is really a matter of luck.
Julien Puydt (Dec 07 2021 at 16:36):Does 8.14.1 fix the issue with bytecode architectures?
Guillaume Melquiond (Dec 07 2021 at 16:38):This does not ring a bell, so presumably not. Is there an open bug report?
Emilio Jesús Gallego Arias (Dec 07 2021 at 16:42):Yes there is an open bug report, but I'm afraid we don't really have a reasonable mean to test these archs
Emilio Jesús Gallego Arias (Dec 07 2021 at 16:42):I see no point on shipping Coq on archs we can't test
Emilio Jesús Gallego Arias (Dec 07 2021 at 16:42):which are so slow that Coq is unusable to start with
Emilio Jesús Gallego Arias (Dec 07 2021 at 16:43):I'd be very happy to fix a byte-only build if someone setups a toolchain in our CI that can test that, but so far I only heard really ugly hacks such as "delete ocamlopt" etc...
Julien Puydt (Dec 07 2021 at 17:11):Well, it's possible to get access to ugly architectures, and once they are fixed, the Debian build daemons will cry anytime they break... how do you think I know? ;-)
PS: https://dsa.debian.org/doc/guest-account/
Théo Zimmermann (Dec 07 2021 at 17:16):The point (I think) is that we don't care enough (given our manpower). This is what I told Ralf when he asked me about it in my office.
Gaëtan Gilbert (Dec 07 2021 at 17:17):we should just have configure fail if there's no ocamlopt and forget about byte only
Emilio Jesús Gallego Arias (Dec 07 2021 at 17:21):@Julien Puydt I am aware I can get access to these machines, but they are super slow in general, so unless we are able to do byte-only in x64 / arm I'm afraid the time investment for us is just not worth it.
Emilio Jesús Gallego Arias (Dec 07 2021 at 17:22):It's not only the manpower, but the lack of CI !
Emilio Jesús Gallego Arias (Dec 07 2021 at 17:23):And moreover, the fact that nobody is using Coq on these archs, so even if the manpower needed would be epsilon, the effort/benefit ratio would be infitive
Emilio Jesús Gallego Arias (Dec 07 2021 at 17:23):infinite
Julien Puydt (Dec 07 2021 at 17:51):Théo Zimmermann said:
The point (I think) is that we don't care enough (given our manpower). This is what I told Ralf when he asked me about it in my office.
Exotic architectures are like mine canaries : they will provide early warnings of problems.
Emilio Jesús Gallego Arias (Dec 07 2021 at 17:54):Julien Puydt said:
Théo Zimmermann said:
The point (I think) is that we don't care enough (given our manpower). This is what I told Ralf when he asked me about it in my office.
Exotic architectures are like mine canaries : they will provide early warnings of problems.
Do you have an example of such a problem?
Julien Puydt (Dec 07 2021 at 19:10):I'm the maintainer of the packages for libraries like flint and flint-arb, and I'm generally the one to see and report strange issues because of the Debian build daemons reporting ; for example https://github.com/wbhart/flint2/issues/784 or https://github.com/wbhart/flint2/issues/771
Paolo Giarrusso (Dec 07 2021 at 20:39):That's still to be traded off with the downsides above. Besides, arm64 is exotic enough for Coq!
Julien Puydt (Dec 08 2021 at 07:57):Paolo Giarrusso said:
That's still to be traded off with the downsides above. Besides, arm64 is exotic enough for Coq!
If that's an official statement that the architectures are abandoned, I'll also drop them officially from the package...
Pierre Roux (Dec 08 2021 at 08:21):AFAIK, we have no official list of supported architecture, the only requirement (in INSTALL.md) seems to be
"an IEEE-754 compliant architecture with rounding to nearest
ties to even as default rounding mode (most architectures
should work nowadays)"
Julien Puydt (Dec 08 2021 at 08:58):That might need updating, then
Théo Zimmermann (Dec 08 2021 at 09:53):Indeed, I think @Gaëtan Gilbert and @Emilio Jesús Gallego Arias were suggesting to officially state that byte-only architectures are no longer supported.
Julien Puydt (Dec 08 2021 at 11:14):Just close my report about them being broken, and I'll do the necessary on the Debian end so those architectures get out of the picture.
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):Note that as I said I wouldn't mind supporting them, it is just that I have no good way to get a byte-only setup in my dev machine
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):all other options are just too time involved for me
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):so we can keep the bug open tho, if someone would have interested to setup a byte-only CI
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):but indeed, I think supporting byte-only without CI is not supporting it at all
Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):we can consider "supported" only what we test, the rest is magic
Théo Zimmermann (Dec 08 2021 at 13:17):It's fine to keep the bug report open, but we should formally state in INSTALL.md that we don't support byte-only architectures.
Last updated: Jun 09 2023 at 07:01 UTC