-
Notifications
You must be signed in to change notification settings - Fork 3.5k
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
[Bug][move-compiler-v2] move-prover tests timeout more with MOVE_COMPILER_V2=true after PR#13184 #13186
Comments
@rahxephon89 fyi |
@wrwg fyi |
This issue originally also mentioned a different test output difference that appeared after PR#13184, but this has been removed from the issue summary after some more study. Here is a little discussion: The first error mentioned related to some checks for modules with identical names if letter case is ignored:
This seems to be a harmless difference. Firstly, it's not clear what is the motivation for this concern, but as a build of a package produces a file The detailed change here is captured by he following diff:
The difference comes down to the use of script functions, and their potential conflict with modules due to case insensitivity. This shouldn't be an issue with V2 as scripts and functions are canonicalized. I'm renaming this issue and changing the summary to focus on the move-prover timeouts with MOVE_COMPILER_V2. |
Hi @brmataptos, I tried using |
If you undo the fix mentioned above in fixed_point32.move
then you can see timeouts in several tests. Actually, even with that fix we see timeouts in some
but I'm unfamiliar with how to debug this situation. How can I see the full boogie input/output for these test cases (e.g., for V1 and V2)? Are there "debugging move-prover" best practices that could be shared in our doc? |
Fixed by #13270 |
🐛 Bug
PR #13184 fixes many things but seems to increase timeouts in move-prover tests with MOVE_COMPILER_V2=true. This is likely due to attempts to prove things about library dependencies, since the timeouts were accompanied by poiters to the function
std::fixed_point32::round()
, although the exact cause is unclear. This was temporarily worked around by the following change to move-stdlib:This needs more investigation. It seems likely that the assignment of input files to "primary target sources", "non-primary target sources" and "dependences" is somehow incorrect in the move-prover case.
The text was updated successfully, but these errors were encountered: