diff --git a/README.rst b/README.rst index c0eb8eb..65bd176 100644 --- a/README.rst +++ b/README.rst @@ -2,7 +2,7 @@ ``z3.wasm`` ============= -This repo contains a build script to compile `Z3 `_ to WebAssembly using `emscripten `_. To make things more reproducible, the entire build happens in a `Vagrant ` VM (but the build script should be fairly platform-agnostic). +This repo contains a build script to compile `Z3 `_ to WebAssembly using `emscripten `_. To make things more reproducible, the build script may be run in a `Vagrant ` VM. Loading Z3 is fairly slow (~15 seconds on Chrome, though less than 1 second on Firefox), but verification typically is within a factor 2 to 5 of native performance. @@ -17,10 +17,15 @@ Install `Vagrant `_, then run this:: vagrant ssh VAGRANT=true /vagrant/z3.sh -A detailed log is written to ``provision.log``, with an outline printed to stdout. The first build can take up to two hours (emscripten requires a custom build of LLVM, Z3 is large, and all of this is running in a VM). - +The first build can take up to two hours (emscripten may require a custom build of LLVM, Z3 is large, and all of this is running in a VM). The output is written to ``z3w.js``, ``z3w.wasm``, ``z3smt2w.js``, and ``z3smt2w.wasm``. +On Debian/Ubuntu systems, you may prefer to run natively (the build will be much faster):: + + BASEDIR="$(pwd)/build/" ./z3.sh + +Some Vagrant configurations can cause clang to crash; in that case, building on a physical machine is the best workaround. + Using the generated code ======================== diff --git a/z3.sh b/z3.sh index 0d975d3..35a4c69 100755 --- a/z3.sh +++ b/z3.sh @@ -33,8 +33,15 @@ # * This script is only know to work on Ubuntu. You can run it locally, but in # that case DO NOT set VAGRANT=true. -: "${BASEDIR:=/vagrant}" : "${VAGRANT:=false}" + +if [ "$VAGRANT" = true ]; then + : "${BASEDIR:=/vagrant}" +else + : "${BASEDIR:=$(pwd)/build}" +fi +mkdir -p "$BASEDIR" + export DEBIAN_FRONTEND=noninteractive export JS_ROOT="$BASEDIR/z3-wasm/" @@ -200,6 +207,8 @@ EMCC_WASM_OPTIONS=( EMCC_Z3_JS_INPUTS=("${Z3_ROOT}/build/z3.bc") EMCC_Z3_SMT2_JS_INPUTS=("${BASEDIR}/z3smt2.c" "${Z3_ROOT}/build/libz3.a") +cd "$Z3_ROOT" + say '* Z3: Linking (slow!)'; { cp "${Z3_ROOT}/build/z3" "${Z3_ROOT}/build/z3.bc" # emcc "${EMCC_Z3_OPTIONS[@]}" "${EMCC_Z3_JS_INPUTS[@]}" -o z3.js @@ -213,5 +222,5 @@ say '* Z3 smt2 client: Linking (slow!)'; { say "" say '*********************************' -say '*** Setup complete ***' +say '*** Build complete ***' say '*********************************'