From 83e92c2dd7716f7ad765030facbb90da688e73af Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 7 Oct 2012 02:26:27 +0100 Subject: [PATCH] added build and test scripts and READMEs to distribute --- ml/README-linux | 22 ++++++++++++++++++++++ ml/README-osx | 22 ++++++++++++++++++++++ ml/README-test-linux | 17 +++++++++++++++++ ml/README-test-osx | 17 +++++++++++++++++ ml/README-test-win | 23 +++++++++++++++++++++++ ml/README-win | 23 +++++++++++++++++++++++ ml/build-lib.cmd | 3 +++ ml/build-lib.sh | 31 +++++++++++++++++++++++++++++++ ml/build-test.cmd | 19 +++++++++++++++++++ ml/build-test.sh | 6 ++++++ ml/exec.cmd | 5 +++++ ml/exec.sh | 4 ++++ 12 files changed, 192 insertions(+) create mode 100644 ml/README-linux create mode 100644 ml/README-osx create mode 100644 ml/README-test-linux create mode 100644 ml/README-test-osx create mode 100644 ml/README-test-win create mode 100644 ml/README-win create mode 100644 ml/build-lib.cmd create mode 100644 ml/build-lib.sh create mode 100644 ml/build-test.cmd create mode 100644 ml/build-test.sh create mode 100644 ml/exec.cmd create mode 100644 ml/exec.sh diff --git a/ml/README-linux b/ml/README-linux new file mode 100644 index 000000000..a726c0c94 --- /dev/null +++ b/ml/README-linux @@ -0,0 +1,22 @@ +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + ./build-lib.sh + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/ml/README-osx b/ml/README-osx new file mode 100644 index 000000000..a726c0c94 --- /dev/null +++ b/ml/README-osx @@ -0,0 +1,22 @@ +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + ./build-lib.sh + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/ml/README-test-linux b/ml/README-test-linux new file mode 100644 index 000000000..34900883d --- /dev/null +++ b/ml/README-test-linux @@ -0,0 +1,17 @@ +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.sh' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi. diff --git a/ml/README-test-osx b/ml/README-test-osx new file mode 100644 index 000000000..bfc6b115e --- /dev/null +++ b/ml/README-test-osx @@ -0,0 +1,17 @@ +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.sh' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi. diff --git a/ml/README-test-win b/ml/README-test-win new file mode 100644 index 000000000..d9be0174b --- /dev/null +++ b/ml/README-test-win @@ -0,0 +1,23 @@ +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.cmd' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. +Running from the Visual Studio Command Prompt configures the Microsoft C compiler. + +- The script 'exec.cmd' adds the bin directory to the path. So, + test_mlapi.exe can find z3.dll. + + + + diff --git a/ml/README-win b/ml/README-win new file mode 100644 index 000000000..91d2faa4f --- /dev/null +++ b/ml/README-win @@ -0,0 +1,23 @@ +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + .\build-lib.cmd + +Remark: The OCaml and C compiler tool chains must be configured in your environment. +Running from the Visual Studio Command Prompt configures the Microsoft C compiler. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/ml/build-lib.cmd b/ml/build-lib.cmd new file mode 100644 index 000000000..93d667a34 --- /dev/null +++ b/ml/build-lib.cmd @@ -0,0 +1,3 @@ +@echo off + +call .\compile_mlapi.cmd ..\include ..\bin ..\bin diff --git a/ml/build-lib.sh b/ml/build-lib.sh new file mode 100644 index 000000000..93c7262b1 --- /dev/null +++ b/ml/build-lib.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +# Script to compile the Z3 OCaml API +# Expects to find ../lib/libz3{,_dbg}.{a,so,dylib} + +CFLAGS="-ccopt -Wno-discard-qual -ccopt -I../include" +XCDBG="-g -ccopt -g $CFLAGS" +XCOPT="-ccopt -O3 -ccopt -fomit-frame-pointer $CFLAGS" + + +ocamlc -c $XCDBG z3_stubs.c z3_theory_stubs.c z3.mli z3.ml + +ocamlopt -c $XCDBG z3_stubs.c z3_theory_stubs.c z3.mli z3.ml + +ar rcs libz3stubs_dbg.a z3.o z3_stubs.o z3_theory_stubs.o + +ocamlopt -c $XCOPT z3_stubs.c z3_theory_stubs.c z3.mli z3.ml + +ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o + +ocamlc -custom -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3_dbg -cclib -lcamlidl -cclib -lz3stubs_dbg z3.cmo -o z3_dbg.cma + +ocamlc -custom -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmo -o z3.cma + +ocamlopt -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3_dbg -cclib -lcamlidl -cclib -lz3stubs_dbg z3.cmx -o z3_dbg.cmxa + +ocamlopt -a $XCOPT -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa + +ocamlmktop -o ocamlz3 z3.cma -cclib -L. + +rm z3.cm{o,x} *.o diff --git a/ml/build-test.cmd b/ml/build-test.cmd new file mode 100644 index 000000000..7b80dc795 --- /dev/null +++ b/ml/build-test.cmd @@ -0,0 +1,19 @@ +@echo off + +if not exist ..\..\ocaml\z3.cmxa ( + echo "YOU MUST BUILD OCAML API! Go to directory ..\ocaml" + goto :EOF +) + +REM ocaml (>= 3.11) calls the linker through flexlink +ocamlc -version >> ocaml_version +set /p OCAML_VERSION=