On 19/10/2020 13:12, David Matthews wrote: > > Instead the foreign function interface is handled essentially as part of the > compiler. The high-level interface in the Foreign structure remains unchanged > but the buildCallN functions now actually compile interface functions. This > results in foreign function calls being substantially faster than with libffi; > at least 10 times faster for trivial calls on the X86/64. The cost is, of > course, some extra work when buildCallN is called, meaning that it is > essential that these functions are only used at the top level.
I have adopted a current version from the Poly/ML repository, see https://isabelle-dev.sketis.net/rISABELLE63ec86626ec3 This did not require any changes, but I also started to experiment with clear division of the compile-time vs. run-time of Foreign calls. With mixed results, ending up to dismiss the attempt for now (Isabelle/18eed4f718e0). Some problems encountered so far: * Interpreted arm64-linux does not quite work. A statically compiled Foreign.buildCall within the heap image causes the dynamic invocation to "hang"; e.g. see https://isabelle-dev.sketis.net/rISABELLE7cb68b5b103d The problem (before the above change) can be reproduced on Raspberry Pi 4 / PI OS 64bit like this: $ isabelle build Pure $ isabelle console -l Pure ML> SHA1.digest "" (* hangs *) * Native x86_64_32-windows: building an image on one Windows server installation and running it on another one (Windows 10) caused an error in accessing the sha1.dll (different file location, potentially different load addresses). * I did not test linux and macos in that respect yet, but wonder if loading symbols from a shared library, and storing the result in the ML heap image can be portable over processes and OS installations. That is just my feedback for now. I guess we won't need the division of compiletime/runtime in Isabelle, because the only Foreign call is SHA1.digest, used on a few big blobs, and not invoked too often. Makarius _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
