Skip to content
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

Lean: Make the RISC-V Sail model build #1012

Draft
wants to merge 6 commits into
base: sail2
Choose a base branch
from

Conversation

tobiasgrosser
Copy link
Collaborator

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.

@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 15, 2025
Copy link

github-actions bot commented Feb 15, 2025

Test Results

   13 files     27 suites   0s ⏱️
  821 tests   821 ✅ 0 💤 0 ❌
2 932 runs  2 932 ✅ 0 💤 0 ❌

Results for commit a9936a5.

♻️ This comment has been updated with latest results.

@tobiasgrosser
Copy link
Collaborator Author

Let's keep this as draft, until #1015 is merged.

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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant