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 _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
