TS/JS Bindings - Poor documentation, inconsistent API, ADTs?

[kizerkizer]

The documentation comments, the documentation website, and the code are all saying different things. Is there support for algebraic data types in the JS API? I'm talking about the "high level" API.

Please let me know if you'd like help getting TS to parity with the Python API, which from what I understand is the primary one aside from the C API. Or if you need help keeping docs consistent and updated!

[kizerkizer]

For example, this site https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples/ seems to be running an ancient build of z3js from https://microsoft.github.io/z3guide/z3-built.js.

[bakkot]

The documentation comments, the documentation website, and the code are all saying different things.

Can you be more specific about what differences you're seeing?

Is there support for algebraic data types in the JS API? I'm talking about the "high level" API.

What specifically do you mean by algebraic data types in this context? I don't think of the Python API as having ADTs, so I'm not really sure what you mean here. The high-level API follows the Python API quite closely, except that it's missing a lot of stuff.

Please let me know if you'd like help getting TS to parity with the Python API

Definitely; people have been adding this missing parts incrementally (e.g. #7471, #7426), and there's plenty left to do. I'm happy to review PRs or give comments on the design if you ping me. (I did the original JS/TS implementation.)

this site https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples/ seems to be running an ancient build of z3js

The version on the website is a couple years old, but it's not ancient, and everything it's doing is still supported in newer versions.

[NikolajBjorner]

The version on the website is a couple years old

I prefer to not update this version on the online guide too often to avoid having to deal with inadvertent regressions.

I'm happy to review PRs or give comment

Please add PRs. For extra credit, but I wonder if JS/TS programmers would have moral qualms, there are pyodide bindings in the works. They are not fully reliable yet and figuring out what is the root cause for the issues will require investigation.

[kizerkizer]

I apologize if I came across as curt. I was frustrated in the moment. I was interested in the JS bindings because I wanted to integrate Z3 into a NodeJS app. I hadn't heard of pyodide prior to your reference; perhaps that would work better as the Python API would be the source of truth. Though, it would be nice to have an idiomatic JS api.

I'll check things out and see if I can make a good contribution. Thank you for responding.