Comment author: @nojb

Hello, thanks for the report.

It would be useful if you could run the command ocamlopt -ccopt -static ... with 4.05 and 4.06 adding the flag -verbose, which will show us a trace of the linking command used and any passed flags.

A small reproduction case would also be useful if you can produce one.

Comment author: korovin

Thanks for quick reply.

The project is in

http://www.cs.man.ac.uk/~korovink/iprover/iprover_2017_Dec_22_7h.tar.gz

To compile:

./configure
make STATIC=true

--
I'm not sure if it is relevant but it uses ocamlgraph-1.8.8

Sorry I don't have a small example at hand.

Output for 4.06:

ocamlopt -ccopt -static obj/aiger.o obj/aigLoad.o obj/solver.o obj/solver_interface.o -o iproveropt
-cclib -Lutil/objsize-stub objsize.cmxa
-verbose -w @6+5+7+44+45 -inline 10 -I obj/ -I util/lib -I ocamlgraph/ -I util/objsize-stub unix.cmxa str.cmxa util/lib/minisat.cmxa ./ocamlgraph/graph.cmxa obj/lib.cmx obj/ref_cnt.cmx obj/hashcons.cmx obj/union_find.cmx obj/options.cmx obj/statistics.cmx obj/signals.cmx obj/bit_vec.cmx obj/assignMap.cmx obj/tableArray.cmx obj/heap.cmx obj/priority_queue.cmx obj/priority_queues.cmx obj/tree.cmx obj/trie.cmx obj/trie_func.cmx obj/vectorIndex.cmx obj/abstDB.cmx obj/abstAssignDB.cmx obj/symbol.cmx obj/symbolDB.cmx obj/var.cmx obj/term.cmx obj/termDB.cmx obj/orderings.cmx obj/subst.cmx obj/substBound.cmx obj/dismatching.cmx obj/clause.cmx obj/systemDBs.cmx obj/important_lit.cmx obj/logic_interface.cmx obj/cone_symb.cmx obj/finiteDomain.cmx obj/parser_types.cmx obj/problem_properties.cmx obj/prop_var.cmx obj/prop_env.cmx obj/lexer_tptp.cmx obj/lexer_fof.cmx obj/parser_tptp.cmx obj/instantiation_env.cmx obj/aigCommon.cmx obj/aigLoader.cmx obj/aigWitness.cmx obj/aigOptimiser.cmx obj/bmc1Common.cmx obj/aigClausifier.cmx obj/parseFiles.cmx obj/aigSaver.cmx obj/definitions.cmx obj/splitting_grd.cmx obj/splitting_nvd.cmx obj/splitting_cvd.cmx obj/splitting.cmx obj/prep_unary_pred.cmx obj/unif.cmx obj/unifIndex.cmx obj/discrTree.cmx obj/discrTree_func.cmx obj/unifIndexMap.cmx obj/unifIndexDiscrTree.cmx obj/unifIndexDebug.cmx obj/subsetSubsume.cmx obj/subsumptionIndex.cmx obj/eq_axioms.cmx obj/cMinisat.cmx obj/propSolver.cmx obj/unsatCore.cmx obj/prop_solver_exchange.cmx obj/symbol_reach.cmx obj/type_inf.cmx obj/prep_sem_filter.cmx obj/prep_sem_filter_unif.cmx obj/inference_rules.cmx obj/simplify.cmx obj/predElim.cmx obj/passiveQueues.cmx obj/clauseUnifIndex.cmx obj/tstpProof.cmx obj/resolution_env.cmx obj/resolution_sel.cmx obj/resolution_loop.cmx obj/bin_hyper_res.cmx obj/preprocess.cmx obj/instantiation_sel.cmx obj/instantiation_loop.cmx obj/lemma_lifting.cmx obj/bmc1Equal.cmx obj/bmc1Axioms.cmx obj/bmc1Deadlock.cmx obj/bmc1InitTarget.cmx obj/bmc1SplitPredicate.cmx obj/model_inst.cmx obj/model_res.cmx obj/bmc1Witness.cmx obj/finite_models.cmx obj/proof_search_loop.cmx obj/abstr_ref_arg_filter.cmx obj/axiom_selection.cmx obj/finite_models_loop.cmx obj/proof_search_schedule.cmx obj/bmc1_loop.cmx obj/git_info.cmx obj/qbf_env.cmx obj/qbf_preprocess.cmx obj/qbf_fof.cmx obj/iprover.cmx

