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.

Sign up for GitHub

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

Jump to bottom

sail-to-lean: set set_option linter.unusedVariables false (- 1449 warnings) #1011

Closed
tobiasgrosser opened this issue Feb 15, 2025 · 0 comments · Fixed by #1013
Closed

sail-to-lean: set set_option linter.unusedVariables false (- 1449 warnings) #1011

tobiasgrosser opened this issue Feb 15, 2025 · 0 comments · Fixed by #1013
Labels
Lean Issues with Sail to Lean translation

Comments

@tobiasgrosser
Copy link
Collaborator

This should reduce the number of warnings+errors from 3021 to 1562.
@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 15, 2025
@tobiasgrosser tobiasgrosser changed the title sail-to-lean: set 'set_option linter.unusedVariables false` (- 1449 warnings) sail-to-lean: set set_option linter.unusedVariables false (- 1449 warnings) Feb 15, 2025
tobiasgrosser added a commit to opencompl/sail that referenced this issue Feb 15, 2025
@tobiasgrosser
Lean: ignore unused variables
c7a85da 
This reduces the number of warnings+errors from 3021 to 1562 on the RISC-V
spec. This closes rems-project#1011.
@tobiasgrosser tobiasgrosser mentioned this issue Feb 15, 2025
Merged
tobiasgrosser added a commit to opencompl/sail that referenced this issue Feb 15, 2025
@tobiasgrosser
Lean: ignore unused variables
037fa78 
This reduces the number of warnings+errors from 3021 to 1562 on the RISC-V
spec. This closes rems-project#1011.
tobiasgrosser added a commit to opencompl/sail that referenced this issue Feb 15, 2025
@tobiasgrosser @ineol
Lean: ignore unused variables
1328b4e 
This reduces the number of warnings+errors from 3021 to 1562 on the RISC-V
spec. This closes rems-project#1011.

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
Assignees
No one assigned
Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Lean: ignore unused variables and increase compute outs opencompl/sail
1 participant
@tobiasgrosser