search

polazarus / ocamlyices

Yices SMT solver's binding for the OCaml programming language
http://micdel.fr/ocamlyices.html
7 stars 3 forks source link

Compilation issues on cygwin #6

Open tari3x opened 13 years ago

tari3x commented 13 years ago

FYI, I tried compiling on cygwin and get the following error at linking stage:

gcc -O2 -fPIC -I/usr/lib/ocaml -shared -L/usr/lib/ocaml -L/usr/local/lib yices_stubs.o yicesl_stubs.o yices_extra.o \ -Wl,-Bstatic -lcamlidl \ -Wl,-Bdynamic -lyices -lstdc++ \ -o dllocamlyices.so yices_stubs.o:yices_stubs.c:(.text+0x18e): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x306): undefined reference to_caml_copy_string' yices_stubs.o:yices_stubs.c:(.text+0x346): undefined reference to _caml_copy_double' yices_stubs.o:yices_stubs.c:(.text+0x38a): undefined reference to_caml_copy_int64' yices_stubs.o:yices_stubs.c:(.text+0x472): undefined reference to _caml_copy_string' yices_stubs.o:yices_stubs.c:(.text+0x4d2): undefined reference to_caml_copy_string' yices_stubs.o:yices_stubs.c:(.text+0x516): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x56d): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x594): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x5b6): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x5e6): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x616): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x670): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x694): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x6e9): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x70d): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x75d): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x784): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x7d0): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x7f4): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x83d): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x864): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x886): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x918): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x93d): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x9e5): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xa0a): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xa5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xa7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xadb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xaff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xb5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xb7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xbdb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xbff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xc5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xc7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xcdb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xcff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xd5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xd7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xddb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xdff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xe5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xe7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xedb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xeff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xf5b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xf7f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0xfdb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0xfff): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x105b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x107f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x10e4): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1108): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1152): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1176): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x11cb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x11ef): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x124b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x126f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x12cb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x12ef): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x134b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x136f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x13c2): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x13e6): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x143b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x145f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x14bb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x14df): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x153b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x155f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x15e8): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x160d): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x166c): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1690): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x16eb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x170f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x176b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x178f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x17eb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x180f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x186b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x188f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1918): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x193d): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x19c8): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x19ed): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1a78): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1a9d): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1af0): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1b14): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1b62): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1b86): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1c1c): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1c41): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1c92): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1cb6): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1d02): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1d26): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1d84): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1da8): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1dfb): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1e1f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1e7b): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1e9f): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1f28): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1f4d): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x1fd8): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x1ffd): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2052): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2076): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x20bd): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x20e4): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2130): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2154): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x219d): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x21c4): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x220d): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2234): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2256): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x230d): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2332): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2382): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x23a6): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2431): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2456): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x24a0): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x24c4): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x24ec): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2516): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2593): undefined reference to _caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x25ba): undefined reference to_caml_modify' yices_stubs.o:yices_stubs.c:(.text+0x25e0): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2609): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2611): undefined reference to _caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x261c): undefined reference to_caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x265f): undefined reference to _caml_modify' yices_stubs.o:yices_stubs.c:(.text+0x266b): undefined reference to_caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x26bd): undefined reference to _caml_copy_double' yices_stubs.o:yices_stubs.c:(.text+0x26de): undefined reference to_caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x273c): undefined reference to _caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x2755): undefined reference to_caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x2766): undefined reference to _caml_copy_int32' yices_stubs.o:yices_stubs.c:(.text+0x2774): undefined reference to_caml_copy_int32' yices_stubs.o:yices_stubs.c:(.text+0x278b): undefined reference to _caml_alloc_small' yices_stubs.o:yices_stubs.c:(.text+0x27a0): undefined reference to_caml_local_roots' yices_stubs.o:yices_stubs.c:(.text+0x27bf): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x280d): undefined reference to_caml_copy_int32' yices_stubs.o:yices_stubs.c:(.text+0x282e): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x287d): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x28a4): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2bf5): undefined reference to_caml_alloc' yices_stubs.o:yices_stubs.c:(.text+0x2c1c): undefined reference to _caml_failwith' yices_stubs.o:yices_stubs.c:(.text+0x2d54): undefined reference to_caml_invalid_argument' yices_stubs.o:yices_stubs.c:(.text+0x2e3c): undefined reference to _caml_enter_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2e53): undefined reference to_caml_leave_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2e9b): undefined reference to _caml_enter_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2eaa): undefined reference to_caml_leave_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2ef5): undefined reference to _caml_enter_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2f08): undefined reference to_caml_leave_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2f4b): undefined reference to _caml_enter_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2f5a): undefined reference to_caml_leave_blocking_section' yices_stubs.o:yices_stubs.c:(.text+0x2d20): undefined reference to _caml_copy_string' yicesl_stubs.o:yicesl_stubs.c:(.text+0x9b): undefined reference to_caml_enter_blocking_section' yicesl_stubs.o:yicesl_stubs.c:(.text+0xb1): undefined reference to _caml_leave_blocking_section' yicesl_stubs.o:yicesl_stubs.c:(.text+0xd8): undefined reference to_caml_failwith' yicesl_stubs.o:yicesl_stubs.c:(.text+0x1b6): undefined reference to _caml_alloc' yicesl_stubs.o:yicesl_stubs.c:(.text+0x1e6): undefined reference to_caml_alloc' yicesl_stubs.o:yicesl_stubs.c:(.text+0x235): undefined reference to _caml_alloc' yicesl_stubs.o:yicesl_stubs.c:(.text+0x25c): undefined reference to_caml_failwith' yicesl_stubs.o:yicesl_stubs.c:(.text+0x170): undefined reference to _caml_copy_string' yices_extra.o:yices_extra.c:(.text+0x10): undefined reference toimp__gmpz_init' yices_extra.o:yices_extra.c:(.text+0x3b): undefined reference to __imp____gmpz_sizeinbase' yices_extra.o:yices_extra.c:(.text+0x61): undefined reference toimp__gmpz_get_str' yices_extra.o:yices_extra.c:(.text+0x86): undefined reference to _caml_failwith' yices_extra.o:yices_extra.c:(.text+0xa7): undefined reference toimp__gmpq_init' yices_extra.o:yices_extra.c:(.text+0xc7): undefined reference to __imp____gmpz_sizeinbase' yices_extra.o:yices_extra.c:(.text+0x10d): undefined reference toimp__gmpq_get_str' yices_extra.o:yices_extra.c:(.text+0x138): undefined reference to _caml_failwith' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In functioncamlidl_find_enum': /home/avatar/camlidl-1.05/runtime/idlalloc.c:35: undefined reference to _caml_invalid_argument' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In functioncamlidl_alloc_flag_list': /home/avatar/camlidl-1.05/runtime/idlalloc.c:44: undefined reference to _caml_local_roots' /home/avatar/camlidl-1.05/runtime/idlalloc.c:44: undefined reference to_caml_local_roots' /home/avatar/camlidl-1.05/runtime/idlalloc.c:47: undefined reference to _caml_alloc_small' /home/avatar/camlidl-1.05/runtime/idlalloc.c:53: undefined reference to_caml_local_roots' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In function camlidl_register_allocation': /home/avatar/camlidl-1.05/runtime/idlalloc.c:73: undefined reference to_caml_stat_alloc' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In function camlidl_malloc': /home/avatar/camlidl-1.05/runtime/idlalloc.c:95: undefined reference to_caml_stat_alloc' /home/avatar/camlidl-1.05/runtime/idlalloc.c:96: undefined reference to _caml_stat_free' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In functioncamlidl_free': /home/avatar/camlidl-1.05/runtime/idlalloc.c:108: undefined reference to _caml_stat_free' /usr/lib/ocaml/libcamlidl.a(idlalloc.o): In functioncamlidl_malloc_string': /home/avatar/camlidl-1.05/runtime/idlalloc.c:114: undefined reference to `_caml_string_length' collect2: ld returned 1 exit status make: *\ [dllocamlyices.so] Error 1

tari3x commented 13 years ago

After fighting with C compilation for a while, I switched to --enable-custom and it worked.

tari3x commented 13 years ago

Some further cygwin issues:

polazarus commented 13 years ago

I pushed a commit to fix install-yices (+ install cyg*.dll in bin) and improve Yices and GMP autodetection in the configure. I don't have any time for testing it right now so... you're on your own. Did you try using g++? -lstdc++ might not be enough on Cygwin...

tari3x commented 13 years ago

thanks! Didn't try g++ (thanks for the idea!), just using custom build for now

tari3x commented 13 years ago

There were several issues. I have commented on them in the clone, together with some temporary fixes. I'll try to keep the clone up-to-date with your repository.

Maybe you could just take the view that it's the user's responsibility to maintain appropriate versions of GMP and Yices? In that case AC_CHECK_LIB will probably become enough.