On 07/11/2020 11:56, Makarius wrote:
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).
I can see the problem. The path is captured when the code is compiled.
This isn't a big problem but fixing it needs a small change to the
Foreign structure.
The key to understanding this is that there is a difference between
Foreign.System.loadLibrary/getSymbol and Foreign.loadLibrary/getSymbol.
The former call the underlying system calls immediately to get the
address, the latter don't. Instead they create functions that only call
the system when those functions are themselves called. The result is
then cached. Internally in the high-level Foreign structure the
"library" and "symbol" types are both defined as "unit->voidStar". This
means that although buildCall1, say, takes a "symbol" as an argument and
compiles an interface function containing the "symbol" it is actually
compiling a function that needs to call a function to get the address.
Underneath all this is the Foreign.Memory.volatileRef which is a special
kind of ref that can contain a C address but is always cleared to zero
at the start of a session. This can be used to cache the address of the
entry point to a function that could be different in different runs or
on different machines. If a volatileRef is written out with
PolyML.SaveState.saveState it will always be reset to zero when it is
loaded in with PolyML.SaveState.loadState.
What is needed is a hook so that when Foreign.library actually calls
Foreign.System.loadLibrary it first calls your function to get the path.
It would do this once immediately before calling "sha1_buffer" for the
first time during any run.
I'll think how best to do this.
David
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
