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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
