From 066076557fa3dc7ade8324f559f61e6ff05b1420 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Mon, 25 Oct 2021 05:21:02 -0400 Subject: [PATCH] Add post-install testing for ocaml binding. (#5617) * Add path flags for cc loader (linux). * Fix os linking and loading problem (maybe on #4840). * Add post-install test of OCaml binding on ubuntu. * Minor. * Tentative CI for macos. --- azure-pipelines.yml | 86 +++++++++++++++++++++++++++++++++++++++++++-- scripts/mk_util.py | 45 ++++++++++++++++++++++-- 2 files changed, 126 insertions(+), 5 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index ee00013857d..e805c4a2c7f 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -44,28 +44,74 @@ jobs: - template: scripts/test-regressions.yml - job: "Ubuntu20OCaml" - displayName: "Ubuntu 20 with ocaml" + displayName: "Ubuntu 20 with OCaml" pool: vmImage: "Ubuntu-20.04" steps: - script: sudo apt-get install ocaml opam libgmp-dev - script: opam init -y - script: eval `opam config env`; opam install zarith ocamlfind -y - - script: eval `opam config env`; python scripts/mk_make.py --ml --staticlib + - script: eval `opam config env`; python scripts/mk_make.py --ml - script: | set -e cd build - eval `opam config env` + eval `opam config env` make -j3 make -j3 examples make -j3 test-z3 + ./ml_example.byte ./ml_example cd .. + - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.* + - script: | + set -e + cd build + eval `opam config env` + make -j3 + make -j3 _ex_ml_example_post_install + ./ml_example_shared.byte + ./ml_example_shared_custom.byte + ./ml_example_shared + cd .. - template: scripts/test-z3.yml - template: scripts/test-regressions.yml - template: scripts/generate-doc.yml +- job: "Ubuntu20OCamlStatic" + displayName: "Ubuntu 20 with OCaml on z3-static" + pool: + vmImage: "Ubuntu-20.04" + steps: + - script: sudo apt-get install ocaml opam libgmp-dev + - script: opam init -y + - script: eval `opam config env`; opam install zarith ocamlfind -y + - script: eval `opam config env`; python scripts/mk_make.py --ml --staticlib + - script: | + set -e + cd build + eval `opam config env` + make -j3 + make -j3 examples + make -j3 test-z3 + ./ml_example.byte + ./ml_example + cd .. + - script: eval `opam config env`; ocamlfind install z3-static build/api/ml/* build/libz3-static.a + - script: | + set -e + cd build + eval `opam config env` + make -j3 + make -j3 _ex_ml_example_post_install + ./ml_example_static.byte + ./ml_example_static_custom.byte + ./ml_example_static + cd .. + - template: scripts/test-z3.yml + - template: scripts/test-regressions.yml + - template: scripts/generate-doc.yml + - job: "LinuxMSan" displayName: "Ubuntu build - cmake" condition: eq(0,1) @@ -252,3 +298,37 @@ jobs: # - template: scripts/test-examples-cmake.yml - template: scripts/test-regressions.yml # - template: scripts/test-java-cmake.yml + + +- job: "MacOSOCaml" + displayName: "MacOS build with OCaml" + pool: + vmImage: "macOS-latest" + steps: + - script: brew install opam + - script: opam init -y + - script: eval `opam config env`; opam install zarith ocamlfind -y + - script: eval `opam config env`; python scripts/mk_make.py --ml + - script: | + set -e + cd build + make -j3 + make -j3 examples + make -j3 test-z3 + ./ml_example.byte + ./ml_example + cd .. + - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.* + - script: | + set -e + cd build + eval `opam config env` + make -j3 + make -j3 _ex_ml_example_post_install + ./ml_example_shared.byte + ./ml_example_shared_custom.byte + ./ml_example_shared + cd .. +# Skip as dead-slow in debug mode: +# - template: scripts/test-z3.yml + - template: scripts/test-regressions.yml \ No newline at end of file diff --git a/scripts/mk_util.py b/scripts/mk_util.py index baa00b1912f..8f664b942cb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2013,9 +2013,12 @@ def mk_makefile(self, out): LIBZ3 = z3linkdep LIBZ3 = LIBZ3 + ' ' + ' '.join(map(lambda x: '-cclib ' + x, LDFLAGS.split())) + + stubs_install_path = '$$(%s printconf path)/stublibs' % OCAMLFIND if not STATIC_LIB: - dllpath = '-dllpath $$(%s printconf path)/stublibs' % OCAMLFIND - LIBZ3 = LIBZ3 + ' ' + dllpath + loadpath = '-ccopt -L' + stubs_install_path + dllpath = '-dllpath ' + stubs_install_path + LIBZ3 = LIBZ3 + ' ' + loadpath + ' ' + dllpath if DEBUG_MODE and not(is_cygwin()): # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well. @@ -2036,6 +2039,9 @@ def mk_makefile(self, out): out.write('\n') out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) + if IS_OSX: + out.write('\tinstall_name_tool -id libz3.dylib %s/libz3.dylib libz3.dylib\n' % (stubs_install_path)) + out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path)) out.write('\n') if IS_WINDOWS: @@ -2294,6 +2300,41 @@ def mk_makefile(self, out): out.write('\n') out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name) + debug_opt = '-g ' if DEBUG_MODE else '' + + if STATIC_LIB: + opam_z3_opts = '-thread -package z3-static -linkpkg' + ml_post_install_tests = [ + (OCAMLC, 'ml_example_static.byte'), + (OCAMLC + ' -custom', 'ml_example_static_custom.byte'), + (OCAMLOPT, 'ml_example_static$(EXE_EXT)') + ] + else: + opam_z3_opts = '-thread -package z3 -linkpkg' + ml_post_install_tests = [ + (OCAMLC, 'ml_example_shared.byte'), + (OCAMLC + ' -custom', 'ml_example_shared_custom.byte'), + (OCAMLOPT, 'ml_example_shared$(EXE_EXT)') + ] + + for ocaml_compiler, testname in ml_post_install_tests: + out.write(testname + ':') + for mlfile in get_ml_files(self.ex_dir): + out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) + out.write('\n') + out.write('\tocamlfind %s -o %s %s %s ' % (ocaml_compiler, debug_opt, testname, opam_z3_opts)) + for mlfile in get_ml_files(self.ex_dir): + out.write(' %s/%s' % (self.to_ex_dir, mlfile)) + out.write('\n') + + if STATIC_LIB: + out.write('_ex_ml_example_post_install: ml_example_static.byte ml_example_static_custom.byte ml_example_static$(EXE_EXT)\n') + else: + out.write('_ex_ml_example_post_install: ml_example_shared.byte ml_example_shared_custom.byte ml_example_shared$(EXE_EXT)\n') + + out.write('\n') + + class PythonExampleComponent(ExampleComponent): def __init__(self, name, path): ExampleComponent.__init__(self, name, path)