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