• as -o '/tmp/camlstartup5302e0.o' '/tmp/camlstartup64abb6.s'
• gcc -std=gnu99 -O2 -fno-strict-aliasing -fwrapv -fno-builtin-memcmp -Wall -fno-tree-vrp -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE -Wl,-E -o 'iproveropt' '-Lobj/' '-Lutil/lib' '-Locamlgraph/' '-Lutil/objsize-stub' '-L/shareddata/home/korovin/.opam/4.06.0/lib/ocaml' -static '/tmp/camlstartup5302e0.o' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/std_exit.o' 'obj/iprover.o' 'obj/qbf_fof.o' 'obj/qbf_preprocess.o' 'obj/qbf_env.o' 'obj/git_info.o' 'obj/bmc1_loop.o' 'obj/proof_search_schedule.o' 'obj/finite_models_loop.o' 'obj/axiom_selection.o' 'obj/abstr_ref_arg_filter.o' 'obj/proof_search_loop.o' 'obj/finite_models.o' 'obj/bmc1Witness.o' 'obj/model_res.o' 'obj/model_inst.o' 'obj/bmc1SplitPredicate.o' 'obj/bmc1InitTarget.o' 'obj/bmc1Deadlock.o' 'obj/bmc1Axioms.o' 'obj/bmc1Equal.o' 'obj/lemma_lifting.o' 'obj/instantiation_loop.o' 'obj/instantiation_sel.o' 'obj/preprocess.o' 'obj/bin_hyper_res.o' 'obj/resolution_loop.o' 'obj/resolution_sel.o' 'obj/resolution_env.o' 'obj/tstpProof.o' 'obj/clauseUnifIndex.o' 'obj/passiveQueues.o' 'obj/predElim.o' 'obj/simplify.o' 'obj/inference_rules.o' 'obj/prep_sem_filter_unif.o' 'obj/prep_sem_filter.o' 'obj/type_inf.o' 'obj/symbol_reach.o' 'obj/prop_solver_exchange.o' 'obj/unsatCore.o' 'obj/propSolver.o' 'obj/cMinisat.o' 'obj/eq_axioms.o' 'obj/subsumptionIndex.o' 'obj/subsetSubsume.o' 'obj/unifIndexDebug.o' 'obj/unifIndexDiscrTree.o' 'obj/unifIndexMap.o' 'obj/discrTree_func.o' 'obj/discrTree.o' 'obj/unifIndex.o' 'obj/unif.o' 'obj/prep_unary_pred.o' 'obj/splitting.o' 'obj/splitting_cvd.o' 'obj/splitting_nvd.o' 'obj/splitting_grd.o' 'obj/definitions.o' 'obj/aigSaver.o' 'obj/parseFiles.o' 'obj/aigClausifier.o' 'obj/bmc1Common.o' 'obj/aigOptimiser.o' 'obj/aigWitness.o' 'obj/aigLoader.o' 'obj/aigCommon.o' 'obj/instantiation_env.o' 'obj/parser_tptp.o' 'obj/lexer_fof.o' 'obj/lexer_tptp.o' 'obj/prop_env.o' 'obj/prop_var.o' 'obj/problem_properties.o' 'obj/parser_types.o' 'obj/finiteDomain.o' 'obj/cone_symb.o' 'obj/logic_interface.o' 'obj/important_lit.o' 'obj/systemDBs.o' 'obj/clause.o' 'obj/dismatching.o' 'obj/substBound.o' 'obj/subst.o' 'obj/orderings.o' 'obj/termDB.o' 'obj/term.o' 'obj/var.o' 'obj/symbolDB.o' 'obj/symbol.o' 'obj/abstAssignDB.o' 'obj/abstDB.o' 'obj/vectorIndex.o' 'obj/trie_func.o' 'obj/trie.o' 'obj/tree.o' 'obj/priority_queues.o' 'obj/priority_queue.o' 'obj/heap.o' 'obj/tableArray.o' 'obj/assignMap.o' 'obj/bit_vec.o' 'obj/signals.o' 'obj/statistics.o' 'obj/options.o' 'obj/union_find.o' 'obj/hashcons.o' 'obj/ref_cnt.o' 'obj/lib.o' './ocamlgraph/graph.a' 'util/lib/minisat.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/str.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/unix.a' 'util/objsize-stub/objsize.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/stdlib.a' '-L/shareddata/home/korovin/iprover-local/util/lib' '-L/shareddata/home/korovin/iprover-local/util/minisat/simp' '-lminisat_stubs' '-lminisat' '-lstdc++' '-lcamlstr' '-lunix' '-lobjsize' 'obj/aiger.o' 'obj/aigLoad.o' 'obj/solver.o' 'obj/solver_interface.o' '-Lutil/objsize-stub' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a' -lm -ldl
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a(unix.o): In function caml_dlopen': /shareddata/home/korovin/.opam/4.06.0/build/ocaml/asmrun/unix.c:273: warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(initgroups.o): In function unix_initgroups':
  initgroups.c:(.text+0x1f): warning: Using 'initgroups' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrgid': getgr.c:(.text+0x128): warning: Using 'getgrgid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrnam':
  getgr.c:(.text+0x101): warning: Using 'getgrnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwnam': getpw.c:(.text+0x151): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwuid':
  getpw.c:(.text+0x178): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getaddrinfo.o): In function unix_getaddrinfo': getaddrinfo.c:(.text+0x224): warning: Using 'getaddrinfo' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyaddr':
  gethost.c:(.text+0x209): warning: Using 'gethostbyaddr_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyname': gethost.c:(.text+0x2b9): warning: Using 'gethostbyname_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobynumber':
  getproto.c:(.text+0xe8): warning: Using 'getprotobynumber' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobyname': getproto.c:(.text+0xc1): warning: Using 'getprotobyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getserv.o): In function unix_getservbyname':
  getserv.c:(.text+0x108): warning: Using 'getservbyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getserv.o): In function unix_getservbyport': getserv.c:(.text+0x159): warning: Using 'getservbyport' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/bin/ld: dynamic STT_GNU_IFUNC symbol floor' with pointer equality in `/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/libm.a(s_floor.o)' cannot be used when making an executable; recompile with -fPIE and relink with -pie
  collect2: error: ld returned 1 exit status
  File "caml_startup", line 1:
  Error: Error during linking
  make: *** [iproveropt] Error 2

============
output for 4.05:

