mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 01:46:39 +00:00
69 lines
2.7 KiB
Text
69 lines
2.7 KiB
Text
# Makefile to compile OCaml interface to Z3
|
|
#
|
|
# Parameters: ARGS and DEPS environment variables
|
|
# ARGS is passed through to the Makefile that generates the OCaml interface
|
|
# DEPS is a sequence of files that are deleted when the OCaml interface changes
|
|
|
|
SRC_ML=../../../src/api/ml
|
|
ifeq (${OS}, Windows_NT)
|
|
# the BLD_ML path ends up stored in z3.cm{,x}a, so it must be in windows format
|
|
BLD_ML=$(shell cygpath -m $(CURDIR))
|
|
CFLAGS=-ccopt -wd4090 -ccopt -I$(SRC_ML)/..
|
|
XCDBG=-g $(CFLAGS)
|
|
XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS)
|
|
# ole32 is needed by camlidl (COM support)
|
|
XLIB=-cclib ole32.lib
|
|
AR=lib /nologo /LIBPATH:../../build ../../libz3.lib /out:
|
|
O=obj
|
|
A=lib
|
|
else
|
|
BLD_ML=$(CURDIR)
|
|
CFLAGS=-ccopt -Wno-discard-qual -ccopt -Wno-unused-variable -ccopt -I$(SRC_ML)/..
|
|
XCDBG=-g -ccopt -g $(CFLAGS)
|
|
XCOPT=-ccopt -O3 -ccopt -fomit-frame-pointer $(CFLAGS)
|
|
XLIB=
|
|
AR=ar rcs # note trailing space is significant
|
|
O=o
|
|
A=a
|
|
endif
|
|
|
|
|
|
all: z3.cma z3.cmxa ocamlz3
|
|
|
|
|
|
# keep these files to avoid repeatedly rebuilding them
|
|
.PRECIOUS: $(SRC_ML)/z3.ml $(SRC_ML)/z3.mli $(SRC_ML)/z3_stubs.c z3.ml z3.mli z3_stubs.c z3_theory_stubs.c
|
|
|
|
# regenerate OCaml API if needed
|
|
$(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c: $(SRC_ML)/Makefile
|
|
make -C $(SRC_ML) z3.mli z3.ml z3_stubs.c
|
|
|
|
# copy OCaml API from src to build directories
|
|
%.mli %.ml %_stubs.c %_theory_stubs.c: $(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c Makefile
|
|
cp $(SRC_ML)/z3.mli $(SRC_ML)/z3.ml $(SRC_ML)/z3_stubs.c $(SRC_ML)/z3_theory_stubs.c .
|
|
|
|
# OCaml library module for native code clients
|
|
%.cmxa %.cmi lib%stubs.a %.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
|
|
rm -f $(DEPS)
|
|
ocamlopt.opt -c $(XCOPT) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
|
|
$(AR)libz3stubs.$(A) z3.$(O) z3_stubs.$(O) z3_theory_stubs.$(O)
|
|
ocamlopt.opt -a -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs z3.cmx -o z3.cmxa
|
|
rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.$(O) z3.cmx
|
|
|
|
# OCaml library module for byte code clients
|
|
%.cma %.cmi lib%stubs_dbg.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
|
|
rm -f $(DEPS)
|
|
ocamlc.opt -c $(XCDBG) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
|
|
$(AR)libz3stubs_dbg.$(A) z3_stubs.$(O) z3_theory_stubs.$(O)
|
|
ocamlc.opt -custom -a $(CXDBG) -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs_dbg z3.cmo -o z3.cma
|
|
rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.cmo
|
|
|
|
|
|
# OCaml custom toplevel system pre-linked with Z3
|
|
ocamlz3: z3.cma Makefile
|
|
ocamlmktop -o ocamlz3 z3.cma -cclib -L.
|
|
|
|
|
|
clean: Makefile
|
|
make -C $(SRC_ML) clean
|
|
rm -rf Makefile libz3stubs.$(A) libz3stubs_dbg.$(A) ocamlz3 ocamlz3.dSYM z3.$(O) z3.$(A) z3.cma z3.cmi z3.cmo z3.cmx z3.cmxa z3.ml z3.mli z3_stubs.$(O) z3_stubs.c z3_theory_stubs.$(O) z3_theory_stubs.c
|