Re: [polyml] polyc and libraries
Phil, I've now added -lpolymain to polyml.pc.in so that should handle your specific problem. Can you check it? I'd be happy if you could produce an improved version of this. It's not something I use or have any familiarity with. Regards, David On 19/12/2017 21:47, Phil Clayton wrote: David, I think I would expect `pkg-config --libs polyml` to provide the linker flags required to create an executable, i.e. I wouldn't expect to have to specify -lpolymain additionally. I can't think of any other use cases of pkg-config because Poly/ML can't be used to produce a library. Even if it could, I don't believe adding -lpolymain would cause overlinking because only an archive version of libpolymain is available (and should always be available) and this shouldn't be included by the linker if there is no reference to the symbol "main". For Poly/ML built with --disable-shared, Libs still has all the linker flags, as I would expect, except for -lpolymain. If -lpolymain is added, it appears that it would need to be added _before_ -lpolyml (where it used to be), at least for my Linux distribution. On a separate note, for Poly/ML built with --enable-shared, I believe that the flags recently removed to avoid overlinking should still be produced if `pkg-config --static ...` is used, so should appear in Libs.private. However, it looks like this is only useful in the unusual case where all dependencies are to be statically linked. Most distributions don't supply archives for all libraries so that isn't usually possible. For Poly/ML built with --enable-shared, static linking of the Poly/ML library but not its dependencies is possible, e.g. gcc file.o \ -Wl,-Bstatic \ -L/tmp/polyml/lib -lpolymain -lpolyml \ -Wl,-Bdynamic \ -lpthread -lffi -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc but `pkg-config --static ...` can't produce such commands. Such a command could be produced with some shell trickery to get static-only dependencies, so perhaps it is worth supporting --static. Finally, I note that libffi has its own PC file, so when Poly/ML is built with --with-system-libffi, instead of adding -lffi to Libs/Libs.private, libffi could be added to Requires/Requires.private, respectively. Phil On 18/12/17 15:47, David Matthews wrote: Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
David, I think I would expect `pkg-config --libs polyml` to provide the linker flags required to create an executable, i.e. I wouldn't expect to have to specify -lpolymain additionally. I can't think of any other use cases of pkg-config because Poly/ML can't be used to produce a library. Even if it could, I don't believe adding -lpolymain would cause overlinking because only an archive version of libpolymain is available (and should always be available) and this shouldn't be included by the linker if there is no reference to the symbol "main". For Poly/ML built with --disable-shared, Libs still has all the linker flags, as I would expect, except for -lpolymain. If -lpolymain is added, it appears that it would need to be added _before_ -lpolyml (where it used to be), at least for my Linux distribution. On a separate note, for Poly/ML built with --enable-shared, I believe that the flags recently removed to avoid overlinking should still be produced if `pkg-config --static ...` is used, so should appear in Libs.private. However, it looks like this is only useful in the unusual case where all dependencies are to be statically linked. Most distributions don't supply archives for all libraries so that isn't usually possible. For Poly/ML built with --enable-shared, static linking of the Poly/ML library but not its dependencies is possible, e.g. gcc file.o \ -Wl,-Bstatic \ -L/tmp/polyml/lib -lpolymain -lpolyml \ -Wl,-Bdynamic \ -lpthread -lffi -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc but `pkg-config --static ...` can't produce such commands. Such a command could be produced with some shell trickery to get static-only dependencies, so perhaps it is worth supporting --static. Finally, I note that libffi has its own PC file, so when Poly/ML is built with --with-system-libffi, instead of adding -lffi to Libs/Libs.private, libffi could be added to Requires/Requires.private, respectively. Phil On 18/12/17 15:47, David Matthews wrote: Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 18:41, Makarius wrote: On 15/12/17 17:46, David Matthews wrote: On 15/12/2017 16:15, Makarius wrote: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? See the included change: my very first commit produced with git (with VSCode and gitk). Thanks. I've merged and pushed it. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 18:41, Makarius wrote: On 15/12/17 17:46, David Matthews wrote: On 15/12/2017 16:15, Makarius wrote: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? See the included change: my very first commit produced with git (with VSCode and gitk). Thanks. I'll have a look at that. * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. The paths are set from the installation directories in configure i.e. where the binaries and libraries are to be installed. It's possible to set the library and binary directories independently so there's no necessary relationship between them. The above change might already be sufficient for that: isabelle build_polyml merely needs to change /bin/sh into bash and make the prefix relative. This will allow users of Isabelle to use the bundled Poly/ML polyc, even though it is not directly relevant for Isabelle -- see also https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00144.html I don't think you can give configure anything but absolute paths but when I'm testing I usually set --libdir, --bindir and --mandir to the same directory so everything ends up in the same place. The only case where I've had a problem is with shared libraries in Msys/Mingw where libtool insists on putting the DLL in "libdir/../bin". I see further references to the install dir in: pkgconfig/polyml.pc libpolymain.la libpolyml.la Are these relevant for polyc? No. polyml.pc is only used if you have pkg_config. The other two are only used by libtool as far as I'm aware. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 16:15, Makarius wrote: On 12/12/17 14:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Here are some further observations and open problems from the past: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. The paths are set from the installation directories in configure i.e. where the binaries and libraries are to be installed. It's possible to set the library and binary directories independently so there's no necessary relationship between them. * Use of libgmp on Mac OS X is generally unclear to me. Is there a robust way to build poly with gmp on an old OS version (e.g. Mac OS X 10.10) and use it on a newer one? Is there any chance to do this with x86 instead of x86_64? There have been problems with linking libgmp and Poly/ML on Mac OS X in the past. Is there someone who uses Mac OS who could answer this? David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
There seems to be a problem with building it as a shared library in FreeBSD. It seems to work fine with ./configure --disable-shared David On 15/12/2017 12:58, Kostirya wrote: It is broken. I think this is because of the inconsistency of the options: -nostdlib and -lstdc++. libtool: link: c++ -fPIC -DPIC -shared -nostdlib /usr/lib/crti.o /usr/lib/crtbeginS.o .libs/arb.o .libs/basicio.o .libs/bitmap.o .libs/check_objects.o .libs/diagnostics.o .libs/errors.o .libs/exporter.o .libs/foreign.o .libs/gc.o .libs/gc_check_weak_ref.o .libs/gc_copy_phase.o .libs/gc_mark_phase.o .libs/gc_share_phase.o .libs/gc_update_phase.o .libs/gctaskfarm.o .libs/heapsizing.o .libs/locking.o .libs/memmgr.o .libs/mpoly.o .libs/network.o .libs/objsize.o .libs/osmem.o .libs/pexport.o .libs/poly_specific.o .libs/polyffi.o .libs/polystring.o .libs/process_env.o .libs/processes.o .libs/profiling.o .libs/quick_gc.o .libs/realconv.o .libs/reals.o .libs/rts_module.o .libs/rtsentry.o .libs/run_time.o .libs/save_vec.o .libs/savestate.o .libs/scanaddrs.o .libs/sharedata.o .libs/sighandler.o .libs/statistics.o .libs/timing.o .libs/xwindows.o .libs/x86_dep.o .libs/x86assembly_gas32.o .libs/elfexport.o .libs/unix_specific.o -Wl,--whole-archive libffi/.libs/libffi_convenience.a -Wl,--no-whole-archive -L/usr/local/lib -lpthread -lgmp -lstdc++ -L/usr/lib -lc++ -lm -lc -lgcc -lgcc_s /usr/lib/crtendS.o /usr/lib/crtn.o -O3 -Wl,-soname -Wl,libpolyml.so.9 -o .libs/libpolyml.so.9.0.0 /usr/bin/ld: cannot find -lstdc++ c++: error: linker command failed with exit code 1 (use -v to see invocation) *** Error code 1 Stop. make[1]: stopped in /scr/polyml_git/libpolyml *** Error code 1 I delete AC_CHECK_LIB(stdc++, main) line from configure.ac and do successfully built polyml on FreeBSD and DragonFlyBSD. But stdc++ is need for linux... ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 12/12/17 14:14, David Matthews wrote: > The polyc script has been developed mainly to simplify the linking of an > exported ML function and in particular to try to capture the libraries > that need to be included. I've been having another look at this because > of an issue that was reported a while back. Here are some further observations and open problems from the past: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. * Use of libgmp on Mac OS X is generally unclear to me. Is there a robust way to build poly with gmp on an old OS version (e.g. Mac OS X 10.10) and use it on a newer one? Is there any chance to do this with x86 instead of x86_64? Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc with different base executable
23/09/15 03:11, Michael Norrish wrote: Or is there another way of getting what I need? I'd like to dispense with explicit calls in our own code to PolyML.export, and then needing to call the linker, but we do want to be able to build heaps in this way, layer by layer. Have you looked at PolyML.SaveState ? http://www.polyml.org/documentation/Reference/PolyMLSaveState.html Phil ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
Hi Phil, I've changed configure so that FFI_LIBS gets added to LIBS within the configure script. This should avoid the need to add it explicitly in other places. Let me know if there are problems. David On 23/03/2015 23:45, Phil Clayton wrote: Hi David, 15/10/13 17:50, David Matthews wrote: On 15/10/2013 17:38, René Neumann wrote: @David: Have you seen my other issue in the original email? Was this the --with-system-ffi issue? I've fixed it in SVN trunk. It may be something to port to the fixed branch. It looks like r1871 didn't update polyml.pc.in similarly. pkg-config is not producing -lffi when Poly/ML is built with --with-system-ffi Phil ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
Hi David, Thanks - I've tried building an application with r1985 in the following configurations and pkg-config is working now: static, non-system libffi static, system libffi shared, non-system libffi shared, system libffi Phil 24/03/15 12:01, David Matthews wrote: Hi Phil, I've changed configure so that FFI_LIBS gets added to LIBS within the configure script. This should avoid the need to add it explicitly in other places. Let me know if there are problems. David On 23/03/2015 23:45, Phil Clayton wrote: Hi David, 15/10/13 17:50, David Matthews wrote: On 15/10/2013 17:38, René Neumann wrote: @David: Have you seen my other issue in the original email? Was this the --with-system-ffi issue? I've fixed it in SVN trunk. It may be something to port to the fixed branch. It looks like r1871 didn't update polyml.pc.in similarly. pkg-config is not producing -lffi when Poly/ML is built with --with-system-ffi Phil ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc
On 6 May 2014, at 12:56, David Matthews david.matth...@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 fileWrite the executable file to file (default 'a.out') Ignored if not linking --help Write this help text and exit Regards, Rob. ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc
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 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc
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. ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc
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 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
Am 11.10.2013 15:42, schrieb David Matthews: On 11/10/2013 14:17, René Neumann wrote: Am 11.10.2013 15:12, schrieb Ramana Kumar: (Ie, what I want: if is_script then main() else () ) If your main : unit - unit (which perhaps it must be?), then main() is equivalent to the if expression above, modulo side-effects. There is a misunderstanding here: I need the main to be run with poly --script -- which does not run it by default. But if I'd include 'main ()' in the script itself, it'd be run on compiling too (which I'd like to avoid). I'm still unclear what you're trying to achieve. Are you trying to write a single file that can either be used as a script or run through polyc to generate a stand-alone executable? If so, you're going to have a problem with the #! line because it is only treated specially if --script is given. If you try to run the file through polyc it will complain about a syntax error. You should be able to discover whether you are running as a script by looking for the presence of the --script option using CommandLine.arguments(). Thanks! This was the information I was looking for. Some explanation for my use case: For debugging an application, I'd like to run it with polyc --script (not using the shebang) as this prints out intermediate datastructures. When I only need the pure output w/o interleaved compiler output, I want to use the compiled executable. @David: Have you seen my other issue in the original email? - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Kryptografische Unterschrift ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
(Ie, what I want: if is_script then main() else () ) If your main : unit - unit (which perhaps it must be?), then main() is equivalent to the if expression above, modulo side-effects. Thanks, René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
Am 11.10.2013 15:12, schrieb Ramana Kumar: (Ie, what I want: if is_script then main() else () ) If your main : unit - unit (which perhaps it must be?), then main() is equivalent to the if expression above, modulo side-effects. There is a misunderstanding here: I need the main to be run with poly --script -- which does not run it by default. But if I'd include 'main ()' in the script itself, it'd be run on compiling too (which I'd like to avoid). - René Thanks, René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Kryptografische Unterschrift ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and poly --script
On 11/10/2013 14:17, René Neumann wrote: Am 11.10.2013 15:12, schrieb Ramana Kumar: (Ie, what I want: if is_script then main() else () ) If your main : unit - unit (which perhaps it must be?), then main() is equivalent to the if expression above, modulo side-effects. There is a misunderstanding here: I need the main to be run with poly --script -- which does not run it by default. But if I'd include 'main ()' in the script itself, it'd be run on compiling too (which I'd like to avoid). I'm still unclear what you're trying to achieve. Are you trying to write a single file that can either be used as a script or run through polyc to generate a stand-alone executable? If so, you're going to have a problem with the #! line because it is only treated specially if --script is given. If you try to run the file through polyc it will complain about a syntax error. You should be able to discover whether you are running as a script by looking for the presence of the --script option using CommandLine.arguments(). David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
