3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 06:16:09 +00:00

Allow JS/WASM init to accept Deno-friendly wasm load paths (#9621)

The JS bindings currently assume the wasm can be located via the default
Emscripten path resolution, which can force Deno users into
`--allow-read`. This change lets callers provide a custom wasm load path
through `init(...)`, so Deno can resolve the packaged wasm asset without
filesystem reads.

- **Public init API**
- Extend the JS entrypoints (`node` and `browser`) so `init(...)`
accepts optional Emscripten module overrides.
- Surface a typed `Z3ModuleOverrides` shape with explicit support for
`locateFile(path, prefix)`.

- **Low-level initialization**
- Thread module overrides through the generated low-level wrapper
instead of always calling the Emscripten module factory with no
arguments.
  - Keep the default behavior unchanged when no overrides are provided.

- **Docs**
  - Document the Deno usage pattern in the published JS README.
- Clarify the `locateFile` signature and show the intended Deno 2.1+
`import.meta.resolve(...)` flow.

- **Focused coverage**
- Add unit tests for `node` and `browser` init to verify module
overrides are forwarded correctly.

Example:

```ts
import { init } from 'npm:z3-solver';

const api = await init({
  locateFile: (file, _prefix): string =>
    import.meta.resolve(`npm:z3-solver/build/${file}`),
});
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-05-26 14:02:04 -07:00 committed by GitHub
parent 2d827af322
commit 91205d2f60
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 110 additions and 8 deletions

View file

@ -16,6 +16,17 @@ const {
This package has different initialization for browser and node. Your bundler and node should choose good version automatically, but you can import the one you need manually - `const { init } = require('z3-solver/node');` or `const { init } = require('z3-solver/browser');`.
The `init` function also accepts an optional Emscripten module overrides object. This is useful in runtimes such as Deno where you may want to provide a wasm load path explicitly instead of relying on filesystem reads. In Deno 2.1+, `import.meta.resolve(...)` returns a string synchronously, so it can be used directly in `locateFile`. For example:
```typescript
import { init } from 'npm:z3-solver';
const api = await init({
locateFile: (file, _prefix): string =>
import.meta.resolve(`npm:z3-solver/build/${file}`), // _prefix is unused here
});
```
### Limitations
The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications.