model/CMakeLists: add Lean variant

[RaitoBezarius]

This adds the support to try the Lean generation for RISC-V CPU.

I was not able to test it until the very end using Sail v2 rev a5a1072ac69a9207fb9202082161fc127f90567a and failed with the following error:

Type error:
riscv_step.sail:120.8-9:
120 |        i = 0;
    |        ^ checking function argument has type (unit, int, int)
    | Cannot modify immutable let-bound constant or enumeration constructor i
make[3]: *** [model/CMakeFiles/generated_lean_rv64d_lean.dir/build.make:165: model/lean_rv64d_lean.?] Error 1
make[2]: *** [CMakeFiles/Makefile2:1015: model/CMakeFiles/generated_lean_rv64d_lean.dir/all] Error 2
make[1]: *** [CMakeFiles/Makefile2:1022: model/CMakeFiles/generated_lean_rv64d_lean.dir/rule] Error 2
make: *** [Makefile:583: generated_lean_rv64d_lean] Error 2

This might have to do with how I did set up the generation.

[tobiasgrosser]

I used this PR over the last week and it works great for me. I also created a CI-action for the sail repository (rems-project/sail#1012), which demonstrates that this PR works.

@RaitoBezarius, if you could fix the formatting issue, we can see CI results for this repo. If they are green, I would like to get this PR merged, as this will simplify other workflows.

[Timmmm]

LGTM, I'll merge this if nobody has any objections. Thanks for testing!

[jordancarlin]

Might want to add a note that this requires the latest upstream version of sail, but otherwise LGTM

[RaitoBezarius]

Might want to add a note that this requires the latest upstream version of sail, but otherwise LGTM

We could add --min-required-version and select an arbitrary reasonable version to fail hard at runtime?

[github-actions]

Test Results

392 tests  ±0   392 ✅ ±0   1m 20s ⏱️ ±0s
  1 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 03df94e. ± Comparison against base commit dd7d438.

♻️ This comment has been updated with latest results.

[jordancarlin]

We could add --min-required-version and select an arbitrary reasonable version to fail hard at runtime?

Seems reasonable since right now there is no minimum required version. We should probably bump the coq minimum required version as well (that can be in a separate PR though).

[tobiasgrosser]

We could add --min-required-version and select an arbitrary reasonable version to fail hard at runtime?

Seems reasonable since right now there is no minimum required version. We should probably bump the coq minimum required version as well (that can be in a separate PR though).

This sounds reasonable to me. @RaitoBezarius, will you take care?

[RaitoBezarius]

We could add --min-required-version and select an arbitrary reasonable version to fail hard at runtime?

Seems reasonable since right now there is no minimum required version. We should probably bump the coq minimum required version as well (that can be in a separate PR though).

This sounds reasonable to me. @RaitoBezarius, will you take care?

This is done!

[tobiasgrosser]

I tested again, and this PR still works for me. I am happy to see this merged.

[jordancarlin]

LGTM now

[tobiasgrosser]

Increasing the sail version to 0.19 breaks my build. Any advice on how I should use this, given that sail 0.19 is not yet released? I am trying to use this with the current sail HEAD.

[jordancarlin]

Increasing the sail version to 0.19 breaks my build. Any advice on how I should use this, given that sail 0.19 is not yet released? I am trying to use this with the current sail HEAD.

Hmm. That is a good point. A couple of different things come to mind:

• Depending on how @Alasdair feels, it might make more sense for Sail to bump its version immediately after each release instead of right before. So after 0.18 released we'd have something like 0.19-dev until 0.19 is ready and then after releasing 0.19 bump the head to 0.20-dev.
• I imagine there are not many people using the Lean version right now, so one option would be to manually reduce the minimum version back to 0.18 if you are intending to actually use Lean. For purposes of CI, this could be done using a simple sed command or patch. Definitely not as elegant though.
• We could also just leave it at 0.18 for now and decide that's fine. I'm slightly hesitant to do that though because we've already had people attempt to use the coq target and see it fail because the current released version of Sail is incompatible.

[RaitoBezarius]

IMHO it'd make sense to bump sail HEAD to 0.19 right now but I'm not familiar with details and sail release management.

[tobiasgrosser]

That works for me. Why don't we merge it as is? I can then propose a PR to sail. If it goes through, we are golden. Otherwise, I will fix this via CI/sed.

[Timmmm]

Yeah I feel like this should require 0.19, and then either:

1. You just locally edit the CMake to require 0.18 so it works with Sail master. We could add -DCHECK_SAIL_VERSION=FALSE or something.
2. You locally edit the Sail version to 0.19 when building master.
3. Sail immediately bumps the version to 0.19 after releasing 0.18. A bit unsatisfying though since it isn't version 0.19.

[Timmmm]

(So I'm in favour of merging this as-is.)

[Timmmm]

I created #744 so we hopefully remember to add this to CI when it works with a released version of the Sail compiler.