OCaml / aarch64 / binutils / coq mess

[Richard W.M. Jones]

OCaml 4.05 was added to Fedora 27+ recently.  Unfortunately, on
aarch64 only, it interacts badly with a change made in binutils 2.29
which tightens up the rules on relocations for PC-relative addresses.
More details:

  https://caml.inria.fr/mantis/view.php?id=7585            detailed discussion
  https://github.com/ocaml/ocaml/pull/1268                 partial solution
  https://sourceware.org/ml/binutils/2017-06/msg00171.html binutils change

This only affects dynamic loading of OCaml modules on aarch64, and in
particular it only affects the Coq theorem prover.  This package has a
number of dependencies, so it affects several other packages too.  I
believe the complete list is:

  - coq           Theorem prover
  - frama-c       Framework for source code analysis of C software
  - gappalib-coq  Coq support library for gappa
  - why           Software verification platform

I tried very hard to modify the OCaml aarch64 code generator to make
this work, but it seems as if the OCaml front end compiler doesn't
provide enough information for us to know if a particular symbol will
be used outside a module (it just assumes that all non-private symbols
can be used this way).  Or something.  Anyway I couldn't work out how
to fix it.

So ...  I don't know what to do here, but I guess possible options
include:

(1) Continue having broken dependencies for the affected packages on
aarch64 for a bit and see if upstream come up with anything.

(2) ‘ExcludeArch: aarch64’ on coq and its dependencies.  We would of
course file the relavent ExcludeArch bugs.  The thing that stops me
doing this is that we're nowhere nearer to having a fix, so it just
punts the problem, plus aarch64 is an important target and Coq is an
important package.

(3) Disable the problematic coq modules.  I'm not clear if they are
necessary however, since I've only used Coq as an end user, I've never
delved into how it works.

(4) Back out the binutils change?  I guess it was made for good
reasons even though it breaks everything.  Also it would be a
downstream change which is bad for Fedora, and we'd probably need to
mass-rebuild everything which is even worse.

(5) Your Plan Here.

Suggestions?

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
Fedora Windows cross-compiler. Compile Windows programs, test, and
build Windows installers. Over 100 libraries supported.
http://fedoraproject.org/wiki/MinGW

[Dan Horák]

On Tue, 29 Aug 2017 14:51:49 +0100
"Richard W.M. Jones" <rjones(a)redhat.com&gt; wrote:

>  OCaml 4.05 was added to Fedora 27+ recently.  Unfortunately, on
>  aarch64 only, it interacts badly with a change made in binutils 2.29
>  which tightens up the rules on relocations for PC-relative addresses.
>  More details:
>  
>    https://caml.inria.fr/mantis/view.php?id=7585            detailed discussion
>    https://github.com/ocaml/ocaml/pull/1268                 partial solution
>    https://sourceware.org/ml/binutils/2017-06/msg00171.html binutils change
>  
>  This only affects dynamic loading of OCaml modules on aarch64, and in
>  particular it only affects the Coq theorem prover.  This package has a
>  number of dependencies, so it affects several other packages too.  I
>  believe the complete list is:
>  
>    - coq           Theorem prover
>    - frama-c       Framework for source code analysis of C software
>    - gappalib-coq  Coq support library for gappa
>    - why           Software verification platform
>  
>  I tried very hard to modify the OCaml aarch64 code generator to make
>  this work, but it seems as if the OCaml front end compiler doesn't
>  provide enough information for us to know if a particular symbol will
>  be used outside a module (it just assumes that all non-private symbols
>  can be used this way).  Or something.  Anyway I couldn't work out how
>  to fix it.
>  
>  So ...  I don't know what to do here, but I guess possible options
>  include:
>  
>  (1) Continue having broken dependencies for the affected packages on
>  aarch64 for a bit and see if upstream come up with anything. 
I would lean to that "solution"

>  
>  (2) ‘ExcludeArch: aarch64’ on coq and its dependencies.  We would of
>  course file the relavent ExcludeArch bugs.  The thing that stops me
>  doing this is that we're nowhere nearer to having a fix, so it just
>  punts the problem, plus aarch64 is an important target and Coq is an
>  important package.
>  
>  (3) Disable the problematic coq modules.  I'm not clear if they are
>  necessary however, since I've only used Coq as an end user, I've never
>  delved into how it works.
>  
>  (4) Back out the binutils change?  I guess it was made for good
>  reasons even though it breaks everything.  Also it would be a
>  downstream change which is bad for Fedora, and we'd probably need to
>  mass-rebuild everything which is even worse.
>  
>  (5) Your Plan Here. 
I would file a bug against binutils to get attention from the
maintainer (nickc), not sure he is monitoring this list.


		Dan

