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
