[isabelle-dev] Code check failed for SML on lxbroy10

[Makarius]

On 06/02/18 15:09, Fabian Immler wrote:
> 
> Stripping the problem down, I realized that this has nothing to do with Native_Word, because the same issue arises with the following theory:
> 
> theory Test imports HOL.Code_Generator begin
> export_code Code_Generator.holds checking SML
> end
> 
> The log says:
> 
> Loading theory "Test.Test"
> /home/immler/.isabelle/contrib/jdk-8u162/x86_64-linux/jre/bin/java: symbol lookup error: /usr/lib64/libhogweed.so.4: undefined symbol: __gmpn_cnd_add_n

That is a conflict of libgmp as bundled with our polyml component and
the one already installed on the system. It occurs here, because
LD_LIBRARY_PATH is augmented before starting the poly process, and then
java is started recursively for the generated code tests. With x86-linux
there is no problem, because java is an x86_64 process and ignores the
conflicting x86-linux libgmp.

Moreover, the problem appears to be specific to the Gentoo installation
of lxbroy10. I've never seen it on the many Ubuntu machines that I
routinely use for testing x86-linux and x86_64-linux.


In Isabelle/8b19a8a7f029 I have now changed the situation as follows:

  * polyml-5.7.1-1 no longer requires any local changes to
LD_LIBRARY_PATH (Linux) nor DYLD_LIBRARY_PATH (macOS). Instead the
library path is baked into the poly executable -- using funny tricks
that I did not know before, see
http://isabelle.in.tum.de/repos/isabelle/annotate/8b19a8a7f029/src/Pure/Admin/build_polyml.scala#l25
http://isabelle.in.tum.de/repos/isabelle/annotate/8b19a8a7f029/src/Pure/Admin/build_polyml.scala#l172

  * polyi is no longer needed: plain poly works as standalone executable

  * polyc should now work properly (it was never used for Isabelle)

  * libgmp is now provided for x86_64-darwin as well (before it was only
available for Linux and Windows); libgmp for x86-darwin still does not
work, because I don't know how to build it.

The explanations for libgmp on x86_64-darwin are in
polyml-5.7.1-1/README. If anybody figures out how to build the shared
library for x86-darwin, we can probably use it in the polyml component
to fill this remaining discontinuity.


	Makarius