> 
> Suggestions?
> 
> Rich.
> 
> -- 
> Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
> Read my programming and virtualization blog: http://rwmj.wordpress.com
> Fedora Windows cross-compiler. Compile Windows programs, test, and
> build Windows installers. Over 100 libraries supported.
> http://fedoraproject.org/wiki/MinGW
> _______________________________________________
> devel mailing list -- devel(a)lists.fedoraproject.org
> To unsubscribe send an email to devel-leave(a)lists.fedoraproject.org

[Jerry James]

On Wed, Aug 30, 2017 at 2:57 PM, Dan Horák <dan(a)danny.cz&gt; wrote:
>  On Tue, 29 Aug 2017 14:51:49 +0100
>  "Richard W.M. Jones" <rjones(a)redhat.com&gt; wrote:
>
> > (1) Continue having broken dependencies for the affected packages on
> > aarch64 for a bit and see if upstream come up with anything.
>
>  I would lean to that "solution" 
Me, too.  Let's give upstream a chance to fix the problem.

BTW, most of the packages that sit on top of coq have new versions
available, so when this is fixed, I will want to update the other
packages anyway.  If you could let me know when a fix for this issue
is available, I will take care of building everything else.

> > (2) ‘ExcludeArch: aarch64’ on coq and its dependencies.  We would
> of
> > course file the relavent ExcludeArch bugs.  The thing that stops me
> > doing this is that we're nowhere nearer to having a fix, so it just
> > punts the problem, plus aarch64 is an important target and Coq is an
> > important package. 
I'd say we should do this only if we are getting close to F27 beta
(maybe final) freeze and no upstream fix is in sight.  In that case,
we'll want to have the rebuilt packages available for other
architectures.

> > (3) Disable the problematic coq modules.  I'm not clear if
> they are
> > necessary however, since I've only used Coq as an end user, I've never
> > delved into how it works. 
Which ones are problematic?  All of them?
-- 
Jerry James
http://www.jamezone.org/

[Richard W.M. Jones]

On Wed, Aug 30, 2017 at 07:23:04PM -0600, Jerry James wrote:
>  BTW, most of the packages that sit on top of coq have new versions
>  available, so when this is fixed, I will want to update the other
>  packages anyway.  If you could let me know when a fix for this issue
>  is available, I will take care of building everything else. 
Sure.

>  >> (3) Disable the problematic coq modules.  I'm not clear
> if they are
>  >> necessary however, since I've only used Coq as an end user, I've never
>  >> delved into how it works.
>  
>  Which ones are problematic?  All of them? 
It could be all of them.  The first failure is:

  rm -f theories/Init/Datatypes.glob
  bin/coqtop -boot  -native-compiler -compile theories/Init/Datatypes.v  -noinit -R
theories Coq
  File "./theories/Init/Datatypes.v", line 13, characters 0-38:
  Error: while loading
  /home/rjones/d/coq/plugins/syntax/nat_syntax_plugin.cmxs:
  error loading shared library: /home/rjones/d/coq/plugins/syntax/nat_syntax_plugin.cmxs:
undefined symbol: camlLoc__3

