Skip to content

Commit

Permalink
build: Set BASEDIR automatically based on VAGRANT
Browse files Browse the repository at this point in the history
  • Loading branch information
cpitclaudel committed Apr 15, 2018
1 parent dbae91a commit 1353721
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 5 deletions.
11 changes: 8 additions & 3 deletions README.rst
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
``z3.wasm``
=============

This repo contains a build script to compile `Z3 <https://github.com/Z3Prover/z3/>`_ to WebAssembly using `emscripten <https://github.com/kripken/emscripten/>`_. To make things more reproducible, the entire build happens in a `Vagrant <https://www.vagrantup.com/>` VM (but the build script should be fairly platform-agnostic).
This repo contains a build script to compile `Z3 <https://github.com/Z3Prover/z3/>`_ to WebAssembly using `emscripten <https://github.com/kripken/emscripten/>`_. To make things more reproducible, the build script may be run in a `Vagrant <https://www.vagrantup.com/>` 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.

Expand All @@ -17,10 +17,15 @@ Install `Vagrant <https://www.vagrantup.com/>`_, 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
========================

Expand Down
13 changes: 11 additions & 2 deletions z3.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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/"
Expand Down Expand Up @@ -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
Expand All @@ -213,5 +222,5 @@ say '* Z3 smt2 client: Linking (slow!)'; {

say ""
say '*********************************'
say '*** Setup complete ***'
say '*** Build complete ***'
say '*********************************'

0 comments on commit 1353721

Please sign in to comment.