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
