Arlen Cox  committed f64b4e3

ocamlfind library support is now complete! hooray!

  • Participants
  • Parent commits 24381ed
  • Branches master

Comments (0)

Files changed (2)

File README.ocaml

+To build and use the OCaml binding on OS X, you need to install the basic prerequisites:
+* A recent version of OCaml (this was tested with 4.00)
+* findlib
+Then build the Z3 libraries with the following commands:
+# autoconf
+# ./configure
+# make
+# make dylib
+# make lib
+Then copy the libraries to the appropriate location:
+# cp bin/external/z3 /usr/local/bin
+# cp bin/external/libz3.dylib /usr/local/lib
+# cp bin/external/libz3.a /usr/local/lib
+Then change to the ml directory and build the bindings:
+# make
+# sudo make install
+To use the z3 package use ocamlbuild:
+ocamlbuild -use-ocamlfind -package z3 blah.byte
+to build a blah.byte from (and all dependencies) and to link with the Z3 package.
+Alternatively you can add package(z3) to the _tags file for use with ocamlbuild.
+# assumes that libz3.a is in the link path -L and that
+# is in the dynamic load libary path (LD_LIBRARY_PATH or
+OCAML_LOC=$(shell ocamlc -where)
+Z3_VERSION=$(shell ../bin/external/z3 -version)
+.PHONY: all install clean uninstall remove
+LIBS=z3.cmi z3.cmo z3.cmx z3.o libz3caml.a z3caml.cma z3caml.cmxa z3caml.a 
+all : $(LIBS)
+install : META $(LIBS)
+	$(OCAMLFIND) install z3 META $(LIBS)
+# build the library
+#$(OCAMLMKLIB) -custom -verbose z3_stubs.o z3_theory_stubs.o z3.mli -cclib -L$(OCAML_LOC) -cclib -lz3caml -cclib -lcamlidl -cclib -lz3 -ccopt -fopenmp -o z3caml
+$(LIBS) : z3_theory_stubs.o z3_stubs.o
+	ar rc ./libz3caml.a  z3_stubs.o z3_theory_stubs.o; ranlib ./libz3caml.a
+	$(OCAMLC) -custom -a -o z3caml.cma      -ccopt -fopenmp z3.mli -cclib -lz3caml -cclib -lz3 -cclib -L/usr/local/lib/ocaml -cclib -lcamlidl 
+	$(OCAMLOPT) -a -o z3caml.cmxa      -ccopt -fopenmp z3.mli -cclib -lz3caml -cclib -lz3 -cclib -L/usr/local/lib/ocaml -cclib -lcamlidl 
+# build the stubs
+z3_theory_stubs.o z3_stubs.o : z3_theory_stubs.c z3_stubs.c
+	$(OCAMLC) -verbose -c -I ../lib z3_theory_stubs.c z3_stubs.c > /dev/null 2>&1
+# construct the meta file
+	@echo "version=\"$(Z3_VERSION)\"" > META
+	@echo "description=\"Z3 Theorem Prover\"" >> META
+	@echo "archive(byte)=\"z3.cmo\"" >> META
+	@echo "archive(native)=\"z3.cmx\"" >> META
+	@echo "linkopts(byte)=\"-custom -cclib -lz3caml -cclib -lz3 -cclib -L$(OCAML_LOC) -cclib -lcamlidl -cclib -fopenmp\"" >> META
+	@echo "linkopts=\"-cclib -lz3caml -cclib -lz3 -cclib -L$(OCAML_LOC) -cclib -lcamlidl -cclib -fopenmp\"" >> META
+clean :
+	-rm -rf META $(LIBS) z3_theory_stubs.o z3_stubs.o
+remove uninstall :
+	$(OCAMLFIND) remove z3