ocamlopt -ccopt -static obj/aiger.o obj/aigLoad.o obj/solver.o obj/solver_interface.o -o iproveropt
-cclib -Lutil/objsize-stub objsize.cmxa
-verbose -w @6+5+7+44+45 -inline 10 -I obj/ -I util/lib -I ocamlgraph/ -I util/objsize-stub unix.cmxa str.cmxa util/lib/minisat.cmxa ./ocamlgraph/graph.cmxa obj/lib.cmx obj/ref_cnt.cmx obj/hashcons.cmx obj/union_find.cmx obj/options.cmx obj/statistics.cmx obj/signals.cmx obj/bit_vec.cmx obj/assignMap.cmx obj/tableArray.cmx obj/heap.cmx obj/priority_queue.cmx obj/priority_queues.cmx obj/tree.cmx obj/trie.cmx obj/trie_func.cmx obj/vectorIndex.cmx obj/abstDB.cmx obj/abstAssignDB.cmx obj/symbol.cmx obj/symbolDB.cmx obj/var.cmx obj/term.cmx obj/termDB.cmx obj/orderings.cmx obj/subst.cmx obj/substBound.cmx obj/dismatching.cmx obj/clause.cmx obj/systemDBs.cmx obj/important_lit.cmx obj/logic_interface.cmx obj/cone_symb.cmx obj/finiteDomain.cmx obj/parser_types.cmx obj/problem_properties.cmx obj/prop_var.cmx obj/prop_env.cmx obj/lexer_tptp.cmx obj/lexer_fof.cmx obj/parser_tptp.cmx obj/instantiation_env.cmx obj/aigCommon.cmx obj/aigLoader.cmx obj/aigWitness.cmx obj/aigOptimiser.cmx obj/bmc1Common.cmx obj/aigClausifier.cmx obj/parseFiles.cmx obj/aigSaver.cmx obj/definitions.cmx obj/splitting_grd.cmx obj/splitting_nvd.cmx obj/splitting_cvd.cmx obj/splitting.cmx obj/prep_unary_pred.cmx obj/unif.cmx obj/unifIndex.cmx obj/discrTree.cmx obj/discrTree_func.cmx obj/unifIndexMap.cmx obj/unifIndexDiscrTree.cmx obj/unifIndexDebug.cmx obj/subsetSubsume.cmx obj/subsumptionIndex.cmx obj/eq_axioms.cmx obj/cMinisat.cmx obj/propSolver.cmx obj/unsatCore.cmx obj/prop_solver_exchange.cmx obj/symbol_reach.cmx obj/type_inf.cmx obj/prep_sem_filter.cmx obj/prep_sem_filter_unif.cmx obj/inference_rules.cmx obj/simplify.cmx obj/predElim.cmx obj/passiveQueues.cmx obj/clauseUnifIndex.cmx obj/tstpProof.cmx obj/resolution_env.cmx obj/resolution_sel.cmx obj/resolution_loop.cmx obj/bin_hyper_res.cmx obj/preprocess.cmx obj/instantiation_sel.cmx obj/instantiation_loop.cmx obj/lemma_lifting.cmx obj/bmc1Equal.cmx obj/bmc1Axioms.cmx obj/bmc1Deadlock.cmx obj/bmc1InitTarget.cmx obj/bmc1SplitPredicate.cmx obj/model_inst.cmx obj/model_res.cmx obj/bmc1Witness.cmx obj/finite_models.cmx obj/proof_search_loop.cmx obj/abstr_ref_arg_filter.cmx obj/axiom_selection.cmx obj/finite_models_loop.cmx obj/proof_search_schedule.cmx obj/bmc1_loop.cmx obj/git_info.cmx obj/qbf_env.cmx obj/qbf_preprocess.cmx obj/qbf_fof.cmx obj/iprover.cmx

