Compiling z3 ml's API with cygwin

[anmaped]

It appears that can be a flexdll related issue. Could you guys confirm ? Maybe something related to elf lib file "libz3ml.a".

I'm using ocaml 4.03.0 and flexdll-0.35.

$ make
ocamlc  -i -I api/ml -c ../src/api/ml/z3enums.ml > api/ml/z3enums.mli
ocamlc  -I api/ml -o api/ml/z3enums.cmi -c api/ml/z3enums.mli
ocamlc  -I api/ml -o api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml
ocamlc  -i -I api/ml -c ../src/api/ml/z3native.ml > api/ml/z3native.mli
ocamlc  -I api/ml -o api/ml/z3native.cmi -c api/ml/z3native.mli
ocamlc  -I api/ml -o api/ml/z3native.cmo -c ../src/api/ml/z3native.ml
cp ../src/api/ml/z3.mli api/ml/z3.mli
ocamlc  -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli
ocamlc  -I api/ml -o api/ml/z3.cmo -c ../src/api/ml/z3.ml
ocamlc  -ccopt "-D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -std=c++11 -fvisibility=hidden -c -mfpmath=sse -msse -msse2 -D_NO_OMP_ -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer -D_CYGWIN -fno-strict-aliasing -I /home/anmap/.opam/4.03.0/lib/ocaml -I ../src/api -I ../src/api/ml -o api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c
cc1: warning: command line option ‘-std=c++11’ is valid for C++/ObjC++ but not for C
ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo  libz3.dll
ocamlopt  -I api/ml -o api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml
ocamlopt  -I api/ml -o api/ml/z3native.cmx -c ../src/api/ml/z3native.ml
ocamlopt  -I api/ml -o api/ml/z3.cmx -c ../src/api/ml/z3.ml
ocamlmklib -o api/ml/z3ml -I api/ml api/ml/z3native_stubs.o  api/ml/z3enums.cmx api/ml/z3native.cmx api/ml/z3.cmx libz3.dll
ocamlopt  -shared -o api/ml/z3ml.cmxs -I api/ml api/ml/z3ml.cmxa
** Fatal error: Error while reading api/ml/libz3ml.a: Invalid_argument("String.create")
File "caml_startup", line 1:
Error: Error during linking
make: *** [Makefile:4370: api/ml/z3ml.cmxs] Error 2

[nojb]

Is your flexlink.exe 32-bit executable ?

[anmaped]

@nojb Yes, it is. First, I have used the pre-compiled binary and then I have compiled one from scratch in order to discard other issues.

gcc and g++ is for i686.

[nojb]

Yes, flexlink.exe currently reads the object file into a string, hence it fails if 32-bit and the object file is larger than maximum string size. Did you try recompiling flexlink.exe as a 64-bit executable ?

[anmaped]

@nojb Thanks.

I have found that using Andreas Hauptmann's installer the same does not happen (for x86 and x86_64). I also have compiled flexdll for x86 and x86_64. Probably It is something in the ocaml build.

It is not related with flexdll.