polazarus / ocamlyices Goto Github PK

after installation (without any obvious errors), when trying to compile the examples I get this error:

/usr/lib/ocaml/ocamlyices/libocamlyices.a(ocamlyices.o): In function `get_unsat_core':
(.text+0x3099): undefined reference to `yices_get_unsat_core_size'
/usr/lib/ocaml/ocamlyices/libocamlyices.a(ocamlyices.o): In function `get_unsat_core':
(.text+0x30bf): undefined reference to `yices_get_unsat_core'

used yices 1.028 during installation.

I am new to ocaml and thus really do not know what's going wrong. Any hint?

Because Yices is not built with the -fPIC flag, the compilation ends with :

gcc -O2 -fPIC -shared -L/usr/local/lib/ocaml -L/usr/local/lib/ocaml/site-lib yices_stubs.o yicesl_stubs.o -Wl,-Bstatic  -lcamlidl -lyices -Wl,-Bdynamic  -lstdc++ -o dllocamlyices.so
/usr/bin/ld: /usr/local/lib/libyices.a(yices.o): relocation R_X86_64_32S against `_ZNSs4_Rep20_S_empty_rep_storageE' can not be used when making a shared object; recompile with -fPIC
/usr/local/lib/libyices.a: could not read symbols: Bad value
collect2: error: ld returned 1 exit status
make: *** [dllocamlyices.so] Error 1

Slight syntax difference between Linux and BSD sed. Taking pull requests or should I maintain a fork?

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 to__imp____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 to__imp____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 to__imp____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 to__imp____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

hi,

just wanted to summarize my experience getting ocamlyices to work on 64-bit SuSE 11.2 . Some stumbling points were:

• /usr/local/lib is not scanned by ldconfig, /usr/local/lib64 is, thus I had to do yices installation manually
• instead of running ldconfig -n had to run just ldconfig when installing yices
• had to run ./configure as root, because ldconfig is in /sbin, which is not in user's path
• had to use
  CFLAGS = -O2 -I/usr/lib64/ocaml/ -fPIC

Best,
Misha

I'm planning to distribute ocamlyices bundled with my tools, but I'd like not to have the dependency on camlidl. Do you think it is safe to distribute the idl files, or are they likely to be very different for different versions of yices?

hi,

a question regarding the use of the API: the C functions can return NULL pointers, is it somehow reflected in the ocaml API?

Best,
Misha