• as -o '/tmp/camlstartup11fd11.o' '/tmp/camlstartup7eecae.s'
• gcc -std=gnu99 -O2 -fno-strict-aliasing -fwrapv -fno-builtin-memcmp -D_FILE_OFFSET_BITS=64 -D_REENTRANT -o 'iproveropt' '-Lobj/' '-Lutil/lib' '-Locamlgraph/' '-Lutil/objsize-stub' '-L/shareddata/home/korovin/.opam/4.05.0/lib/ocaml' -static '/tmp/camlstartup11fd11.o' '/shareddata/home/korovin/.opam/4.05.0/lib/ocaml/std_exit.o' 'obj/iprover.o' 'obj/qbf_fof.o' 'obj/qbf_preprocess.o' 'obj/qbf_env.o' 'obj/git_info.o' 'obj/bmc1_loop.o' 'obj/proof_search_schedule.o' 'obj/finite_models_loop.o' 'obj/axiom_selection.o' 'obj/abstr_ref_arg_filter.o' 'obj/proof_search_loop.o' 'obj/finite_models.o' 'obj/bmc1Witness.o' 'obj/model_res.o' 'obj/model_inst.o' 'obj/bmc1SplitPredicate.o' 'obj/bmc1InitTarget.o' 'obj/bmc1Deadlock.o' 'obj/bmc1Axioms.o' 'obj/bmc1Equal.o' 'obj/lemma_lifting.o' 'obj/instantiation_loop.o' 'obj/instantiation_sel.o' 'obj/preprocess.o' 'obj/bin_hyper_res.o' 'obj/resolution_loop.o' 'obj/resolution_sel.o' 'obj/resolution_env.o' 'obj/tstpProof.o' 'obj/clauseUnifIndex.o' 'obj/passiveQueues.o' 'obj/predElim.o' 'obj/simplify.o' 'obj/inference_rules.o' 'obj/prep_sem_filter_unif.o' 'obj/prep_sem_filter.o' 'obj/type_inf.o' 'obj/symbol_reach.o' 'obj/prop_solver_exchange.o' 'obj/unsatCore.o' 'obj/propSolver.o' 'obj/cMinisat.o' 'obj/eq_axioms.o' 'obj/subsumptionIndex.o' 'obj/subsetSubsume.o' 'obj/unifIndexDebug.o' 'obj/unifIndexDiscrTree.o' 'obj/unifIndexMap.o' 'obj/discrTree_func.o' 'obj/discrTree.o' 'obj/unifIndex.o' 'obj/unif.o' 'obj/prep_unary_pred.o' 'obj/splitting.o' 'obj/splitting_cvd.o' 'obj/splitting_nvd.o' 'obj/splitting_grd.o' 'obj/definitions.o' 'obj/aigSaver.o' 'obj/parseFiles.o' 'obj/aigClausifier.o' 'obj/bmc1Common.o' 'obj/aigOptimiser.o' 'obj/aigWitness.o' 'obj/aigLoader.o' 'obj/aigCommon.o' 'obj/instantiation_env.o' 'obj/parser_tptp.o' 'obj/lexer_fof.o' 'obj/lexer_tptp.o' 'obj/prop_env.o' 'obj/prop_var.o' 'obj/problem_properties.o' 'obj/parser_types.o' 'obj/finiteDomain.o' 'obj/cone_symb.o' 'obj/logic_interface.o' 'obj/important_lit.o' 'obj/systemDBs.o' 'obj/clause.o' 'obj/dismatching.o' 'obj/substBound.o' 'obj/subst.o' 'obj/orderings.o' 'obj/termDB.o' 'obj/term.o' 'obj/var.o' 'obj/symbolDB.o' 'obj/symbol.o' 'obj/abstAssignDB.o' 'obj/abstDB.o' 'obj/vectorIndex.o' 'obj/trie_func.o' 'obj/trie.o' 'obj/tree.o' 'obj/priority_queues.o' 'obj/priority_queue.o' 'obj/heap.o' 'obj/tableArray.o' 'obj/assignMap.o' 'obj/bit_vec.o' 'obj/signals.o' 'obj/statistics.o' 'obj/options.o' 'obj/union_find.o' 'obj/hashcons.o' 'obj/ref_cnt.o' 'obj/lib.o' './ocamlgraph/graph.a' 'util/lib/minisat.a' '/shareddata/home/korovin/.opam/4.05.0/lib/ocaml/str.a' '/shareddata/home/korovin/.opam/4.05.0/lib/ocaml/unix.a' 'util/objsize-stub/objsize.a' '/shareddata/home/korovin/.opam/4.05.0/lib/ocaml/stdlib.a' '-L/shareddata/home/korovin/iprover-local/util/lib' '-L/shareddata/home/korovin/iprover-local/util/minisat/simp' '-lminisat_stubs' '-lminisat' '-lstdc++' '-lcamlstr' '-lunix' '-lobjsize' 'obj/aiger.o' 'obj/aigLoad.o' 'obj/solver.o' 'obj/solver_interface.o' '-Lutil/objsize-stub' '/shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libasmrun.a' -lm -ldl
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libasmrun.a(unix.o): In function caml_dlopen': /shareddata/home/korovin/.opam/4.05.0/build/ocaml/asmrun/unix.c:273: warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(initgroups.o): In function unix_initgroups':
  initgroups.c:(.text+0x1f): warning: Using 'initgroups' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrgid': getgr.c:(.text+0x128): warning: Using 'getgrgid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrnam':
  getgr.c:(.text+0x101): warning: Using 'getgrnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwnam': getpw.c:(.text+0x151): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwuid':
  getpw.c:(.text+0x178): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getaddrinfo.o): In function unix_getaddrinfo': getaddrinfo.c:(.text+0x224): warning: Using 'getaddrinfo' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyaddr':
  gethost.c:(.text+0x209): warning: Using 'gethostbyaddr_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyname': gethost.c:(.text+0x2b9): warning: Using 'gethostbyname_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobynumber':
  getproto.c:(.text+0xe8): warning: Using 'getprotobynumber' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobyname': getproto.c:(.text+0xc1): warning: Using 'getprotobyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getserv.o): In function unix_getservbyname':
  getserv.c:(.text+0x108): warning: Using 'getservbyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.05.0/lib/ocaml/libunix.a(getserv.o): In function `unix_getservbyport':
  getserv.c:(.text+0x159): warning: Using 'getservbyport' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

Comment author: @nojb

Diffing both traces, we see that for 4.06 we are passing -Wl,-E to the linker. Could you try adding the flag -ccopt -Wl,--no-export-dynamic to your ocamlopt invocation and see if it works?

Comment author: korovin

After including these flags (together with -static) I'm getting:

