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
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.
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/.
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.
It is really a matter of luck.
Does 8.14.1 fix the issue with bytecode architectures?
This does not ring a bell, so presumably not. Is there an open bug report?
Yes there is an open bug report, but I'm afraid we don't really have a reasonable mean to test these archs
I see no point on shipping Coq on archs we can't test
which are so slow that Coq is unusable to start with
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...
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/
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.
we should just have configure fail if there's no ocamlopt and forget about byte only
@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.
It's not only the manpower, but the lack of CI !
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
infinite
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.
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?
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
That's still to be traded off with the downsides above. Besides, arm64 is exotic enough for Coq!
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...
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)"
That might need updating, then
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.
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.
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
all other options are just too time involved for me
so we can keep the bug open tho, if someone would have interested to setup a byte-only CI
but indeed, I think supporting byte-only without CI is not supporting it at all
we can consider "supported" only what we test, the rest is magic
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