diff --git a/Makefile b/Makefile index 467ea0d14edcc19dbde34baab97d239ef62cfa60..b2ab6ae28f0da6be7948d99b773d948abfc55888 100644 --- a/Makefile +++ b/Makefile @@ -1,17 +1,136 @@ -.PHONY: build install - -PREFIX= -ECLIPSEBIN= - -build: - rm -f Src/COLIBRI/lib/v7/x86_64_linux/* Src/COLIBRI/simplex_ocaml.pl - (cd Src/COLIBRI/simplex_ocaml; ECLIPSEBIN=$(ECLIPSEBIN) dune build simplex_ocaml_mod_v7.so simplex_ocaml.pl) - (cd Src/COLIBRI/simplex_ocaml; cp _build/default/simplex_ocaml.pl ..) - mkdir -p Src/COLIBRI/lib/v7/x86_64_linux - (cd Src/COLIBRI/simplex_ocaml; cp _build/default/simplex_ocaml_mod_v7.so ../lib/v7/x86_64_linux/simplex_ocaml.so) - (cd Src/Floats; g++ -fPIC -O -D__LINUX__ -I $(ECLIPSEBIN)/include/x86_64_linux -shared EclipseInterfaceSimFloat2.2.cpp Floatcpp-3.0_SimFloat2.2.cpp -o ../COLIBRI/lib/v7/x86_64_linux/float_util.so) - ocamlopt -o compile_colibri unix.cmxa compile_colibri.ml +.PHONY: all install clean clean_install simplex simplex_epilog + +# Bundle prefix, override to specify a different directory +BUNDLE ?= $(PWD)/bundle + +# Which eclipse version to use, among {v5|v7} +# (v5 is currently broken) +ECL_VERSION ?= v7 + +all : build + +# ================================================== +# MACRO +# ================================================== + +# Target of copy dependencies are added to this variable. +COPY_DEPS := + +define add_copy_rule +COPY_DEPS += $(2) +$(2) : $(1) + mkdir -p $(dir $(2)) + cp $(1) $(2) +endef + +# Add a rule to copy a file from a source to a destination, while +# ensuring that the target directory exists. +# +# $(1): source +# $(2): destination +# +define require_copy +$(eval $(call add_copy_rule,$(1),$(2))) +endef + +# ================================================== +# CONFIGURATION +# ================================================== + +ROOT := $(realpath Src/) +COLIBRI := $(ROOT)/COLIBRI +SIMPLEX_BUILD := $(COLIBRI)/simplex_ocaml/_build/default +$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml.pl,$(COLIBRI)/simplex_ocaml.pl) + +ifeq ($(ECL_VERSION),v7) +export ECLIPSEBIN=$(PWD)/Bin/ECLIPSE_V7.0_45 +LIBDIR=$(COLIBRI)/lib/v7 +SIMPLEX := simplex_ocaml_mod_v7.so +FLOAT_LIB := $(LIBDIR)/x86_64_linux/float_util.so +$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml_mod_v7.so,$(LIBDIR)/x86_64_linux/simplex_ocaml.so) +endif + +ifeq ($(ECL_VERSION),v5) +export ECLIPSEBIN= +LIBDIR=$(COLIBRI)/lib/v5 +SIMPLEX := simplex_ocaml_mod.so +FLOAT_LIB := $(LIBDIR)/x86_64_linux/float_util.so +$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml_mod.so,$(LIBDIR)/x86_64_linux/simplex_ocaml.so) +endif + +# ================================================== +# INFOS +# ================================================== + +$(info BUNDLE=$(BUNDLE)) +$(info ECL_VERSION=$(ECL_VERSION)) +$(info COLIBRI=$(COLIBRI)) +$(info ECLIPSEBIN=$(ECLIPSEBIN)) + +# ================================================== +# SIMPLEX_OCAML +# ================================================== + +simplex: $(ECLIPSEBIN) + cd $(COLIBRI)/simplex_ocaml && dune build $(SIMPLEX) simplex_ocaml.pl + +simplex_epilog : simplex $(COPY_DEPS) + @true + +# ================================================== +# FLOAT LIBRARY +# ================================================== + +CPP_FLAGS := -fPIC -O -D__LINUX__ -shared +CPP_FLAGS += -I $(ECLIPSEBIN)/include/x86_64_linux + +CPP_FILES := \ + $(ROOT)/Floats/EclipseInterfaceSimFloat2.2.cpp \ + $(ROOT)/Floats/Floatcpp-3.0_SimFloat2.2.cpp + +$(FLOAT_LIB) : $(CPP_FILES) + g++ $(CPP_FLAGS) $(CPP_FILES) -o $@ + +# ================================================== +# BUILD +# ================================================== + +clean: + rm -rf $(LIBDIR) + rm -f $(COLIBRI)/simplex_ocaml.pl + rm -f $(FLOAT_LIB) + rm -f compile_colibri + +compile_colibri : compile_colibri.ml + ocamlopt -o $@ unix.cmxa $^ + +build: simplex_epilog $(FLOAT_LIB) compile_colibri ./compile_colibri --eclipsedir $(ECLIPSEBIN) -install: - ./bundle.sh $(PREFIX) +# ================================================== +# INSTALL +# ================================================== + +BUNDLE_SRC := \ + Src/COLIBRI/col_solve.eco \ + Src/COLIBRI/filter_smtlib_file \ + Src/COLIBRI/filter_smtlib_file.exe + +$(BUNDLE)/colibri.exe : colibri_for_bundle.ml + ocamlopt -o $@ unix.cmxa $^ + chmod u+x $@ + +clean_install: + rm -fr $(BUNDLE) + +$(BUNDLE): + mkdir -p $(BUNDLE) + +install: $(BUNDLE) $(BUNDLE)/colibri.exe + cp $(BUNDLE)/colibri.exe $(BUNDLE)/colibri + mkdir -p $(BUNDLE)/COLIBRI/lib/ + cp -ra $(LIBDIR) $(BUNDLE)/COLIBRI/lib/ + cp -ra $(BUNDLE_SRC) $(BUNDLE)/COLIBRI/ + cp -ra compile_flag.pl $(BUNDLE)/COLIBRI/ + cp -ra version $(BUNDLE)/ + cp -ra $(ECLIPSEBIN) $(BUNDLE)/ECLIPSE/ diff --git a/bundle.sh b/bundle.sh deleted file mode 100755 index 533d1dad625ce6839e6f1c772bb53339e1e0aaaa..0000000000000000000000000000000000000000 --- a/bundle.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/bin/sh - -PREFIX=$1 -rm -fr $PREFIX -mkdir -p $PREFIX/COLIBRI/lib/ - -cp -ra Src/COLIBRI/lib/v7 $PREFIX/COLIBRI/lib/ -cp -ra Src/COLIBRI/col_solve.eco Src/COLIBRI/filter_smtlib_file Src/COLIBRI/filter_smtlib_file.exe $PREFIX/COLIBRI/ -cp -ra compile_flag.pl $PREFIX/COLIBRI/ -cp -ra version $PREFIX/ -ocamlopt unix.cmxa -o $PREFIX/colibri.exe colibri_for_bundle.ml -cp $PREFIX/colibri.exe $PREFIX/colibri -chmod u+x $PREFIX/colibri