In a recent development version (commit 38d36b51a) doing “make” in the
directory “Manual” fails. I traced the error to a failure to build
polyscripter. Here is what appears in Manual/Tools/.hollogs/polyscripter:
“““
---------------------------------------------------------------------
HOL-4 [Kananaskis 11 (stdknl, built Tue Dec 19 11:34:27 2017)]
For introductory HOL help, type: help "hol";
To exit type <Control>-D
---------------------------------------------------------------------
[extending loadPath with Holmakefile INCLUDES variable]
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`add_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int)':
arb.cpp:(.text+0x181): undefined reference to `__gmpn_add_n'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`sub_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int)':
arb.cpp:(.text+0x2d8): undefined reference to `__gmpn_sub_n'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`quotRem(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*&,
SaveVecEntry*&)':
arb.cpp:(.text+0xbf1): undefined reference to `__gmpn_tdiv_qr'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*)':
arb.cpp:(.text+0xf2c): undefined reference to `__gmpn_gcd_1'
arb.cpp:(.text+0x102e): undefined reference to `__gmpn_rshift'
arb.cpp:(.text+0x10d3): undefined reference to `__gmpn_rshift'
arb.cpp:(.text+0x1153): undefined reference to `__gmpn_gcd'
arb.cpp:(.text+0x1175): undefined reference to `__gmpn_lshift'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`mult_longc(TaskData*, SaveVecEntry*, SaveVecEntry*)':
arb.cpp:(.text+0x1964): undefined reference to `__gmpn_mul'
collect2: error: ld returned 1 exit status
”””
I am using Debian 9 with Poly/ML 5.7.1 built from source and installed
using GNU Stow. The error message appears to indicate that libGMP is not
being found. However, compiling HOL (“bin/build -j 2”) works without
such problems. libGMP has been installed using the package manager; the
shared objects and static library are under
“/usr/lib/x86_64-linux-gnu/”, which is the standard location for Debian.
It appears that “ld” is called somewhere (I can not figure where) and it
is missing the command line option “-lgmp”.
What can I do to make it work?
Thanks.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
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
