I have a couple of comments and a query about polyc (which seemed particularly attractive on Cygwin, where there seems to be quite a long list of libraries you need to know about if you are going to call the linker directly).
The comment is that the help text is a bit misleading as it has more functionality than just compiling and linking a source file, e.g., you can pass it the name of an object file and it will link it with libpolymain and libpolyml.
The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.)
Regards,
Rob.
On Wed, 23 Apr 2014, Rob Arthan wrote:
The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.)
Just empirically, from maintaining Poly/ML executables for Isabelle since 2008 on all three platform families, my rules of thumb are like this:
* Linux: tinkering with LD_LIBRARY_PATH and hoping for the best concerning the global libc/libc++ personality wrt. x86/x86_64. (Linux users are surprisingly ignorant about what they have.)
* Mac OS X: tinkering with DYLD_LIBRARY_PATH and relying on the fact that both x86/x86_64 works on current Macs unconditionally.
* Windows: no tinkering at all, merely relying on the fact that DLLs are first looked-up in the same directory as the main .exe
Classically, Cygwin always uses x86, which is not a problem due to the wonderful online heap sharing that David Matthews implemented in the past few years. Cygwin x86_64 has emerged recently, but I have not tried it yet.
What might be also interesting is MinGW for x86 or x86_64, but I have not really tried that either.
Makarius
Hi Rob,
23/04/14 17:13, Rob Arthan wrote:
The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.)
I believe that, by default, Gcc default would not link libpolyml statically if a shared version of the library exists. Whether the shared version exists depends on the particular Poly/ML installation. Supplying the argument --enable-shared to 'configure' when building creates the SO file.
If Poly/ML is built with a shared library and is not installed to a system location (so the libpolyml SO file is not automatically found), then executables from polyc require LD_LIBRARY_PATH to be set. Setting the linker path in polyc came up in discussion before, in a thread starting here: http://lists.inf.ed.ac.uk/pipermail/polyml/2013-April/001216.html (due to the comment in item 3) The current position seems to be that anyone installing (a shared version) to a non-system location needs to set LD_LIBRARY_PATH, just as they will need to set PATH.
I believe that LD_RUN_PATH can be specified in the environment for polyc to achieve the required effect. However, its value would have to be determined, which is unfortunate given that polyc has this information internally (libdir). The PC file for use with pkg-config is an alternative that is useful for Makefiles, e.g.
POLYMLLIB := `pkg-config polyml --variable=libdir`
$(NAME)-polyml : $(NAME)-polyml.o @LD_RUN_PATH=$(POLYMLLIB):$(LD_RUN_PATH) $(CC) -ggdb -o $@ `pkg-config --libs polyml` $<
but you may not want a dependency on that utility.
Regards, Phil
P.S. I think there have been a few updates/fixes to polyc since the 5.5.1 release.
Hi Rob, I've been away and I'm now just trying to catch up.
On 23/04/2014 17:13, Rob Arthan wrote:
I have a couple of comments and a query about polyc (which seemed particularly attractive on Cygwin, where there seems to be quite a long list of libraries you need to know about if you are going to call the linker directly).
The comment is that the help text is a bit misleading as it has more functionality than just compiling and linking a source file, e.g., you can pass it the name of an object file and it will link it with libpolymain and libpolyml.
I take it you mean the text that gets printed with polyc --help. The man page contains a bit more. Any suggestions for a suitable, brief replacement?
The query relates to the fact that polyc doesn?t do anything with LD_RUN_PATH (or DYLD_LIBRARY_PATH on Mac OS). Am I right in thinking that libpolyml will now always be statically linked so that you no longer to need to tell the dynamic linker where to find it? (For Poly/ML versions 5.5 and earlier the ProofPower makefiles that I am updating used to create an executable that linked libpolyml dynamically.)
What exactly does LD_RUN_PATH do and how does it relate to LD_LIBRARY_PATH? With the default setting of --disable-shared there should not be any need to specify the location of a shared library. Of course, if --enable-shared is given explicitly then there will be, but I would have thought that that would only be used when packaging for a system where the libraries were being installed to the "standard" location.
polyc is really a work in progress and I'm happy to receive suggestions to improve it.
On a more general note, I think it's time for a new release of Poly/ML. Unless there are any immediate bug reports I'm planning to release the current SVN as 5.5.2.
David
On 6 May 2014, at 12:56, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Hi Rob, I've been away and I'm now just trying to catch up.
On 23/04/2014 17:13, Rob Arthan wrote:
I have a couple of comments and a query about polyc (which seemed particularly attractive on Cygwin, where there seems to be quite a long list of libraries you need to know about if you are going to call the linker directly).
The comment is that the help text is a bit misleading as it has more functionality than just compiling and linking a source file, e.g., you can pass it the name of an object file and it will link it with libpolymain and libpolyml.
I take it you mean the text that gets printed with polyc --help. The man page contains a bit more. Any suggestions for a suitable, brief replacement?
Yes, that is what I meant. I had a go at this, but came to a halt when I realised that the implementation didn?t quite match the man page or my expectations. I expected polyc to use the file name extension to distinguish between source files and object files. The man page says it treats text files as source files and binary files as object files. The implementation checks the extension first and uses that to make the distinction if it recognises it. Otherwise it has a go at using the file program to see if the file is a text file. Was this actually what was intended? It seems odd not just to rely on the extensions (perhaps making them case insensitive, so you would recognise foo.ml and FOO.SML as well as foo.ML and foo.sml).
Here is the text I would propose for the implementation I expected:
Usage: polyc [OPTION]... [SOURCEFILE | OBJECTFILE]
Compile and/or link a file with Poly/ML.
A Standard ML source file has extension .ML or .sml and must define a function 'main' of type 'unit -> unit' that will be called when the executable is run. An object file has a .o extension.
Options:
-c Compile but do not link, writing an object file with the same base name as the source file -o <file> Write the executable file to <file> (default 'a.out') Ignored if not linking --help Write this help text and exit
Regards,
Rob.
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
phil.clayton＠veonix.com -
rda＠lemma-one.com