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