Stream: Coq devs & plugin devs

Topic: zarith


view this post on Zulip Jason Gross (Sep 23 2020 at 16:30):

Trying to backport zarith 1.10 to precise, I get

ocamlc -I +compiler-libs -bin-annot  -c big_int_Z.ml
ocamlmklib -failsafe -o zarith z.cmo q.cmo big_int_Z.cmo -Wl,-Bsymbolic-functions -Wl,-z,relro -lgmp
Unknown option -Wl,-Bsymbolic-functions
Unknown option -Wl,-z,relro
gcc -DZ_OCAML_LEGACY_CUSTOM_OPERATIONS -DZ_OCAML_HASH -DZ_OCAML_COMPARE_EXT -DHAS_GMP -DZ_ELF -DZ_DOT_LABEL_PREFIX   -D_FORTIFY_SOURCE=2  -c -o caml_z_x86_64.o caml_z_x86_64.S
ocamlc -ccopt "-I/usr/lib/ocaml -D_FORTIFY_SOURCE=2 -DZ_OCAML_LEGACY_CUSTOM_OPERATIONS -DZ_OCAML_HASH -DZ_OCAML_COMPARE_EXT -DHAS_GMP -DZ_ELF -DZ_DOT_LABEL_PREFIX  -O3 -Wall -Wextra -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Werror=format-security" -c caml_z.c
caml_z.c: In function ‘ml_z_fac2’:
caml_z.c:2987:3: warning: implicit declaration of function ‘mpz_2fac_ui’ [-Wimplicit-function-declaration]
caml_z.c: In function ‘ml_z_facM’:
caml_z.c:3002:3: warning: implicit declaration of function ‘mpz_mfac_uiui’ [-Wimplicit-function-declaration]
caml_z.c: In function ‘ml_z_primorial’:
caml_z.c:3017:3: warning: implicit declaration of function ‘mpz_primorial_ui’ [-Wimplicit-function-declaration]
ocamlmklib -failsafe -o zarith caml_z_x86_64.o caml_z.o -Wl,-Bsymbolic-functions -Wl,-z,relro -lgmp
Unknown option -Wl,-Bsymbolic-functions
Unknown option -Wl,-z,relro
ocamlc -I +compiler-libs -bin-annot  -c zarith_top.ml
ocamlc -o zarith_top.cma -a zarith_top.cmo
ocamlopt -I +compiler-libs  -c z.ml
ocamlopt -I +compiler-libs  -c q.ml
ocamlopt -I +compiler-libs  -c big_int_Z.ml
ocamlmklib -failsafe -o zarith z.cmx q.cmx big_int_Z.cmx -Wl,-Bsymbolic-functions -Wl,-z,relro -lgmp
Unknown option -Wl,-Bsymbolic-functions
Unknown option -Wl,-z,relro
ocamlopt -shared -o zarith.cmxs -I . zarith.cmxa -linkall
make[1]: Leaving directory `/<<PKGBUILDDIR>>'
   debian/rules override_dh_auto_test
make[1]: Entering directory `/<<PKGBUILDDIR>>'
/usr/bin/make tests
make[2]: Entering directory `/<<PKGBUILDDIR>>'
make -C tests test
make[3]: Entering directory `/<<PKGBUILDDIR>>/tests'
ocamlopt -I .. -ccopt "-L.." zarith.cmxa nums.cmxa -o zq.exe zq.ml
../libzarith.a(caml_z.o): In function `ml_z_fac2':
/<<PKGBUILDDIR>>/caml_z.c:2987: undefined reference to `mpz_2fac_ui'
../libzarith.a(caml_z.o): In function `ml_z_facM':
/<<PKGBUILDDIR>>/caml_z.c:3002: undefined reference to `mpz_mfac_uiui'
../libzarith.a(caml_z.o): In function `ml_z_primorial':
/<<PKGBUILDDIR>>/caml_z.c:3017: undefined reference to `mpz_primorial_ui'
collect2: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
make[3]: *** [zq.exe] Error 2
make[3]: Leaving directory `/<<PKGBUILDDIR>>/tests'
make[2]: *** [tests] Error 2
make[2]: Leaving directory `/<<PKGBUILDDIR>>'
make[1]: *** [override_dh_auto_test] Error 2
make[1]: Leaving directory `/<<PKGBUILDDIR>>'
make: *** [build] Error 2
dpkg-buildpackage: error: debian/rules build gave error exit status 2

Any ideas?
(https://launchpadlibrarian.net/498698829/buildlog_ubuntu-precise-amd64.ocaml-zarith_1.10-1.1~precise~ppa10_BUILDING.txt.gz)

view this post on Zulip Enrico Tassi (Sep 23 2020 at 17:16):

It looks like the C library you link against lacks 3 symbols (see the warnings about implicit function declaration). I don't know gmp, sorry

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2020 at 12:39):

@Jason Gross precise doesn't even appear in packages.ubuntu.com anymore, so it is too hard for me to debug. Any reason you are sticking to precise? It could be time to move to more recent distro, precise is shipping software 9 years old.

view this post on Zulip Jason Gross (Sep 24 2020 at 23:08):

Indeed, I guess the thing to do is to stop building packages for precise.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2020 at 23:47):

Well the problem here seems that gmp is too old, so indeed backporting gmp too may be challenging


Last updated: Oct 16 2021 at 01:03 UTC