-
Notifications
You must be signed in to change notification settings - Fork 26
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
Cogent Refinement Proofs fail for RISC-V architecture #387
Comments
I have made changes to the proofs (commit 90f9d19) that should fix this. Could you test this on your code and see if this change helps. Thanks. |
Yes, it seems to help, I was now able to build the CogentCRefinement session for architecture RISCV64. |
A similar problem now occurs later in AllRefine.thy (which I could not test before).
The error message is:
|
When setting L4V_ARCH to RISCV64 instead of ARM, isabelle fails to build the session CogentCRefinement.
The Cogent version was commit 7f8b944... of Oct 29th.
The error occurs in theory Value_Relation.thy
The error message is:
The text was updated successfully, but these errors were encountered: