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
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
