Well, as I said, I think it’s quite possible that we don’t need to know this
any more. Before polyc was provided, we needed to provide explicit -L paths so
that the linker could look in the right places when building executables like
Holmake. All this is now handled by polyc I think.
In the meantime, I think it should be easy enough to follow the script’s
instructions and specify the path to the file in the overrides file.
Michael
On 2/5/17, 22:04, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
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
