On 02/11/2020 17:05, Makarius wrote:
On 19/10/2020 13:12, David Matthews wrote: 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 *)
The interpreted version still uses libffi and that hadn't been tested as well as the compiled X86 version. I've fixed a couple of problems and it now seems fine.
- 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).
This is odd. I've been running some tests with various X86 platforms and not seen anything like this.
- 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.
Only the conversion function is stored in the heap. The entry point to the function is still found using lazy loading just as it was in the old version. When a foreign function is first used in a session the library is loaded and the symbol is looked up. From then on the cached value is used but only in the same session.
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.
It's not just efficiency, the interpreted version will leak C memory if the build functions are repeatedly called. This was the case before the recent changes on the X86 as well. It isn't any longer because the conversion functions on the X86 can be garbage collected.
David