Tim Hutt

Rebased & README added.

I'll see if I can sort out the Lean errors.

Rebased but it's broken now and awkward to fix due to using the Sail generated header. Will probably have to wait until runtime XLEN is merged.

Rebased & tweaked a little to handle the changes since. I'll give this a couple of days before merging in case anyone wants to take a look.

Ah yeah good call - also since the XLEN stuff was merged I can move the generated C into the library. I renamed it to `riscv_model` since it's not just...

Ok I had a look into this and the issue is that Lean is treating the very *last* function in the code as special. On `master` the `LeanRV64D.lean` file starts...

I think `execute` might be nested for RVC... but yeah I would avoid it in general. As for being interrupted in the middle of the instruction, that is true for...

Discussed in meeting. We're going to wait for the new config system and then add separate flags for each case we encounter.

Maybe you could provide some details about the motivation for this, because at first glance I'd agree with Jessica. Doesn't seem like it belongs here.

Definitely an improvement but I'd still like to hear the motivation for this and how you plan to handle compiler options like `-fPIC`, `-mcmodel`, etc. Is the idea to create...