Lean: add matchbv support #1222
Conversation
The only semantic change this PR proposes is to not assert on argument pattern that we cannot yet translate, but instead to record them as `TODO_ARG_PATTERN`. This is sufficient to build the full RISC-V Sail model without assertions and with about 3500 warnings and errors remaining. This PR also introduces a GitHub action to validate that the RISC-V model builds. The RISC-V model currently requires two patches (one in Ryan's repository and one applied through this patch). Over time, we expect to switch to the main RISC-V repo. Co-authored-by: Léo Stefanesco <[email protected]>
|
This superseeds #1182 |
Test Results 13 files 28 suites 0s ⏱️ Results for commit 4421904. ♻️ This comment has been updated with latest results. |
|
I get a super strange universe error in test |
|
There's an |
|
It now has a flag |
test/lean/run_tests.py
Outdated
| 'encdec_subrange', # Deactivated to enable match_bv | ||
| 'option_nest', # Deactivated to enable match_bv | ||
| 'special_annot', # Deactivated to enable match_bv | ||
| 'vector_subrange_pattern' # Deactivated to enable match_bv |
There was a problem hiding this comment.
@ineol, these do not need to be disabled, no? match_bv is disabled by default.
|
Nice. Would it be possible to add a single |
I changed it to run the tests in the |
|
Nice. Then this is good to go. |
|
Merging this will also help to reduce the code size of the arm model, which is important as we hit sie limits at github. |
|
Thanks, will merge once the CI completes. |
No description provided.