On 04/11/2020 18:10, David Matthews wrote:
?? * 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.
Isabelle/81518b38b316 is back to the static invocation: https://isabelle-dev.sketis.net/rISABELLE81518b38b316 --- it also uses an updated polyml-test-7e49fce62e3d.
The above problem is rather profane: I am using Foreign.loadLibrary with the symbolic path "$ML_HOME/sha1.dll" (or .so), but that gets normalized at compile-time. Later at run-time, the Isabelle directory hierarchy might have been moved elsewhere (e.g. a user downloading our pre-built distribution and unpacking it locally).
You can try it with current https://isabelle.sketis.net/devel/release_snapshot (Isabelle/653ac845b466) e.g. on Linux:
$ Isabelle_07-Nov-2020/bin/isabelle console -l Pure Poly/ML> SHA1.digest ""; ### Loading </tmp/tmp.9wQavOmIEp/contrib/polyml-test-7e49fce62e3d/x86_64_32-linux/libsha1.so> failed: /tmp/tmp.9wQavOmIEp/contrib/polyml-test-7e49fce62e3d/x86_64_32-linux/libsha1.so: cannot open shared object file: No such file or directory ### Using slow ML implementation of SHA1.digest val it = "da39a3ee5e6b4b0d3255bfef95601890afd80709": SHA1.digest
(The tmp-directory is from the automatic build process.)
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.
This means we need to get this conceptually right, and cannot just sweep it under the carpet.
Makarius