-
-
Notifications
You must be signed in to change notification settings - Fork 40
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
(De-)serialize BigInt from/to JSON number in Quint import #2661
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I assume the two json files are generated by something, so I didn't read them. The rest looks good.
Aaah yes, that's the revert commit. Thanks! |
We override the upickle implementation, which only (de-)serializes from/to strings.
This reverts commit 3f6bb18.
9f08cea
to
ece1090
Compare
Codecov Report
@@ Coverage Diff @@
## main #2661 +/- ##
==========================================
- Coverage 78.55% 78.50% -0.05%
==========================================
Files 455 455
Lines 15795 15817 +22
Branches 2589 2570 -19
==========================================
+ Hits 12407 12417 +10
- Misses 3388 3400 +12
... and 3 files with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome work! Glad to have the root cause sorted out :)
#2654 fixed the deserialization of
QuintInt.value
into a Scala BigInt.However, this is not the only TypeScript
bigint
needing conversion:All Quint IDs, plus the lookup table references, are also TypeScript bigints and should be deserialized into Scala BigInts.
upickle's built-in
BigInt
(de)serializer reads/writes BigInts only from/to JSON strings.Thus, there's two options for Apalache <-> Quint compatiblity:
bigint
s as strings from Quint.json-bigint
already behaves on the Quint side.A brief investigation showed that approach (1) is non-trivial; for example, it would break the JSON re-import inside Quint.
This PR implements approach (2):
QuintDeserializer
with customBigInt{Reader,Writer}
implicits to read/write JSON numbers.QuintInt.value
s in integration tests into strings as part of DeserializeQuintInt.value
asBigInt
#2654. Since we now read/write JSON numbers, this has become unnecessary.Closes informalsystems/quint#1055
make fmt-fix
(or had formatting run automatically on all files edited)Documentation added for any new functionality./unreleased/
for any new functionality