Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007697OCamlplatform support (windows, cross-compilation, etc)public2017-12-22 10:022018-01-05 17:20
Reporterkorovin 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSUbuntuOS Version14.04.4
Product Version4.06.0 
Target VersionFixed in Version 
Summary0007697: static linking fails
DescriptionHello,

Could you please take a look at the following issue.
After switching from OCaml 4.05 to 4.06 my project fails to link statically (if I switch back to 4.05 it compiles and links statically fine).

ocamlopt -ccopt -static ...

The error message:

/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

Many thanks,
Konstantin
TagsNo tags attached.
Attached Files

- Relationships
related to 0007562acknowledged Ocamlc got segfault in Alpine ppc64le 

-  Notes
(0018772)
nojebar (developer)
2017-12-22 10:24

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.
(0018773)
korovin (reporter)
2017-12-22 10:43

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
(0018774)
nojebar (developer)
2017-12-22 10:51

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?
(0018775)
korovin (reporter)
2017-12-22 17:05

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
(0018776)
gasche (developer)
2017-12-22 17:10

(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.)
(0018777)
nojebar (developer)
2017-12-22 17:18

Could you try adding the flag -ccopt -static-libgcc on top of -ccopt -Wl,--no-export-dynamic to the ocamlopt invocation?
(0018778)
korovin (reporter)
2017-12-22 17:29

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
(0018779)
nojebar (developer)
2017-12-22 17:39

Thanks.

I believe the "culprit" is https://github.com/ocaml/ocaml/commit/8b6df3a755. [^]
(0018780)
nojebar (developer)
2017-12-22 17:39

But I am not sure what is the "right solution" in any case.
(0018781)
korovin (reporter)
2017-12-23 15:50

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
(0018782)
nojebar (developer)
2017-12-23 19:12

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 https://github.com/ocaml/ocaml/commit/8b6df3a755 [^] made it necessary to pass one more flag to achieve static linking, but it is not a "regression" per se, in my view.
(0018783)
gasche (developer)
2017-12-24 00:12

-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.
(0018784)
nojebar (developer)
2017-12-24 07:43

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.

- Issue History
Date Modified Username Field Change
2017-12-22 10:02 korovin New Issue
2017-12-22 10:24 nojebar Note Added: 0018772
2017-12-22 10:43 korovin Note Added: 0018773
2017-12-22 10:51 nojebar Note Added: 0018774
2017-12-22 17:05 korovin Note Added: 0018775
2017-12-22 17:10 gasche Note Added: 0018776
2017-12-22 17:18 nojebar Note Added: 0018777
2017-12-22 17:29 korovin Note Added: 0018778
2017-12-22 17:39 nojebar Note Added: 0018779
2017-12-22 17:39 nojebar Note Added: 0018780
2017-12-22 17:42 nojebar Status new => confirmed
2017-12-23 15:50 korovin Note Added: 0018781
2017-12-23 19:12 nojebar Note Added: 0018782
2017-12-24 00:12 gasche Note Added: 0018783
2017-12-24 07:43 nojebar Note Added: 0018784
2018-01-05 17:20 gasche Relationship added related to 0007562


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker