Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

wasm: increase memory and attempt to GC in tests #7400

Merged
merged 1 commit into from
Sep 25, 2024

Conversation

bakkot
Copy link
Contributor

@bakkot bakkot commented Sep 25, 2024

Attempt to fix #7399.

Just forcing GC or increasing memory size to 2GB alone are each insufficient, but in combination tests pass again at least on my machine. This is not an elegant solution but hopefully at least un-breaks the build. I can try to experiment with newer versions of emscripten or a different test runner if I have time later.

@NikolajBjorner
Copy link
Contributor

Something different is happening. It times out in "can do simple proofs".
I would merge this PR even if it doesn't run to completion because it looks easier to fix than the original code.

@NikolajBjorner NikolajBjorner merged commit 103c5ad into Z3Prover:master Sep 25, 2024
11 of 15 checks passed
@NikolajBjorner
Copy link
Contributor

I get the following now in code spaces:

● Test suite failed to run

RuntimeError: Aborted('PThread' was not exported. add it to EXPORTED_RUNTIME_METHODS (see the Emscripten FAQ))

  887 |   // TODO(https://github.com/google/closure-compiler/pull/3913): Remove if/when upstream closure gets fixed.
  888 |   /** @suppress {checkTypes} */
> 889 |   var e = new WebAssembly.RuntimeError(what);
      |           ^
  890 |
  891 |   readyPromiseReject(e);
  892 |   // Throw the error whether or not MODULARIZE is set because abort is used

  at abort (build/z3-built.js:889:11)
  at Object.get (build/z3-built.js:1200:9)
  at killThreads (src/jest.ts:51:6)
  at Object.<anonymous> (src/high-level/high-level.test.ts:88:22)

Test Suites: 1 failed, 1 passed, 2 total
Tests: 39 passed, 39 total
Snapshots: 0 total
Time: 46.001 s
Ran all test suites.
@NikolajBjorner ➜ .../z3/src/api/js (master) $

@bakkot bakkot deleted the gc-js-tests branch September 25, 2024 15:58
@bakkot
Copy link
Contributor Author

bakkot commented Sep 25, 2024

For code spaces, my guess is that the version of emscripten in code spaces is newer than the version in CI. If you do emsdk install 3.1.15 && emsdk activate 3.1.15 does that fix it?

I should update the emscripten version used in CI; it's way behind. But your experience suggests there have been some breaking changes so this might not happen right away.

NikolajBjorner added a commit that referenced this pull request Sep 27, 2024
@bakkot bakkot mentioned this pull request Dec 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

WASM bindings are broken
2 participants