diff --git a/.gitignore b/.gitignore index 1ae0b45..0292168 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,8 @@ -/z3-wasm/ /.vagrant/ -/provision.log -/html/z3w.wasm -/html/z3w.js +/build/ /dist/ +/html/z3w.js +/html/z3w.wasm +/provision.log +/upload.sh /z3.wasm.tar.gz diff --git a/README.rst b/README.rst index 65bd176..983ae98 100644 --- a/README.rst +++ b/README.rst @@ -11,20 +11,24 @@ Pre-build archives are available at https://github.com/cpitclaudel/z3.wasm/relea Building ======== +In a VM +------- + Install `Vagrant `_, then run this:: vagrant up vagrant ssh VAGRANT=true /vagrant/z3.sh -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``. +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 (``z3w.js``, ``z3w.wasm``, ``z3smt2w.js``, and ``z3smt2w.wasm``) is written to ``build/z3/``. -On Debian/Ubuntu systems, you may prefer to run natively (the build will be much faster):: +Some Vagrant configurations can cause clang to crash or Vagrant to hang. +Building on a physical machine is the most reliable workaround. - BASEDIR="$(pwd)/build/" ./z3.sh +Natively +-------- -Some Vagrant configurations can cause clang to crash; in that case, building on a physical machine is the best workaround. +On Debian/Ubuntu systems, you may prefer to build natively, which will be much faster. In that case, just run ``./z3.sh``, which will place all outputs in ``build/``. Using the generated code ======================== @@ -61,7 +65,7 @@ From a webpage the process is roughly the same: write Z3's input to a file using This is all demoed in ``html/z3.html`` (that example also uses a WebWorker to run Z3, keeping the page responsive while it runs). Try it like this:: - cp z3-wasm/z3/z3w.js z3-wasm/z3/z3w.wasm ./html + cp build/z3/z3w.js build/z3/z3w.wasm ./html python3 -m http.server # Open your browser to http://localhost:8000/html/z3.html diff --git a/dist.sh b/dist.sh index e46b407..bad67ca 100755 --- a/dist.sh +++ b/dist.sh @@ -3,5 +3,5 @@ rm -rf dist/ html/z3*w.* mkdir dist cp html/* dist/ cp README.dist.rst dist/README.rst -cp z3-wasm/z3/z3smt2w.js z3-wasm/z3/z3smt2w.wasm z3-wasm/z3/z3w.js z3-wasm/z3/z3w.wasm dist/ +cp build/z3/z3smt2w.js build/z3/z3smt2w.wasm build/z3/z3w.js build/z3/z3w.wasm dist/ tar --create --gzip --file z3.wasm.tar.gz --transform 's|^dist|z3.wasm|' dist diff --git a/z3.sh b/z3.sh index 35a4c69..658913f 100755 --- a/z3.sh +++ b/z3.sh @@ -22,13 +22,11 @@ # Notes: # -# * If you see an error like this: +# * If you see an error like this, upgrade to a more recent Ubuntu box: # -# /vagrant/z3-wasm/emsdk-portable/clang/e1.37.36_64bit/llc: +# /vagrant/build/emsdk-portable/clang/e1.37.36_64bit/llc: # /usr/lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.20' not -# found (required by /vagrant/z3-wasm/emsdk-portable/clang/e1.37.36_64bit/llc) -# -# Then upgrade to a more recent Ubuntu box +# found (required by /vagrant/build/emsdk-portable/clang/e1.37.36_64bit/llc) # # * This script is only know to work on Ubuntu. You can run it locally, but in # that case DO NOT set VAGRANT=true. @@ -36,20 +34,16 @@ : "${VAGRANT:=false}" if [ "$VAGRANT" = true ]; then - : "${BASEDIR:=/vagrant}" + : "${BASEDIR:=/vagrant/}" else - : "${BASEDIR:=$(pwd)/build}" + : "${BASEDIR:=$(pwd)/}" fi -mkdir -p "$BASEDIR" - -export DEBIAN_FRONTEND=noninteractive - -export JS_ROOT="$BASEDIR/z3-wasm/" -export Z3_ROOT="${JS_ROOT}z3/" -export EMSDK_ROOT="${JS_ROOT}emsdk-portable/" -export EMSCRIPTEN_TEMPDIR="/tmp/emscripten" export OPTLEVEL=3 +export BUILDDIR="${BASEDIR}build/" +export Z3_ROOT="${BUILDDIR}z3/" +export EMSDK_ROOT="${BUILDDIR}emsdk-portable/" +export EMSCRIPTEN_TEMPDIR="/tmp/emscripten/" function say() { printf "\033[1;32m%s\033[0m\n" "$1" @@ -60,6 +54,8 @@ say '*********************************' say '*** Installing dependencies ***' say '*********************************' +export DEBIAN_FRONTEND=noninteractive + say '* apt-get update'; { sudo apt-get -y -q update } @@ -86,12 +82,12 @@ say '*******************' say '*** Downloading ***' say '*******************' -rm -rf "$JS_ROOT" -mkdir "$JS_ROOT" +rm -rf "$BUILDDIR" +mkdir "$BUILDDIR" say '* wget emscripten'; { wget --quiet -O /tmp/emsdk-portable.tar.gz https://s3.amazonaws.com/mozilla-games/emscripten/releases/emsdk-portable.tar.gz - tar -xf /tmp/emsdk-portable.tar.gz -C "$JS_ROOT" + tar -xf /tmp/emsdk-portable.tar.gz -C "$BUILDDIR" } say '* git clone z3'; { @@ -129,7 +125,7 @@ say '* Emscripten: setup'; { # Don't source emsdk_env directly, as it produces output that can't be logged # without creating a subshell (which would break `source`) -source "${EMSDK_ROOT}/emsdk_set_env.sh" +source "${EMSDK_ROOT}emsdk_set_env.sh" # emcc fails in all sorts of weird ways without this ulimit -s unlimited @@ -138,8 +134,7 @@ say '* Emscripten: stdlib (very slow!)'; { mkdir -p "$EMSCRIPTEN_TEMPDIR" cd "$EMSCRIPTEN_TEMPDIR" printf '#include\nint main() { return 0; }\n' > minimal.c - # Adding to emcc here causes it to crash - emcc -v minimal.c + emcc minimal.c } cd "$Z3_ROOT" @@ -204,13 +199,13 @@ EMCC_WASM_OPTIONS=( # in a WebWorker anyway, so it wouldn't buy us much. -s BINARYEN_ASYNC_COMPILATION=0) -EMCC_Z3_JS_INPUTS=("${Z3_ROOT}/build/z3.bc") -EMCC_Z3_SMT2_JS_INPUTS=("${BASEDIR}/z3smt2.c" "${Z3_ROOT}/build/libz3.a") +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" + cp "${Z3_ROOT}build/z3" "${Z3_ROOT}build/z3.bc" # emcc "${EMCC_Z3_OPTIONS[@]}" "${EMCC_Z3_JS_INPUTS[@]}" -o z3.js emcc "${EMCC_Z3_OPTIONS[@]}" "${EMCC_WASM_OPTIONS[@]}" "${EMCC_Z3_JS_INPUTS[@]}" -o z3w.js } diff --git a/z3smt2test.js b/z3smt2test.js index 85392dd..ada7632 100644 --- a/z3smt2test.js +++ b/z3smt2test.js @@ -18,8 +18,8 @@ // OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE // SOFTWARE -process.chdir("./z3-wasm/z3/"); // To find the WASM file -var Z3Factory = require('./z3-wasm/z3/z3smt2w.js'); +process.chdir("./build/z3/"); // To find the WASM file +var Z3Factory = require('./build/z3/z3smt2w.js'); var z3smt2 = Z3Factory(); var smt2API = { diff --git a/z3test.js b/z3test.js index af78c32..f62e2f0 100644 --- a/z3test.js +++ b/z3test.js @@ -18,8 +18,8 @@ // OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE // SOFTWARE -process.chdir("./z3-wasm/z3/"); // To find the WASM file -var Z3Factory = require("./z3-wasm/z3/z3w.js"); +process.chdir("./build/z3/"); // To find the WASM file +var Z3Factory = require("./build/z3/z3w.js"); var z3 = Z3Factory(); var FS = z3["FS"];