Stream: Coq devs & plugin devs

Topic: Coq 8.14.1 changelog


view this post on Zulip 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

view this post on Zulip 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'

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:08):

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

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:26):

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.

view this post on Zulip 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/.

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:29):

It is really a matter of luck.

view this post on Zulip Julien Puydt (Dec 07 2021 at 16:36):

Does 8.14.1 fix the issue with bytecode architectures?

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:38):

This does not ring a bell, so presumably not. Is there an open bug report?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 16:42):

I see no point on shipping Coq on archs we can't test

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 16:42):

which are so slow that Coq is unusable to start with

view this post on Zulip 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...

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 17:22):

It's not only the manpower, but the lack of CI !

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2021 at 17:23):

infinite

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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)"

view this post on Zulip Julien Puydt (Dec 08 2021 at 08:58):

That might need updating, then

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):

all other options are just too time involved for me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 13:16):

we can consider "supported" only what we test, the rest is magic

view this post on Zulip 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: Feb 06 2023 at 00:03 UTC