diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6e440b8ad483aa2d14618715cd2cf5fb2d76af7d..9705777798f25c0de0dc5a08b1510bed2eb6f39d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,6 +4,8 @@ tests_without_recompilation:
#Eclipse Prolog compilation of COLIBRI
- ./compile_colibri.sh
#Bundle in bundle directory
+ - apt-get update
+ - apt-get install -y ocaml-nox
- ./bundle.sh bundle
- cp -ra Bin/ECLIPSE_V7.0_45/ bundle/ECLIPSE/
#Test
diff --git a/bundle.sh b/bundle.sh
index e3b8b8369aa6533f652d438fc5add59d7716e25e..533d1dad625ce6839e6f1c772bb53339e1e0aaaa 100755
--- a/bundle.sh
+++ b/bundle.sh
@@ -8,5 +8,6 @@ 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
+ocamlopt unix.cmxa -o $PREFIX/colibri.exe colibri_for_bundle.ml
+cp $PREFIX/colibri.exe $PREFIX/colibri
chmod u+x $PREFIX/colibri
diff --git a/colibri_for_bundle.ml b/colibri_for_bundle.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fe7a483ef72aa2cbfa0b1e1c36a88ac00831ffd9
--- /dev/null
+++ b/colibri_for_bundle.ml
@@ -0,0 +1,118 @@
+let coldir = Filename.dirname Sys.executable_name
+
+let conf = ref "true"
+let memlimit = ref 3000
+let interpreter = ref false
+let get_steps = ref false
+let max_steps = ref 0
+let exec_cmd = ref ""
+
+let goal = ref ""
+
+let path_sep = if Sys.win32 then ";" else ":"
+
+let print_version () =
+ let cin = open_in (Filename.concat coldir "version") in
+ let s = input_line cin in
+ close_in cin;
+ Printf.printf "%s%!" s;
+ exit 0
+
+let add_to_conf s =
+ conf := (!conf)^","^s
+
+let argspec =
+ ["--version", Arg.Unit print_version, " print version";
+ "--memlimit", Arg.Set_int memlimit, " set memlimit in Megabyte (default 3000)";
+ "--conf", Arg.String add_to_conf, " evaluate the prolog expression (default true)";
+ "--per-call-simplex-timeout",
+ Arg.Int (fun sec -> add_to_conf (Printf.sprintf "set_simplex_timeout(%i)" sec)) ,
+ " timeout for each call of the rational simplex";
+ "--delay-simplex-deactivation",
+ Arg.Int (fun sec -> add_to_conf (Printf.sprintf "setval(simplex_delay_deactivation,%i)" sec)),
+ " stop delta and simplex algorithm after the given time (0 always activated)";
+ "--external-simplex",
+ Arg.Symbol (["z3";"z3-debug"],
+ (fun s -> Unix.putenv "COLIBRI_USE_SOLVER" s;
+ let path = (try Unix.getenv "PATH" with Not_found -> "") in
+ Unix.putenv "PATH" ((Filename.concat coldir "qf_lra_solver")^path_sep^path)
+ )),
+ " use the specified external solver \
+ (QF_LRA) instead of internal simplex \
+ acceptable values are (z3, z3-debug \
+ -- prints z3 inputs outputs to \
+ /tmp/{input,output}.smt2)";
+ "--get-steps", Arg.Set get_steps,
+ " output the number of steps at the end";
+ "--max-steps", Arg.Set_int max_steps,
+ " limit the number of steps";
+ "--interpreter-mode", Arg.Set interpreter,
+ " run the prolog interactive interpreter";
+ "--exec", Arg.Set_string exec_cmd,
+ " exec a command in interpreter mode"
+ ]
+
+let () = Arg.parse (Arg.align argspec)
+ (fun s -> goal := s)
+ "colibri <file>"
+
+let () = if !goal = "" then begin
+ print_endline "No input file given.";
+ exit 1
+ end
+
+let eclipsedir = Filename.concat coldir "ECLIPSE"
+let eclipselib = Filename.concat eclipsedir "lib"
+let colibridir = Filename.concat coldir "COLIBRI"
+
+let arch = if Sys.win32 then "x86_64_nt" else "x86_64_linux"
+
+let () = Unix.putenv "ECLIPSEDIR" eclipsedir
+let () = Unix.putenv "FILTER_SMTLIB_FILE" (Filename.concat colibridir "filter_smtlib_file")
+let () = Unix.putenv "ARCH" arch
+
+let extend_env var value =
+ match Unix.getenv var with
+ | exception Not_found -> Unix.putenv var value
+ | s -> Unix.putenv var (value^path_sep^s)
+
+let eclipseexe = Filename.concat eclipselib arch
+
+let () =
+ if Sys.win32
+ then begin
+ extend_env "PATH" eclipseexe;
+ extend_env "PATH" colibridir;
+ extend_env "PATH" (List.fold_left Filename.concat colibridir ["lib";"v7";arch])
+ end
+ else
+ extend_env "LD_LIBRARY_PATH" eclipseexe
+
+let quote_for_prolog f =
+ let s = Printf.sprintf "%S" f in
+ Printf.sprintf "'%s'" (String.sub s 1 (String.length s - 2))
+
+let () =
+ let exe = Filename.concat eclipseexe "eclipse.exe" in
+ Unix.execv exe
+ (Array.concat
+ [
+ [| exe;
+ "-b"; Filename.concat colibridir "compile_flag";
+ "-b"; Filename.concat colibridir "col_solve";
+ "-g"; Printf.sprintf "%iM" !memlimit;
+ |];
+ (if !exec_cmd = ""
+ then [| |]
+ else [| "-e"; !exec_cmd |])
+ ;
+ (if !interpreter
+ then [| |]
+ else [| "-e"; Printf.sprintf
+ "seed(0),%s,smt_solve%s(%s)"
+ !conf
+ (if !get_steps then "_stats" else "")
+ (quote_for_prolog !goal)
+ |])
+ ]
+ )
diff --git a/compile_colibri.bat b/compile_colibri.bat
new file mode 100644
index 0000000000000000000000000000000000000000..0291022769f8389203c07fa104950e68e23d548c
--- /dev/null
+++ b/compile_colibri.bat
@@ -0,0 +1,10 @@
+@echo off
+
+set COLDIR=%~dp0
+set ECLIPSEDIR=%~dpnx1
+set PATH=%COLDIR%Src\COLIBRI;%COLDIR%Src\COLIBRI\lib\v7\x86_64_nt;%PATH%
+
+cd Src\COLIBRI
+
+@echo on
+"%ECLIPSEDIR%\lib\x86_64_nt\eclipse.exe" -g 3000M -b col_solve_dumpeco.pl -e halt
diff --git a/compile_colibri.sh b/compile_colibri.sh
index fa63f532c2a166585d8b231e6751156df844ea1f..d55a69de35921fb54512dad86916b0586a2468ec 100755
--- a/compile_colibri.sh
+++ b/compile_colibri.sh
@@ -2,7 +2,7 @@
ARCH="x86_64_linux"
ECLIPSEDIR=$(pwd)/Bin/ECLIPSE_V7.0_45
-LD_LIBRARY_PATH="$ECLIPSEDIR/lib/$ARCH"
+LD_LIBRARY_PATH="$ECLIPSEDIR/lib/$ARCH:$LD_LIBRARY_PATH"
export ARCH ECLIPSEDIR LD_LIBRARY_PATH
diff --git a/merlin b/merlin
new file mode 100644
index 0000000000000000000000000000000000000000..52bfc359750cc638cdb51408099c13c9c70f02f4
--- /dev/null
+++ b/merlin
@@ -0,0 +1 @@
+PKG unix