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: missing support for wMem, rMem, wMem_Addr #939

Closed
tobiasgrosser opened this issue Feb 1, 2025 · 0 comments
Closed

sail-to-lean: missing support for wMem, rMem, wMem_Addr #939

tobiasgrosser opened this issue Feb 1, 2025 · 0 comments
Assignees
@ineol
Labels
Lean Issues with Sail to Lean translation

Comments

@tobiasgrosser
Copy link
Collaborator

The tiny-arm model references wMem, rMem, and wMem_Addr, which triggers unknown identifier errors.
@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 1, 2025
@ineol ineol self-assigned this Feb 3, 2025
@ineol ineol mentioned this issue Feb 3, 2025
Merged
bacam pushed a commit that referenced this issue Feb 4, 2025
@ineol
Lean: translate type parameters of record types (#951)
10917a2 
This fixes part of #939 as the type Mem_write_request is now well defined.

A follow up PR will add type annotations to the let bindings to instantiate these parameters.
@ineol ineol mentioned this issue Feb 4, 2025
Closed
@lfrenot lfrenot closed this as completed Feb 13, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ineol ineol

Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ineol @tobiasgrosser @lfrenot