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