(‘make -k’ doesn't get past this point)

The problem specifically is that we're carrying this patch:

  https://github.com/ocaml/ocaml/pull/1268

which marks most global symbols that need to be loaded into registers
as ‘.hidden’.  However this "over-hides", in this case hiding
camlLoc__3 (some anon function in the Loc module) which does actually
need to be public.

We need this patch to get OCaml to compile at all on aarch64, so the
answer is not to remove this patch, but to fix it in some other way.

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
virt-top is 'top' for virtual machines.  Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://people.redhat.com/~rjones/virt-top

[Richard W.M. Jones]

I believe I have come up with a patch which works well enough that we
can push it to Fedora 27+ aarch64:

 
https://pagure.io/fedora-ocaml/c/e7fdaf008e047c445fd7a6acf9362d8b5940bf4b...

Note this patch is not upstream but I've brought it to the attention
of the upstream maintainers.

I will do the rebuilds of the affected packages, and unless those
rebuilds fail there is nothing required for the package maintainers to
do.

However it would be helpful if you could all keep an eye on your
package and after it has been rebuilt try to do some testing (ideally
on aarch64, but even x86_64 testing has some use).

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
virt-top is 'top' for virtual machines.  Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://people.redhat.com/~rjones/virt-top

[Richard W.M. Jones]

Nearly done it.  Unfortunately I updated ‘why’ to the latest upstream
version (the previous one didn't know about OCaml 4.05), however that
will require updating ‘frama-c’:

  configure: WARNING: bad Frama-c version "Silicon-20161101", you need version
Phosphorus

At that point I stopped.  Would you mind updating and rebuilding
‘frama-c’ and ‘why’ in both Rawhide and F27?

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
virt-p2v converts physical machines to virtual machines.  Boot with a
live CD or over the network (PXE) and turn machines into KVM guests.
http://libguestfs.org/virt-v2v

[Jerry James]

On Wed, Sep 6, 2017 at 2:20 PM, Richard W.M. Jones <rjones(a)redhat.com&gt; wrote:
>  Nearly done it.  Unfortunately I updated ‘why’ to the latest
> upstream
>  version (the previous one didn't know about OCaml 4.05), however that
>  will require updating ‘frama-c’:
>
>    configure: WARNING: bad Frama-c version "Silicon-20161101", you need version
> Phosphorus
>
>  At that point I stopped.  Would you mind updating and rebuilding
>  ‘frama-c’ and ‘why’ in both Rawhide and F27? 
Yep.  That's why, earlier in this thread, I said:

BTW, most of the packages that sit on top of coq have new versions
available, so when this is fixed, I will want to update the other
packages anyway.  If you could let me know when a fix for this issue
is available, I will take care of building everything else.


I guess what I should have said was, "Don't rebuild anything that sits
on top of coq.  I'll take care of all of the builds since I have to do
some updates anyway."  Sorry for not being clearer.  I'll get those
updates done in the next day or two.  Thanks a lot for the aarch64 bug
fix.  I appreciate the work you put in on this.

Regards,
-- 
Jerry James
http://www.jamezone.org/

[Richard W.M. Jones]

On Wed, Sep 06, 2017 at 08:38:57PM -0600, Jerry James wrote:
>  On Wed, Sep 6, 2017 at 2:20 PM, Richard W.M. Jones
> <rjones(a)redhat.com&gt; wrote:
>  > Nearly done it.  Unfortunately I updated ‘why’ to the latest upstream
>  > version (the previous one didn't know about OCaml 4.05), however that
>  > will require updating ‘frama-c’:
>  >
>  >   configure: WARNING: bad Frama-c version "Silicon-20161101", you need
> version Phosphorus
>  >
>  > At that point I stopped.  Would you mind updating and rebuilding
>  > ‘frama-c’ and ‘why’ in both Rawhide and F27?
>  
>  Yep.  That's why, earlier in this thread, I said:
>  
>  BTW, most of the packages that sit on top of coq have new versions
>  available, so when this is fixed, I will want to update the other
>  packages anyway.  If you could let me know when a fix for this issue
>  is available, I will take care of building everything else.
>  
>  
>  I guess what I should have said was, "Don't rebuild anything that sits
>  on top of coq.  I'll take care of all of the builds since I have to do
>  some updates anyway."  Sorry for not being clearer.  I'll get those
>  updates done in the next day or two.  Thanks a lot for the aarch64 bug
>  fix.  I appreciate the work you put in on this. 
Great, thanks.  Don't forget that you need to submit updates for F27
packages and probably build overrides too using the clunky web
interface:

https://bodhi.fedoraproject.org/overrides/new

(Apparently the bodhi command line build override mechanism is broken,
at least, I couldn't work out how to fix it.)

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
virt-df lists disk usage of guests without needing to install any
software inside the virtual machine.  Supports Linux and Windows.
http://people.redhat.com/~rjones/virt-df/

[Richard W.M. Jones]

More news.

  https://github.com/ocaml/ocaml/pull/1330

Upstream came up with a different fix.  It's slower since every
reference (even within compilation units) now goes through the GOT,
but it's likely to be safer and it's the one they went with for the
future 4.06 release.

Therefore I have added this fix instead of mine to
ocaml-4.05.0-4.fc{27,28}.  I tested it first by rebuilding coq,
frama-c and a selection of other packages using the new compiler on my
local aarch64 machine and I didn't find any problems.

There is no action required, unless you wish to check that the new
compiler can still build your package.

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
Read my programming and virtualization blog: http://rwmj.wordpress.com
libguestfs lets you edit virtual machines.  Supports shell scripting,
bindings from many languages.  http://libguestfs.org

[Jerry James]

On Thu, Sep 14, 2017 at 6:49 AM, Richard W.M. Jones <rjones(a)redhat.com&gt; wrote:
>  More news.
>
>    https://github.com/ocaml/ocaml/pull/1330
>
>  Upstream came up with a different fix.  It's slower since every
>  reference (even within compilation units) now goes through the GOT,
>  but it's likely to be safer and it's the one they went with for the
>  future 4.06 release.
>
>  Therefore I have added this fix instead of mine to
>  ocaml-4.05.0-4.fc{27,28}.  I tested it first by rebuilding coq,
>  frama-c and a selection of other packages using the new compiler on my
>  local aarch64 machine and I didn't find any problems.
>
>  There is no action required, unless you wish to check that the new
>  compiler can still build your package. 
Thanks for the information, Richard.  Meanwhile, I did successfully
build the new version of frama-c, but the poppler update that went
into Rawhide and the subsequent failure of texlive to build on 32-bit
arches happened at about the same time, so I have not been able to
build the new version of why yet.  Here's hoping the texlive problems
can be resolved soon.

Regards,
-- 
Jerry James
http://www.jamezone.org/