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