Skip to content

Latest commit

 

History

History
13 lines (9 loc) · 1.43 KB

web.md

File metadata and controls

13 lines (9 loc) · 1.43 KB
Raw

How the web build works

The rules attached to the @web alias show how everything is put together:

  • examples.sh is used to embed the examples in index.html.
  • The npm package for Z3 is assumed to be installed. The wasm part of it is copied out to be included directly in the page. To work around WebAssembly SharedBuffer issues, coi-serviceworker.min.js is fetched and included in the page.
  • The OCaml code is compiled into hipjs.bc.js. On being included, the ocaml_ready function is set globally.
  • main.js is the driver which initializes Z3 and the OCaml code, and exposes a solve function wrapping Z3 globally, for the OCaml code to use.
  • main.js and the JS stubs of the Z3 package are bundled by browserify, due to the need to use client-side require in the latter
  • page.js handles user interactions and configures Ace

Z3's native API is synchronous, but its web API is asynchronous. An algebraic effect is used to allow both to have a synchronous interface. js_of_ocaml is thus invoked with --enable=effects, and the JS version of Heifer suspends upon every Z3 call, resuming then it finishes.