ocamlopt -ccopt -Wl,--no-export-dynamic,-static obj/aiger.o obj/aigLoad.o obj/solver.o obj/solver_interface.o -o iproveropt
-cclib -Lutil/objsize-stub objsize.cmxa
-verbose -w @6+5+7+44+45 -inline 10 -I obj/ -I util/lib -I ocamlgraph/ -I util/objsize-stub unix.cmxa str.cmxa util/lib/minisat.cmxa ./ocamlgraph/graph.cmxa obj/lib.cmx obj/ref_cnt.cmx obj/hashcons.cmx obj/union_find.cmx obj/options.cmx obj/statistics.cmx obj/signals.cmx obj/bit_vec.cmx obj/assignMap.cmx obj/tableArray.cmx obj/heap.cmx obj/priority_queue.cmx obj/priority_queues.cmx obj/tree.cmx obj/trie.cmx obj/trie_func.cmx obj/vectorIndex.cmx obj/abstDB.cmx obj/abstAssignDB.cmx obj/symbol.cmx obj/symbolDB.cmx obj/var.cmx obj/term.cmx obj/termDB.cmx obj/orderings.cmx obj/subst.cmx obj/substBound.cmx obj/dismatching.cmx obj/clause.cmx obj/systemDBs.cmx obj/important_lit.cmx obj/logic_interface.cmx obj/cone_symb.cmx obj/finiteDomain.cmx obj/parser_types.cmx obj/problem_properties.cmx obj/prop_var.cmx obj/prop_env.cmx obj/lexer_tptp.cmx obj/lexer_fof.cmx obj/parser_tptp.cmx obj/instantiation_env.cmx obj/aigCommon.cmx obj/aigLoader.cmx obj/aigWitness.cmx obj/aigOptimiser.cmx obj/bmc1Common.cmx obj/aigClausifier.cmx obj/parseFiles.cmx obj/aigSaver.cmx obj/definitions.cmx obj/splitting_grd.cmx obj/splitting_nvd.cmx obj/splitting_cvd.cmx obj/splitting.cmx obj/prep_unary_pred.cmx obj/unif.cmx obj/unifIndex.cmx obj/discrTree.cmx obj/discrTree_func.cmx obj/unifIndexMap.cmx obj/unifIndexDiscrTree.cmx obj/unifIndexDebug.cmx obj/subsetSubsume.cmx obj/subsumptionIndex.cmx obj/eq_axioms.cmx obj/cMinisat.cmx obj/propSolver.cmx obj/unsatCore.cmx obj/prop_solver_exchange.cmx obj/symbol_reach.cmx obj/type_inf.cmx obj/prep_sem_filter.cmx obj/prep_sem_filter_unif.cmx obj/inference_rules.cmx obj/simplify.cmx obj/predElim.cmx obj/passiveQueues.cmx obj/clauseUnifIndex.cmx obj/tstpProof.cmx obj/resolution_env.cmx obj/resolution_sel.cmx obj/resolution_loop.cmx obj/bin_hyper_res.cmx obj/preprocess.cmx obj/instantiation_sel.cmx obj/instantiation_loop.cmx obj/lemma_lifting.cmx obj/bmc1Equal.cmx obj/bmc1Axioms.cmx obj/bmc1Deadlock.cmx obj/bmc1InitTarget.cmx obj/bmc1SplitPredicate.cmx obj/model_inst.cmx obj/model_res.cmx obj/bmc1Witness.cmx obj/finite_models.cmx obj/proof_search_loop.cmx obj/abstr_ref_arg_filter.cmx obj/axiom_selection.cmx obj/finite_models_loop.cmx obj/proof_search_schedule.cmx obj/bmc1_loop.cmx obj/git_info.cmx obj/qbf_env.cmx obj/qbf_preprocess.cmx obj/qbf_fof.cmx obj/iprover.cmx

