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

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

[Fabian Immler]

Dear isabelle-dev,

I noticed that currently (isabelle:ed0a7090167d, AFP:26f074817c9a) 
AFP/Native_Word fails to build on lxbroy10 (with ML_system_64=true):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype 
Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** At command "export_code" (line 889 of 
"~/work/afp/afp-devel/thys/Native_Word/Bits_Integer.thy")

The build works fine on e.g., lxbroy8. It also works on lxbroy10 with 
ML_system_64=false.

This is apparently since the introduction of polyml-5.7.1 
(isabelle:aefaaef29c58, AFP:c7180aa1cb8f).

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
### theory "Test.Test"
### 0.291s elapsed time, 0.009s cpu time, 0.000s GC time
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype 
Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** At command "export_code" (line 5 of "/mnt/home/immler/Test.thy")

Does anyone have an idea about this?
There seems to be an issue with the libraries on lxbroy10, but I wonder why 
this is only triggered with "export_code ... checking SML".

Best regards,
Fabian





smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev