Closed SnarkBoojum closed 2 years ago
To update alt-ergo in Debian, I need to package psmt2-frontend.
I prepared a preliminary package which looks quite sane, with a compilation:
dune build @all dune install --destir=$(CURDIR)/debian/tmp --prefix=/usr --libdir=/usr/lib/ocaml
so far so good. But at the first try with alt-ergo:
/usr/bin/ld: /usr/lib/ocaml/psmt2-frontend/psmt2Frontend.a: error adding symbols: archive has no index; run ranlib to add one
and if I run ranlib by hand, things don't get better:
(cd _build/default && /usr/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -o src/bin/text/Main_text.exe /usr/lib/ocaml/unix.cmxa -I /usr/lib/ocaml /usr/lib/ocaml/nums.cmxa -I /usr/lib/ocaml /usr/lib/ocam l/str.cmxa -I /usr/lib/ocaml /usr/lib/ocaml/zarith/zarith.cmxa -I /usr/lib/ocaml/zarith /usr/lib/ocaml/dynlink.cmxa -I /usr/lib/ocaml /usr/lib/ocaml/ocplib-simplex/ocplibSimplex.cmxa src/lib/AltErgoLib.cmxa /usr /lib/ocaml/zip/zip.cmxa -I /usr/lib/ocaml/zip /usr/lib/ocaml/psmt2-frontend/psmt2Frontend.cmxa src/parsers/AltErgoParsers.cmxa /usr/lib/ocaml/cmdliner/cmdliner.cmxa src/bin/common/alt_ergo_common.cmxa src/bin/te xt/.Main_text.eobjs/native/dune__exe__Main_text.cmx -linkall) /usr/bin/ld: /tmp/builde7c0fe.dune/camlstartupb91ac9.o: in function `caml_program': :(.text+0xda5): undefined reference to `camlPsmt2Frontend__entry' /usr/bin/ld: :(.text+0xdb5): undefined reference to `camlPsmt2Frontend__Version__entry' /usr/bin/ld: :(.text+0xdc5): undefined reference to `camlPsmt2Frontend__Options__entry' /usr/bin/ld: :(.text+0xdd5): undefined reference to `camlPsmt2Frontend__Smtlib_error__entry' /usr/bin/ld: :(.text+0xde5): undefined reference to `camlPsmt2Frontend__Smtlib_ty__entry' /usr/bin/ld: :(.text+0xdf5): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__entry' /usr/bin/ld: :(.text+0xe05): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__entry' /usr/bin/ld: :(.text+0xe15): undefined reference to `camlPsmt2Frontend__Smtlib_printer__entry' /usr/bin/ld: :(.text+0xe25): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__entry' /usr/bin/ld: :(.text+0xe35): undefined reference to `camlPsmt2Frontend__Smtlib_typing__entry' /usr/bin/ld: :(.text+0xe45): undefined reference to `camlPsmt2Frontend__Smtlib_parser__entry' /usr/bin/ld: :(.text+0xe55): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__entry' /usr/bin/ld: :(.text+0xe65): undefined reference to `camlPsmt2Frontend__Main__entry' /usr/bin/ld: /tmp/builde7c0fe.dune/camlstartupb91ac9.o: in function `caml_globals': :(.data+0x928): undefined reference to `camlPsmt2Frontend__gc_roots' /usr/bin/ld: :(.data+0x930): undefined reference to `camlPsmt2Frontend__Version__gc_roots' /usr/bin/ld: :(.data+0x938): undefined reference to `camlPsmt2Frontend__Options__gc_roots' /usr/bin/ld: :(.data+0x940): undefined reference to `camlPsmt2Frontend__Smtlib_error__gc_roots' /usr/bin/ld: :(.data+0x948): undefined reference to `camlPsmt2Frontend__Smtlib_ty__gc_roots' /usr/bin/ld: :(.data+0x950): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__gc_roots' /usr/bin/ld: :(.data+0x958): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__gc_roots' /usr/bin/ld: :(.data+0x960): undefined reference to `camlPsmt2Frontend__Smtlib_printer__gc_roots' /usr/bin/ld: :(.data+0x968): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__gc_roots' /usr/bin/ld: :(.data+0x970): undefined reference to `camlPsmt2Frontend__Smtlib_typing__gc_roots' /usr/bin/ld: :(.data+0x978): undefined reference to `camlPsmt2Frontend__Smtlib_parser__gc_roots' /usr/bin/ld: :(.data+0x980): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__gc_roots' /usr/bin/ld: :(.data+0x988): undefined reference to `camlPsmt2Frontend__Main__gc_roots' /usr/bin/ld: /tmp/builde7c0fe.dune/camlstartupb91ac9.o: in function `caml_data_segments': :(.data+0x4e30): undefined reference to `camlPsmt2Frontend__data_begin' /usr/bin/ld: :(.data+0x4e38): undefined reference to `camlPsmt2Frontend__data_end' /usr/bin/ld: :(.data+0x4e40): undefined reference to `camlPsmt2Frontend__Version__data_begin' /usr/bin/ld: :(.data+0x4e48): undefined reference to `camlPsmt2Frontend__Version__data_end' /usr/bin/ld: :(.data+0x4e50): undefined reference to `camlPsmt2Frontend__Options__data_begin' /usr/bin/ld: :(.data+0x4e58): undefined reference to `camlPsmt2Frontend__Options__data_end' /usr/bin/ld: :(.data+0x4e60): undefined reference to `camlPsmt2Frontend__Smtlib_error__data_begin' /usr/bin/ld: :(.data+0x4e68): undefined reference to `camlPsmt2Frontend__Smtlib_error__data_end' /usr/bin/ld: :(.data+0x4e70): undefined reference to `camlPsmt2Frontend__Smtlib_ty__data_begin' /usr/bin/ld: :(.data+0x4e78): undefined reference to `camlPsmt2Frontend__Smtlib_ty__data_end' /usr/bin/ld: :(.data+0x4e80): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__data_begin' /usr/bin/ld: :(.data+0x4e88): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__data_end' /usr/bin/ld: :(.data+0x4e90): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__data_begin' /usr/bin/ld: :(.data+0x4e98): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__data_end' /usr/bin/ld: :(.data+0x4ea0): undefined reference to `camlPsmt2Frontend__Smtlib_printer__data_begin' /usr/bin/ld: :(.data+0x4ea8): undefined reference to `camlPsmt2Frontend__Smtlib_printer__data_end' /usr/bin/ld: :(.data+0x4eb0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__data_begin' /usr/bin/ld: :(.data+0x4eb8): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__data_end' /usr/bin/ld: :(.data+0x4ec0): undefined reference to `camlPsmt2Frontend__Smtlib_typing__data_begin' /usr/bin/ld: :(.data+0x4ec8): undefined reference to `camlPsmt2Frontend__Smtlib_typing__data_end' /usr/bin/ld: :(.data+0x4ed0): undefined reference to `camlPsmt2Frontend__Smtlib_parser__data_begin' /usr/bin/ld: :(.data+0x4ed8): undefined reference to `camlPsmt2Frontend__Smtlib_parser__data_end' /usr/bin/ld: :(.data+0x4ee0): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__data_begin' /usr/bin/ld: :(.data+0x4ee8): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__data_end' /usr/bin/ld: :(.data+0x4ef0): undefined reference to `camlPsmt2Frontend__Main__data_begin' /usr/bin/ld: :(.data+0x4ef8): undefined reference to `camlPsmt2Frontend__Main__data_end' /usr/bin/ld: /tmp/builde7c0fe.dune/camlstartupb91ac9.o: in function `caml_code_segments': :(.data+0x5e48): undefined reference to `camlPsmt2Frontend__code_begin' /usr/bin/ld: :(.data+0x5e50): undefined reference to `camlPsmt2Frontend__code_end' /usr/bin/ld: :(.data+0x5e58): undefined reference to `camlPsmt2Frontend__Version__code_begin' /usr/bin/ld: :(.data+0x5e60): undefined reference to `camlPsmt2Frontend__Version__code_end' /usr/bin/ld: :(.data+0x5e68): undefined reference to `camlPsmt2Frontend__Options__code_begin' /usr/bin/ld: :(.data+0x5e70): undefined reference to `camlPsmt2Frontend__Options__code_end' /usr/bin/ld: :(.data+0x5e78): undefined reference to `camlPsmt2Frontend__Smtlib_error__code_begin' /usr/bin/ld: :(.data+0x5e80): undefined reference to `camlPsmt2Frontend__Smtlib_error__code_end' /usr/bin/ld: :(.data+0x5e88): undefined reference to `camlPsmt2Frontend__Smtlib_ty__code_begin' /usr/bin/ld: :(.data+0x5e90): undefined reference to `camlPsmt2Frontend__Smtlib_ty__code_end' /usr/bin/ld: :(.data+0x5e98): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__code_begin' /usr/bin/ld: :(.data+0x5ea0): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__code_end' /usr/bin/ld: :(.data+0x5ea8): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__code_begin' /usr/bin/ld: :(.data+0x5eb0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__code_end' /usr/bin/ld: :(.data+0x5eb8): undefined reference to `camlPsmt2Frontend__Smtlib_printer__code_begin' /usr/bin/ld: :(.data+0x5ec0): undefined reference to `camlPsmt2Frontend__Smtlib_printer__code_end' /usr/bin/ld: :(.data+0x5ec8): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__code_begin' /usr/bin/ld: :(.data+0x5ed0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__code_end' /usr/bin/ld: :(.data+0x5ed8): undefined reference to `camlPsmt2Frontend__Smtlib_typing__code_begin' /usr/bin/ld: :(.data+0x5ee0): undefined reference to `camlPsmt2Frontend__Smtlib_typing__code_end' /usr/bin/ld: :(.data+0x5ee8): undefined reference to `camlPsmt2Frontend__Smtlib_parser__code_begin' /usr/bin/ld: :(.data+0x5ef0): undefined reference to `camlPsmt2Frontend__Smtlib_parser__code_end' /usr/bin/ld: :(.data+0x5ef8): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__code_begin' /usr/bin/ld: :(.data+0x5f00): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__code_end' /usr/bin/ld: :(.data+0x5f08): undefined reference to `camlPsmt2Frontend__Main__code_begin' /usr/bin/ld: :(.data+0x5f10): undefined reference to `camlPsmt2Frontend__Main__code_end' /usr/bin/ld: /tmp/builde7c0fe.dune/camlstartupb91ac9.o: in function `caml_frametable': :(.data+0x6790): undefined reference to `camlPsmt2Frontend__frametable' /usr/bin/ld: :(.data+0x6798): undefined reference to `camlPsmt2Frontend__Version__frametable' /usr/bin/ld: :(.data+0x67a0): undefined reference to `camlPsmt2Frontend__Options__frametable' /usr/bin/ld: :(.data+0x67a8): undefined reference to `camlPsmt2Frontend__Smtlib_error__frametable' /usr/bin/ld: :(.data+0x67b0): undefined reference to `camlPsmt2Frontend__Smtlib_ty__frametable' /usr/bin/ld: :(.data+0x67b8): undefined reference to `camlPsmt2Frontend__Smtlib_syntax__frametable' /usr/bin/ld: :(.data+0x67c0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env__frametable' /usr/bin/ld: :(.data+0x67c8): undefined reference to `camlPsmt2Frontend__Smtlib_printer__frametable' /usr/bin/ld: :(.data+0x67d0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_logic__frametable' /usr/bin/ld: :(.data+0x67d8): undefined reference to `camlPsmt2Frontend__Smtlib_typing__frametable' /usr/bin/ld: :(.data+0x67e0): undefined reference to `camlPsmt2Frontend__Smtlib_parser__frametable' /usr/bin/ld: :(.data+0x67e8): undefined reference to `camlPsmt2Frontend__Smtlib_lexer__frametable' /usr/bin/ld: :(.data+0x67f0): undefined reference to `camlPsmt2Frontend__Main__frametable' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__aux_1107': :(.text+0x58c): undefined reference to `camlPsmt2Frontend__Smtlib_ty' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__translate_constant_1208': :(.text+0xb76): undefined reference to `camlPsmt2Frontend__Smtlib_ty' /usr/bin/ld: :(.text+0xbd7): undefined reference to `camlPsmt2Frontend__Smtlib_ty' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__translate_string_identifier_1232': :(.text+0x14d9): undefined reference to `camlPsmt2Frontend__Smtlib_ty' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__translate_identifier_1256': :(.text+0x16d0): undefined reference to `camlPsmt2Frontend__Smtlib_typed_env' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__translate_fun_def_1658': :(.text+0x2504): undefined reference to `camlPsmt2Frontend__Smtlib_ty' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__init_1744': :(.text+0x32f7): undefined reference to `camlPsmt2Frontend__Options' /usr/bin/ld: :(.text+0x36c7): undefined reference to `camlPsmt2Frontend__Options' /usr/bin/ld: :(.text+0x36f5): undefined reference to `camlPsmt2Frontend__Options' /usr/bin/ld: :(.text+0x373f): undefined reference to `camlPsmt2Frontend__Smtlib_error' /usr/bin/ld: :(.text+0x378a): undefined reference to `camlPsmt2Frontend__Smtlib_error' /usr/bin/ld: :(.text+0x3803): undefined reference to `camlPsmt2Frontend__Smtlib_parser' /usr/bin/ld: :(.text+0x3896): undefined reference to `camlPsmt2Frontend__Smtlib_error' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__file_parser_1874': :(.text+0x3937): undefined reference to `camlPsmt2Frontend__Smtlib_parser' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__lexpr_parser_1880': :(.text+0x3957): undefined reference to `camlPsmt2Frontend__Smtlib_parser' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__trigger_parser_1884': :(.text+0x39b2): undefined reference to `camlPsmt2Frontend__Smtlib_parser' /usr/bin/ld: src/parsers/AltErgoParsers.a(altErgoParsers__Psmt2_to_alt_ergo.o): in function `camlAltErgoParsers__Psmt2_to_alt_ergo__entry': :(.text+0x3ec1): undefined reference to `camlPsmt2Frontend__Smtlib_lexer' collect2: error: ld returned 1 exit status File "caml_startup", line 1: Error: Error during linking (exit code 1)
so there's definitely something very wrong. This is with dune 2.9.1.
The something wrong was some other piece coming after the install and clearing all symbols... no real problem from dune, sorry for the noise!
To update alt-ergo in Debian, I need to package psmt2-frontend.
I prepared a preliminary package which looks quite sane, with a compilation:
so far so good. But at the first try with alt-ergo:
and if I run ranlib by hand, things don't get better:
so there's definitely something very wrong. This is with dune 2.9.1.