[isabelle-dev] Code check failed for SML on lxbroy10
makarius at sketis.net
Fri Feb 9 21:16:22 CET 2018
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
> 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
* 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.
More information about the isabelle-dev