diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e65460bf7e6f2f855ee2b5eb8946aabb1cfa2be6..c484aa40cec60731aec68bdf92c5c5bc41b8f69f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -29,16 +29,10 @@ tests_with_recompilation: #OCaml dependencies - opam depext --install dune zarith num ocplib-simplex parsexp #OCaml compilation - - (cd Src/COLIBRI/simplex_ocaml; ECLIPSEBIN=$(pwd)/../../../Bin dune build simplex_ocaml_mod_v7.so simplex_ocaml.pl) - #Copy OCaml targets - - (cd Src/COLIBRI/simplex_ocaml; cp _build/default/simplex_ocaml.pl ..) - - (cd Src/COLIBRI/simplex_ocaml; cp _build/default/simplex_ocaml_mod_v7.so ../lib/v7/x86_64_linux/simplex_ocaml.so) - #C++ compilation and targets copying - - (cd Src/Floats; g++ -fPIC -O -D__LINUX__ -I ../../Bin/ECLIPSE_V7.0_45/include/x86_64_linux -shared EclipseInterfaceSimFloat2.2.cpp Floatcpp-3.0_SimFloat2.2.cpp -o ../COLIBRI/lib/v7/x86_64_linux/float_util.so) - #Eclipse Prolog compilation of COLIBRI - - ./compile_colibri.sh + - make ECLIPSEBIN=$(pwd)/../../../Bin #Bundle in bundle directory - - ./bundle.sh + - cp -ra Bin/ECLIPSE_V7.0_45/ bundle/ECLIPSE/ + - ./bundle.sh bundle #Test - sudo apt-get update - sudo apt-get install -y parallel diff --git a/Makefile b/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..5142505e2423bf6f5d98da4aa5e99a68be71327a --- /dev/null +++ b/Makefile @@ -0,0 +1,16 @@ +.PHONY: build + +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 ..) + (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 ../../Bin/ECLIPSE_V7.0_45/include/x86_64_linux -shared EclipseInterfaceSimFloat2.2.cpp Floatcpp-3.0_SimFloat2.2.cpp -o ../COLIBRI/lib/v7/x86_64_linux/float_util.so) + ./compile_colibri.sh + + +install: + ./bundle.sh $(PREFIX) diff --git a/README.md b/README.md index ec3a681c712a02c303e474a81963d22ac9304e16..f711afacfd41f35c50c2fb6a34f7b7c8434756c0 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ In order to create a bundle of everything needed to run COLIBRI. run -`compile_colibri.sh` then run `./bundle.sh` it will create +`./compile_colibri.sh` then run `./bundle.sh` it will create a relocalisable directory `bundle`. diff --git a/Src/COLIBRI/simplex_ocaml/ocaml_eclipse.ml b/Src/COLIBRI/simplex_ocaml/ocaml_eclipse.ml index bd6a64b1a3757308297f7eced002b1e9b21a3a60..5c2d0f2010daed75452b3e76d3736d16570784e0 100644 --- a/Src/COLIBRI/simplex_ocaml/ocaml_eclipse.ml +++ b/Src/COLIBRI/simplex_ocaml/ocaml_eclipse.ml @@ -845,18 +845,18 @@ let output_stub filename = let cout = open_out (filename^"_header_include_v5.sexp") in if Sys.word_size = 64 then Printf.fprintf cout - "\"-I%s/ECLiPSe_5.10/include/x86_64_%s/\"" eclipsebin os + "\"-I%s/include/x86_64_%s/\"" eclipsebin os else Printf.fprintf cout - "\"-I%s/ECLiPSe_5.10/include/i386_%s/\"" eclipsebin os; + "\"-I%s/nclude/i386_%s/\"" eclipsebin os; close_out cout; let cout = open_out (filename^"_header_include_v7.sexp") in if Sys.word_size = 64 then Printf.fprintf cout - "\"-I%s/ECLIPSE_V7.0_45/include/x86_64_%s/\"" eclipsebin os + "\"-I%s/include/x86_64_%s/\"" eclipsebin os else Printf.fprintf cout - "\"-I%s/ECLIPSE_V7.0_45/include/i386_%s/\"" eclipsebin os; + "\"-I%s/include/i386_%s/\"" eclipsebin os; close_out cout; @@ -864,9 +864,9 @@ let output_stub filename = if os = "nt" then if Sys.word_size = 64 then Printf.fprintf cout - "(\"-L%s/ECLiPSe_5.10/lib/x86_64_nt/\" -leclipse)" eclipsebin + "(\"-L%s/lib/x86_64_nt/\" -leclipse)" eclipsebin else Printf.fprintf cout - "(\"-L%s/ECLiPSe_5.10/lib/i386_nt/\" -leclipse)" eclipsebin + "(\"-L%s/lib/i386_nt/\" -leclipse)" eclipsebin else Printf.fprintf cout "()"; @@ -874,9 +874,9 @@ let output_stub filename = if os = "nt" then if Sys.word_size = 64 then Printf.fprintf cout - "(\"-L%s/ECLIPSE_V7.0_45/lib/x86_64_nt/\" -leclipse)" eclipsebin + "(\"-L%s/lib/x86_64_nt/\" -leclipse)" eclipsebin else Printf.fprintf cout - "(\"-L%s/ECLIPSE_V7.0_45/lib/i386_nt/\" -leclipse)" eclipsebin + "(\"-L%s/lib/i386_nt/\" -leclipse)" eclipsebin else Printf.fprintf cout "()"; diff --git a/bundle.sh b/bundle.sh index e7794ce18c52379ad64b4b3029d6e613e073ffcc..de74b8708dbbdd46205df6cd71e3735f8edd1bef 100755 --- a/bundle.sh +++ b/bundle.sh @@ -1,12 +1,13 @@ #!/bin/sh -rm -fr bundle -mkdir -p bundle/COLIBRI/lib/ +PREFIX=$1 +rm -fr $PREFIX +mkdir -p $PREFIX/COLIBRI/lib/ -cp -ra Bin/ECLIPSE_V7.0_45/ bundle/ECLIPSE/ -cp -ra Src/COLIBRI/lib/v7 bundle/COLIBRI/lib/ -cp -ra Src/COLIBRI/col_solve.eco Src/COLIBRI/filter_smtlib_file Src/COLIBRI/filter_smtlib_file.exe bundle/COLIBRI/ -cp -ra compile_flag.pl bundle/COLIBRI/ -cp -ra version bundle -cp -ra colibri_for_bundle.sh bundle/colibri -chmod u+x bundle/colibri +cp -ra Bin/ECLIPSE_V7.0_45/ $PREFIX/ECLIPSE/ +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 +cp -ra colibri_for_bundle.sh $PREFIX/colibri +chmod u+x $PREFIX/colibri