• as -o '/tmp/camlstartup9e7204.o' '/tmp/camlstartup661b9c.s'
• gcc -std=gnu99 -O2 -fno-strict-aliasing -fwrapv -fno-builtin-memcmp -Wall -fno-tree-vrp -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE -Wl,-E -o 'iproveropt' '-Lobj/' '-Lutil/lib' '-Locamlgraph/' '-Lutil/objsize-stub' '-L/shareddata/home/korovin/.opam/4.06.0/lib/ocaml' -Wl,--no-export-dynamic,-static '/tmp/camlstartup9e7204.o' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/std_exit.o' 'obj/iprover.o' 'obj/qbf_fof.o' 'obj/qbf_preprocess.o' 'obj/qbf_env.o' 'obj/git_info.o' 'obj/bmc1_loop.o' 'obj/proof_search_schedule.o' 'obj/finite_models_loop.o' 'obj/axiom_selection.o' 'obj/abstr_ref_arg_filter.o' 'obj/proof_search_loop.o' 'obj/finite_models.o' 'obj/bmc1Witness.o' 'obj/model_res.o' 'obj/model_inst.o' 'obj/bmc1SplitPredicate.o' 'obj/bmc1InitTarget.o' 'obj/bmc1Deadlock.o' 'obj/bmc1Axioms.o' 'obj/bmc1Equal.o' 'obj/lemma_lifting.o' 'obj/instantiation_loop.o' 'obj/instantiation_sel.o' 'obj/preprocess.o' 'obj/bin_hyper_res.o' 'obj/resolution_loop.o' 'obj/resolution_sel.o' 'obj/resolution_env.o' 'obj/tstpProof.o' 'obj/clauseUnifIndex.o' 'obj/passiveQueues.o' 'obj/predElim.o' 'obj/simplify.o' 'obj/inference_rules.o' 'obj/prep_sem_filter_unif.o' 'obj/prep_sem_filter.o' 'obj/type_inf.o' 'obj/symbol_reach.o' 'obj/prop_solver_exchange.o' 'obj/unsatCore.o' 'obj/propSolver.o' 'obj/cMinisat.o' 'obj/eq_axioms.o' 'obj/subsumptionIndex.o' 'obj/subsetSubsume.o' 'obj/unifIndexDebug.o' 'obj/unifIndexDiscrTree.o' 'obj/unifIndexMap.o' 'obj/discrTree_func.o' 'obj/discrTree.o' 'obj/unifIndex.o' 'obj/unif.o' 'obj/prep_unary_pred.o' 'obj/splitting.o' 'obj/splitting_cvd.o' 'obj/splitting_nvd.o' 'obj/splitting_grd.o' 'obj/definitions.o' 'obj/aigSaver.o' 'obj/parseFiles.o' 'obj/aigClausifier.o' 'obj/bmc1Common.o' 'obj/aigOptimiser.o' 'obj/aigWitness.o' 'obj/aigLoader.o' 'obj/aigCommon.o' 'obj/instantiation_env.o' 'obj/parser_tptp.o' 'obj/lexer_fof.o' 'obj/lexer_tptp.o' 'obj/prop_env.o' 'obj/prop_var.o' 'obj/problem_properties.o' 'obj/parser_types.o' 'obj/finiteDomain.o' 'obj/cone_symb.o' 'obj/logic_interface.o' 'obj/important_lit.o' 'obj/systemDBs.o' 'obj/clause.o' 'obj/dismatching.o' 'obj/substBound.o' 'obj/subst.o' 'obj/orderings.o' 'obj/termDB.o' 'obj/term.o' 'obj/var.o' 'obj/symbolDB.o' 'obj/symbol.o' 'obj/abstAssignDB.o' 'obj/abstDB.o' 'obj/vectorIndex.o' 'obj/trie_func.o' 'obj/trie.o' 'obj/tree.o' 'obj/priority_queues.o' 'obj/priority_queue.o' 'obj/heap.o' 'obj/tableArray.o' 'obj/assignMap.o' 'obj/bit_vec.o' 'obj/signals.o' 'obj/statistics.o' 'obj/options.o' 'obj/union_find.o' 'obj/hashcons.o' 'obj/ref_cnt.o' 'obj/lib.o' './ocamlgraph/graph.a' 'util/lib/minisat.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/str.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/unix.a' 'util/objsize-stub/objsize.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/stdlib.a' '-L/shareddata/home/korovin/iprover-local/util/lib' '-L/shareddata/home/korovin/iprover-local/util/minisat/simp' '-lminisat_stubs' '-lminisat' '-lstdc++' '-lcamlstr' '-lunix' '-lobjsize' 'obj/aiger.o' 'obj/aigLoad.o' 'obj/solver.o' 'obj/solver_interface.o' '-Lutil/objsize-stub' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a' -lm -ldl
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a(unix.o): In function caml_dlopen': /shareddata/home/korovin/.opam/4.06.0/build/ocaml/asmrun/unix.c:273: warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/bin/ld: cannot find -lgcc_s /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(initgroups.o): In function unix_initgroups':
  initgroups.c:(.text+0x1f): warning: Using 'initgroups' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrgid': getgr.c:(.text+0x128): warning: Using 'getgrgid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getgr.o): In function unix_getgrnam':
  getgr.c:(.text+0x101): warning: Using 'getgrnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwnam': getpw.c:(.text+0x151): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getpw.o): In function unix_getpwuid':
  getpw.c:(.text+0x178): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getaddrinfo.o): In function unix_getaddrinfo': getaddrinfo.c:(.text+0x224): warning: Using 'getaddrinfo' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyaddr':
  gethost.c:(.text+0x209): warning: Using 'gethostbyaddr_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(gethost.o): In function unix_gethostbyname': gethost.c:(.text+0x2b9): warning: Using 'gethostbyname_r' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobynumber':
  getproto.c:(.text+0xe8): warning: Using 'getprotobynumber' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getproto.o): In function unix_getprotobyname': getproto.c:(.text+0xc1): warning: Using 'getprotobyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getserv.o): In function unix_getservbyname':
  getserv.c:(.text+0x108): warning: Using 'getservbyname' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libunix.a(getserv.o): In function `unix_getservbyport':
  getserv.c:(.text+0x159): warning: Using 'getservbyport' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
  /usr/bin/ld: cannot find -lgcc_s
  collect2: error: ld returned 1 exit status
  File "caml_startup", line 1:
  Error: Error during linking

I briefly looked but could not find an easy fix to this.

Thanks

Comment author: @gasche

(Once we understand how to get a smaller repro case, I think that having it in the testsuite would be helpful to catch future regressions such as this one.)

Comment author: @nojb

Could you try adding the flag -ccopt -static-libgcc on top of -ccopt -Wl,--no-export-dynamic to the ocamlopt invocation?

Comment author: korovin

It compiles with -ccopt -Wl,--no-export-dynamic -ccopt -static-libgcc (below)

ldd shows:

ldd iproveropt
linux-vdso.so.1 => (0x00007ffed9182000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f3cd2d90000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f3cd2a88000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f3cd2880000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f3cd24b8000)
/lib64/ld-linux-x86-64.so.2 (0x00007f3cd3098000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f3cd22a0000)

==========

ocamlopt -ccopt -Wl,--no-export-dynamic -ccopt -static-libgcc obj/aiger.o obj/aigLoad.o obj/solver.o obj/solver_interface.o -o iproveropt
-cclib -Lutil/objsize-stub objsize.cmxa
-verbose -w @6+5+7+44+45 -inline 10 -I obj/ -I util/lib -I ocamlgraph/ -I util/objsize-stub unix.cmxa str.cmxa util/lib/minisat.cmxa ./ocamlgraph/graph.cmxa obj/lib.cmx obj/ref_cnt.cmx obj/hashcons.cmx obj/union_find.cmx obj/options.cmx obj/statistics.cmx obj/signals.cmx obj/bit_vec.cmx obj/assignMap.cmx obj/tableArray.cmx obj/heap.cmx obj/priority_queue.cmx obj/priority_queues.cmx obj/tree.cmx obj/trie.cmx obj/trie_func.cmx obj/vectorIndex.cmx obj/abstDB.cmx obj/abstAssignDB.cmx obj/symbol.cmx obj/symbolDB.cmx obj/var.cmx obj/term.cmx obj/termDB.cmx obj/orderings.cmx obj/subst.cmx obj/substBound.cmx obj/dismatching.cmx obj/clause.cmx obj/systemDBs.cmx obj/important_lit.cmx obj/logic_interface.cmx obj/cone_symb.cmx obj/finiteDomain.cmx obj/parser_types.cmx obj/problem_properties.cmx obj/prop_var.cmx obj/prop_env.cmx obj/lexer_tptp.cmx obj/lexer_fof.cmx obj/parser_tptp.cmx obj/instantiation_env.cmx obj/aigCommon.cmx obj/aigLoader.cmx obj/aigWitness.cmx obj/aigOptimiser.cmx obj/bmc1Common.cmx obj/aigClausifier.cmx obj/parseFiles.cmx obj/aigSaver.cmx obj/definitions.cmx obj/splitting_grd.cmx obj/splitting_nvd.cmx obj/splitting_cvd.cmx obj/splitting.cmx obj/prep_unary_pred.cmx obj/unif.cmx obj/unifIndex.cmx obj/discrTree.cmx obj/discrTree_func.cmx obj/unifIndexMap.cmx obj/unifIndexDiscrTree.cmx obj/unifIndexDebug.cmx obj/subsetSubsume.cmx obj/subsumptionIndex.cmx obj/eq_axioms.cmx obj/cMinisat.cmx obj/propSolver.cmx obj/unsatCore.cmx obj/prop_solver_exchange.cmx obj/symbol_reach.cmx obj/type_inf.cmx obj/prep_sem_filter.cmx obj/prep_sem_filter_unif.cmx obj/inference_rules.cmx obj/simplify.cmx obj/predElim.cmx obj/passiveQueues.cmx obj/clauseUnifIndex.cmx obj/tstpProof.cmx obj/resolution_env.cmx obj/resolution_sel.cmx obj/resolution_loop.cmx obj/bin_hyper_res.cmx obj/preprocess.cmx obj/instantiation_sel.cmx obj/instantiation_loop.cmx obj/lemma_lifting.cmx obj/bmc1Equal.cmx obj/bmc1Axioms.cmx obj/bmc1Deadlock.cmx obj/bmc1InitTarget.cmx obj/bmc1SplitPredicate.cmx obj/model_inst.cmx obj/model_res.cmx obj/bmc1Witness.cmx obj/finite_models.cmx obj/proof_search_loop.cmx obj/abstr_ref_arg_filter.cmx obj/axiom_selection.cmx obj/finite_models_loop.cmx obj/proof_search_schedule.cmx obj/bmc1_loop.cmx obj/git_info.cmx obj/qbf_env.cmx obj/qbf_preprocess.cmx obj/qbf_fof.cmx obj/iprover.cmx

• as -o '/tmp/camlstartup9e054e.o' '/tmp/camlstartup3e8ac2.s'
• gcc -std=gnu99 -O2 -fno-strict-aliasing -fwrapv -fno-builtin-memcmp -Wall -fno-tree-vrp -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE -Wl,-E -o 'iproveropt' '-Lobj/' '-Lutil/lib' '-Locamlgraph/' '-Lutil/objsize-stub' '-L/shareddata/home/korovin/.opam/4.06.0/lib/ocaml' -Wl,--no-export-dynamic -static-libgcc '/tmp/camlstartup9e054e.o' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/std_exit.o' 'obj/iprover.o' 'obj/qbf_fof.o' 'obj/qbf_preprocess.o' 'obj/qbf_env.o' 'obj/git_info.o' 'obj/bmc1_loop.o' 'obj/proof_search_schedule.o' 'obj/finite_models_loop.o' 'obj/axiom_selection.o' 'obj/abstr_ref_arg_filter.o' 'obj/proof_search_loop.o' 'obj/finite_models.o' 'obj/bmc1Witness.o' 'obj/model_res.o' 'obj/model_inst.o' 'obj/bmc1SplitPredicate.o' 'obj/bmc1InitTarget.o' 'obj/bmc1Deadlock.o' 'obj/bmc1Axioms.o' 'obj/bmc1Equal.o' 'obj/lemma_lifting.o' 'obj/instantiation_loop.o' 'obj/instantiation_sel.o' 'obj/preprocess.o' 'obj/bin_hyper_res.o' 'obj/resolution_loop.o' 'obj/resolution_sel.o' 'obj/resolution_env.o' 'obj/tstpProof.o' 'obj/clauseUnifIndex.o' 'obj/passiveQueues.o' 'obj/predElim.o' 'obj/simplify.o' 'obj/inference_rules.o' 'obj/prep_sem_filter_unif.o' 'obj/prep_sem_filter.o' 'obj/type_inf.o' 'obj/symbol_reach.o' 'obj/prop_solver_exchange.o' 'obj/unsatCore.o' 'obj/propSolver.o' 'obj/cMinisat.o' 'obj/eq_axioms.o' 'obj/subsumptionIndex.o' 'obj/subsetSubsume.o' 'obj/unifIndexDebug.o' 'obj/unifIndexDiscrTree.o' 'obj/unifIndexMap.o' 'obj/discrTree_func.o' 'obj/discrTree.o' 'obj/unifIndex.o' 'obj/unif.o' 'obj/prep_unary_pred.o' 'obj/splitting.o' 'obj/splitting_cvd.o' 'obj/splitting_nvd.o' 'obj/splitting_grd.o' 'obj/definitions.o' 'obj/aigSaver.o' 'obj/parseFiles.o' 'obj/aigClausifier.o' 'obj/bmc1Common.o' 'obj/aigOptimiser.o' 'obj/aigWitness.o' 'obj/aigLoader.o' 'obj/aigCommon.o' 'obj/instantiation_env.o' 'obj/parser_tptp.o' 'obj/lexer_fof.o' 'obj/lexer_tptp.o' 'obj/prop_env.o' 'obj/prop_var.o' 'obj/problem_properties.o' 'obj/parser_types.o' 'obj/finiteDomain.o' 'obj/cone_symb.o' 'obj/logic_interface.o' 'obj/important_lit.o' 'obj/systemDBs.o' 'obj/clause.o' 'obj/dismatching.o' 'obj/substBound.o' 'obj/subst.o' 'obj/orderings.o' 'obj/termDB.o' 'obj/term.o' 'obj/var.o' 'obj/symbolDB.o' 'obj/symbol.o' 'obj/abstAssignDB.o' 'obj/abstDB.o' 'obj/vectorIndex.o' 'obj/trie_func.o' 'obj/trie.o' 'obj/tree.o' 'obj/priority_queues.o' 'obj/priority_queue.o' 'obj/heap.o' 'obj/tableArray.o' 'obj/assignMap.o' 'obj/bit_vec.o' 'obj/signals.o' 'obj/statistics.o' 'obj/options.o' 'obj/union_find.o' 'obj/hashcons.o' 'obj/ref_cnt.o' 'obj/lib.o' './ocamlgraph/graph.a' 'util/lib/minisat.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/str.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/unix.a' 'util/objsize-stub/objsize.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/stdlib.a' '-L/shareddata/home/korovin/iprover-local/util/lib' '-L/shareddata/home/korovin/iprover-local/util/minisat/simp' '-lminisat_stubs' '-lminisat' '-lstdc++' '-lcamlstr' '-lunix' '-lobjsize' 'obj/aiger.o' 'obj/aigLoad.o' 'obj/solver.o' 'obj/solver_interface.o' '-Lutil/objsize-stub' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a' -lm -ldl

Comment author: @nojb

Thanks.

I believe the "culprit" is 8b6df3a755.

Comment author: @nojb

But I am not sure what is the "right solution" in any case.

Comment author: korovin

Some clarification:

1. ocamlopt -verbose -ccopt -static test.ml -o test
   fails with test.ml just containg
   print_endline "test";

ocamlopt -verbose -ccopt -static static_linking_test.ml -o static_linking_test

• as -o 'static_linking_test.o' '/tmp/camlasmcdd738.s'
• as -o '/tmp/camlstartupdf112f.o' '/tmp/camlstartup6e9b40.s'
• gcc -std=gnu99 -O2 -fno-strict-aliasing -fwrapv -fno-builtin-memcmp -Wall -fno-tree-vrp -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE -Wl,-E -o 'static_linking_test' '-L/shareddata/home/korovin/.opam/4.06.0/lib/ocaml' -static '/tmp/camlstartupdf112f.o' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/std_exit.o' 'static_linking_test.o' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/stdlib.a' '/shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a' -lm -ldl
  /shareddata/home/korovin/.opam/4.06.0/lib/ocaml/libasmrun.a(unix.o): In function caml_dlopen': /shareddata/home/korovin/.opam/4.06.0/build/ocaml/asmrun/unix.c:273: warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/bin/ld: dynamic STT_GNU_IFUNC symbol ceil' with pointer equality in `/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/libm.a(s_ceil.o)' cannot be used when making an executable; recompile with -fPIE and relink with -pie
  collect2: error: ld returned 1 exit status
  File "caml_startup", line 1:
  Error: Error during linking

2. On the other hand

   ocamlopt -verbose -ccopt -static -ccopt -Wl,--no-export-dynamic

   works in both cases (in above I messed up some options).

Thanks

Comment author: @nojb

Personally I am leaning to marking this issue as "resolved, no change required".

If one wants to link everything statically it can be done and just needs special flags to be passed to the compiler using -ccopt. The bug fix 8b6df3a755 made it necessary to pass one more flag to achieve static linking, but it is not a "regression" per se, in my view.

Comment author: @gasche

-ccopt -static is what is documented in the manual

http://caml.inria.fr/pub/docs/manual-ocaml-4.06/intfc.html#sec418

and on the web

http://rgrinberg.com/posts/static-binaries-tutorial/

At the very least, it would be nice to have the correct options be documented somewhere.

Comment author: @nojb

Ah, I had missed the fact that -ccopt -static is advertised in the manual, thanks for the pointer. In that case we need to do something about this.

Comment author: @xavierleroy

-ccopt -static is advertised in the manual

Probably it should not be advertised. These days, many C compilers and C libraries just don't work with static linking or require other linking options beyond -static to achieve the same effect.

When that part of the manual was written, "-ccopt -static" was a good way to produce Linux executables that could run on different distributions that have different libraries. This is no longer the case.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.