Updating to z3-solver version 4.12.0 breaks when evaluating js about z3guide HOT 9 CLOSED

The main change since 4.11.0 that is relevant could be the commit,
Z3Prover/z3@f175fcb
On a frist read it appears to just add some new sub-classes without affecting previous classes.

I am currently not clear how to read the error message
main.ts (-2,45): Type 'any' has no signatures for which the type argument list is applicable.
as the line position -2 should relate to some of the auto-generated code.

from z3guide.

I am currently not clear how to read the error message
main.ts (-2,45): Type 'any' has no signatures for which the type argument list is applicable.

From the error message, the problem is more likely to be the previous line:

Error: main.ts (-5,82): Cannot find module 'z3-solver'.

which indicates that it isn't able to find z3-solver during the build process. I don't see the same error when I try the same process locally (except with yarn upgrade z3-solver --latest in place of yarn update z3-solver --latest; yarn update is not a thing).

The subsequent "Type 'any' has no signatures" error is probably a consequence of not being able to find the module with the types, and doesn't really mean anything on its own (just that it can't compile without having access to the types).

from z3guide.

Like the comment above, I also was able to get Z3 version 4.12.0 working locally, though I had to change my node version to v16.19.0 (the version used by the GitHub build hooks) to fix some other obscure errors of my own. @NikolajBjorner perhaps you could try changing your node version if it isn't 16.19.0 already?

from z3guide.

I guess node exposes something then.

This is on my laptop:
C:\z3guide\website>node -v
v18.13.0

Thanks for the inputs. I will then check on my desktop when I get back home (or push to a branch and check the build machines).

from z3guide.

I tried building it locally with node v16.15.1, which got me a different build error regarding type mismatch in one of the z3-js examples. However, after trying v16.9.0 as what @walnutwaldo suggested, the build was successful. So I can confirm that node was causing the issue.

from z3guide.

update: I was able to get further with codespaces, but not with my Windows machines. This suggests the issue to be external (or a configuration setting that resolves differently on platforms).

from z3guide.

@rlisahuang - could it be that we also have to update z3-solver version in package.json?
https://github.com/microsoft/z3guide/blob/main/website/package.json

I updated it, and then reran yarn (install) to update the lock file. At this point it appears Windows and Linux produce the same errors inside what is likely regressions for 12.1 (not external). The error message just remains very poor on my windows environment compared to what the build provides.

from z3guide.

It is resolved to: package.json has to be synchronized with upgrade.sh

from z3guide.

@rlisahuang - could it be that we also have to update z3-solver version in package.json? https://github.com/microsoft/z3guide/blob/main/website/package.json

I updated it, and then reran yarn (install) to update the lock file. At this point it appears Windows and Linux produce the same errors inside what is likely regressions for 12.1 (not external). The error message just remains very poor on my windows environment compared to what the build provides.

upgrade-z3.sh should rewrite the version number in package.json for z3-solver automatically if the upgrade AND build are both successful. If any of them fail (most likely the build), then it would revert the z3-solver back to the version prior to the upgrade (which would lead to a successful build). The version reverse would be reflected in package.json as well, which could be why you won't see package.json updated automatically after running upgrade-z3.sh if the build after upgrade fails.

from z3guide.