You’re right … in these builds, the PolyML was statically linked, so there’s no “libpolyml.so” in the result of “ldd”. This means “ldd” is completely useless for giving information about the actual library dir of polyml.
—binghe > Il giorno 03 mag 2017, alle ore 01:01, Jeremy Dawson > <jeremy.daw...@anu.edu.au> ha scritto: > > It's not a consistent solution, that command returns nothing for me, and > ldd output doesn't include libpolyml (why?) > > [jeremy@hp2016 private]$ ldd /usr/local/bin/poly > linux-vdso.so.1 (0x00007ffed5163000) > libpthread.so.0 => /lib64/libpthread.so.0 (0x00007f99a52dc000) > libgmp.so.10 => /lib64/libgmp.so.10 (0x00007f99a5048000) > libm.so.6 => /lib64/libm.so.6 (0x00007f99a4d3f000) > libdl.so.2 => /lib64/libdl.so.2 (0x00007f99a4b3b000) > libstdc++.so.6 => /lib64/libstdc++.so.6 (0x00007f99a47b2000) > libgcc_s.so.1 => /lib64/libgcc_s.so.1 (0x00007f99a459b000) > libc.so.6 => /lib64/libc.so.6 (0x00007f99a41d9000) > /lib64/ld-linux-x86-64.so.2 (0x000055f8a08ec000) > [jeremy@hp2016 private]$ ldd `which poly` | grep libpolyml > [jeremy@hp2016 private]$ > > That's on Fedora 24 > > At work, on Ubuntu 12.04 (I think), again, no libpolyml > > [jeremy@jasco ~]$ which poly > /home/users/jeremy/polyml-5.6/bin/poly > [jeremy@jasco ~]$ ldd /home/users/jeremy/polyml-5.6/bin/poly > linux-vdso.so.1 => (0x00007fff71775000) > libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 > (0x00007fa5a870f000) > libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 > (0x00007fa5a84a1000) > libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fa5a81a5000) > libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fa5a7fa1000) > libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 > (0x00007fa5a7ca1000) > libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 > (0x00007fa5a7a8b000) > libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fa5a76ca000) > /lib64/ld-linux-x86-64.so.2 (0x00007fa5a892c000) > > > On 03/05/17 06:08, Chun Tian (binghe) wrote: >> Maybe this is a solution: >> >> $ ldd `which poly` | grep libpolyml >> libpolyml.so.7 => /usr/lib/x86_64-linux-gnu/libpolyml.so.7 >> (0x00007fd2a4193000) >> >> That is, call “ldd” on “poly” and filter out the line of libpolyml.so. The >> resulting full path "/usr/lib/x86_64-linux-gnu/“ will also contains >> libpolymain.a. >> >>> Il giorno 02 mag 2017, alle ore 22:04, Chun Tian (binghe) >>> <binghe.l...@gmail.com> ha scritto: >>> >>> Hi, >>> >>> I’m afraid that “ldd” command won’t give anything useful. On Ubuntu 16.04 >>> (x86_64), ldd gives the following outputs on “libpolyml.so” (the pointer >>> addresses are different in different machine): >>> >>> $ ldd /usr/lib/x86_64-linux-gnu/libpolyml.so >>> linux-vdso.so.1 => (0x00007ffcbdbf1000) >>> libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 >>> (0x00007fb1e9de1000) >>> libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 >>> (0x00007fb1e9bd9000) >>> libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb1e99d4000) >>> libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 >>> (0x00007fb1e9652000) >>> libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb1e9349000) >>> libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb1e8f7f000) >>> libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 >>> (0x00007fb1e8d69000) >>> /lib64/ld-linux-x86-64.so.2 (0x000055b8df86b000) >>> >>> Whenever paths like "/usr/lib/x86_64-linux-gnu” are part of the outputs, we >>> can safely expect that, Ubuntu's “polyml" package will also install >>> “libpolyml.so” and “libpolymain.a” into "/usr/lib/x86_64-linux-gnu”. But >>> none of linked libraries are part of PolyML itself, so if user build PolyML >>> manually and install it at somewhere, “ldd” on user-installed >>> "libpolyml.so” will output exactly the same, but this time “libpolymain.a” >>> is not in "/usr/lib/x86_64-linux-gnu” at all. >>> >>> Maybe we should ask this question instead: why HOL has to know the exact >>> position of “libpolymain.a”? I ask this because the path of “.a” files are >>> known by GCC (and “polyc”) automatically, and for ML programmars who use >>> PolyML to build their programs, there’s no need to specify the full path of >>> “libpolymain.a” at all… >>> >>> Regards, >>> >>> Chun >>> >>>> Il giorno 02 mag 2017, alle ore 21:18, michael.norr...@data61.csiro.au ha >>>> scritto: >>>> >>>> I’d certainly be happy to adjust smart-configure to be smarter. (I’d be >>>> even happier to approve a pull request.) >>>> >>>> I don’t understand the suggestion about using ldd on libpolyml.so. Do you >>>> mean to use it on the poly executable itself? (If I knew where >>>> libpolyml.so was, I’d take that to be the lib directory.) >>>> >>>> Next question: on MacOS, there isn’t an ldd, but the supposedly equivalent >>>> otool -L command doesn’t actually spit back anything useful when run on my >>>> poly executable, viz: >>>> >>>> $ otool -L `which poly` >>>> /usr/local/bin/poly: >>>> /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version >>>> 120.1.0) >>>> /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current >>>> version 1226.10.1) >>>> >>>> Does ldd say more useful things on the Linux systems where this appears to >>>> be an issue? >>>> >>>> Having said all this, it’s also possible that using polyc everywhere makes >>>> it unnecessary for HOL itself to know anything about this directory. I’ll >>>> have to check this. >>>> >>>> Michael >>>> >>>> On 2/5/17, 20:01, "Ian Zimmerman" <i...@primate.net> wrote: >>>> >>>> On 2017-05-02 18:31, Chun Tian (binghe) wrote: >>>> >>>>> $ poly < tools/smart-configure.sml >>>>> Poly/ML 5.6 Release >>>>> >>>>> HOL smart configuration. >>>>> >>>>> Determining configuration parameters: holdir OS poly polymllibdir >>>>> >>>>> Looked in poly's sister lib directory /usr/lib >>>>> and couldn't find libpolymain.a >>>>> Please write file tools-poly/poly-includes.ML to specify it. >>>>> This file should include a line of the form >>>>> >>>>> val polymllibdir = "path-to-dir-containing-libpolymain.a"; >>>> >>>> Oh, now I see: >>>> >>>> [1+0]~$ ls -l /usr >>>> total 228 >>>> drwxr-xr-x 3 root root 81920 May 1 19:12 bin >>>> drwxr-xr-x 3 games root 4096 Jun 23 2016 games >>>> drwxr-xr-x 219 root root 20480 May 1 10:52 include >>>> lrwxrwxrwx 1 root root 5 Jun 15 2016 lib -> lib64 >>>> drwxr-xr-x 5 root root 4096 Feb 11 23:11 lib32 >>>> drwxr-xr-x 109 root root 86016 May 1 10:48 lib64 >>>> drwxr-xr-x 11 root root 4096 Apr 25 16:02 libexec >>>> drwxr-xr-x 7 root root 4096 Mar 15 21:41 local >>>> drwxr-xr-x 3 root root 4096 Jun 23 2016 man >>>> lrwxrwxrwx 1 root root 22 Oct 26 2016 portage -> >>>> /var/lib/portage/ports >>>> drwxr-xr-x 2 root root 4096 Apr 25 14:52 sbin >>>> drwxr-xr-x 175 root root 4096 May 1 10:52 share >>>> drwxr-xr-x 5 root root 4096 Apr 30 17:36 src >>>> lrwxrwxrwx 1 root root 8 Jun 15 2016 tmp -> /var/tmp >>>> drwxr-xr-x 6 root root 4096 Jun 15 2016 x86_64-pc-linux-gnu >>>> >>>> So, you were mostly right, HOL install does incorrectly assume /usr/lib >>>> (after finding poly in /usr/bin). >>>> >>>> Maybe smart-configure ought to first resolve libpolyml.so with ldd or so >>>> and look for libpolymain.a in that directory, rather than playing >>>> not-so-smart string substitution games. >>>> >>>> -- >>>> Please *no* private Cc: on mailing lists and newsgroups >>>> Personal signed mail: please _encrypt_ and sign >>>> Don't clear-text sign: >>>> http://primate.net/~itz/blog/the-problem-with-gpg-signatures.html >>>> >>>> >>>> ------------------------------------------------------------------------------ >>>> Check out the vibrant tech community on one of the world's most >>>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >>>> _______________________________________________ >>>> hol-info mailing list >>>> hol-info@lists.sourceforge.net >>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>>> >>>> >>>> ------------------------------------------------------------------------------ >>>> Check out the vibrant tech community on one of the world's most >>>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >>>> _______________________________________________ >>>> hol-info mailing list >>>> hol-info@lists.sourceforge.net >>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>> >> >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> >> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
