On 2017-05-02 15:55, Chun Tian (binghe) wrote: > I forgot one thing: In modern Linux systems, to support installing > 32-bit and 64-bit runtimes together, many package’s library files have > been moved from “/usr/lib” to “/usr/lib/x86_64-linux-gnu”. But HOL’s > building scripts do not recognize “/usr/lib/x86_64-linux-gnu” when > searching for “libpolymain.a”. > > To correctly use system “polyml” for building HOL4, a symbolic link > from “/usr/lib/x86_64-linux-gnu/libpolymain.a” to > “/usr/lib/libpolymain.a” must be made manually. One way is to stand in > “/usr/lib” with root access, and execute the following command: > > ln -s x86_64-linux-gnu/libpolymain.a .
I do not think this is entirely accurate. On my Gentoo amd64 system, libpolymain.a is in /usr/lib64/ HOL builds without problems, no symlink needed. What is the output of the tools/smart-configure phase? -- 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
