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

Link error on WASM assembly in api/js #6518

Closed
zkbitcoin opened this issue Jan 2, 2023 · 1 comment
Closed

Link error on WASM assembly in api/js #6518

zkbitcoin opened this issue Jan 2, 2023 · 1 comment

Comments

@zkbitcoin
Copy link

zkbitcoin commented Jan 2, 2023

Note: (single threaded flag, it is just not part of README, maybe it can be added there somehow then this open task closed)

this succeeds:

export CXXFLAGS="-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0"
export LDFLAGS="-pthread -s USE_PTHREADS=1"
emconfigure python scripts/mk_make.py --staticlib --single-threaded
cd build
emmake make -j$(nproc)


assembled static library

cmake -DZ3_BUILD_LIBZ3_SHARED=false -G "Unix Makefiles" ../
make

then in api/js

npm i
npm run build:ts
npm run build:wasm

Errors: (shown few lines for brevity).

also tried both master and z3-4.11.2

emcc: warning: ../../../build/libz3.a: archive is missing an index; Use emar when creating libraries to ensure an index is created [-Wemcc]
emcc: warning: ../../../build/libz3.a: adding index [-Wemcc]
error: undefined symbol: Z3_algebraic_eval (referenced by top-level compiled C/C++ code)
warning: Link with -sLLD_REPORT_UNDEFINED to get more information on undefined symbols
warning: To disable errors for undefined symbols use -sERROR_ON_UNDEFINED_SYMBOLS=0
warning: _Z3_algebraic_eval may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: Z3_algebraic_roots (referenced by top-level compiled C/C++ code)
warning: _Z3_algebraic_roots may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: Z3_eval_smtlib2_string (referenced by top-level compiled C/C++ code)
warning: _Z3_eval_smtlib2_string may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: Z3_fixedpoint_query (referenced by top-level compiled C/C++ code)
warning: _Z3_fixedpoint_query may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: Z3_fixedpoint_query_from_lvl (referenced by top-level compiled C/C++ code)
warning: _Z3_fixedpoint_query_from_lvl may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library

@zkbitcoin
Copy link
Author

this makes the wasm to compile

export CXXFLAGS="-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0"
export LDFLAGS="-pthread -s USE_PTHREADS=1"
emconfigure python scripts/mk_make.py --staticlib --single-threaded
cd build
emmake make -j$(nproc)

NikolajBjorner added a commit that referenced this issue Jan 3, 2023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
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

No branches or pull requests

1 participant