[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



-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5026 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180206/0578f9b3/attachment.p7s>