We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Initialization is not working for unboxed types like UInt64 and Bool on compiled code
UInt64
Bool
Start a file like this:
initialize test : UInt64 ← pure 0 def main : IO Unit := IO.println test
Then compile and run it.
Expected behavior:
It should output 0
0
Actual behavior:
It breaks with an error like this:
error: incompatible pointer to integer conversion assigning to 'uint64_t' (aka 'unsigned long') from 'b_lean_obj_res' (aka 'lean_object *') [-Wint-conversion] l_test = lean_io_result_get_value(res); ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1 error generated.
Reproduces how often:
Everytime it's executed as compiled code. Although it works on the kernel.
I'm on Ubuntu. This is the output of lake --version: Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2022-12-16)
lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2022-12-16)
The text was updated successfully, but these errors were encountered:
6eb852e
No branches or pull requests
Description
Initialization is not working for unboxed types like
UInt64
andBool
on compiled codeSteps to Reproduce
Start a file like this:
Then compile and run it.
Expected behavior:
It should output
0
Actual behavior:
It breaks with an error like this:
Reproduces how often:
Everytime it's executed as compiled code. Although it works on the kernel.
Versions
I'm on Ubuntu. This is the output of
lake --version
:Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2022-12-16)
The text was updated successfully, but these errors were encountered: