Lean: Make the RISC-V Sail model build

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]>

.github/workflows/build-riscv-lean-workaround-riscv.patch

@@ -0,0 +1,12 @@
+diff --git a/model/riscv_step.sail b/model/riscv_step.sail
+index 7a6d9450..dd38bdc3 100644
+--- a/model/riscv_step.sail
++++ b/model/riscv_step.sail
+@@ -118,6 +118,7 @@ function loop () : unit -> unit = {
+         /* for now, we drive the platform i/o at every clock tick. */
+         tick_platform();
+         i = 0;
++	()
+       }
+     }
+   }

.github/workflows/build-riscv-lean.yml

@@ -0,0 +1,60 @@
+name: Build RISCV For Lean
+
+on: [push, workflow_dispatch]
+
+env:
+  OPAMVERBOSE: 1
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        version: [5.2.1]
+        os: [ubuntu-latest]
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: System dependencies (ubuntu)
+      if: startsWith(matrix.os, 'ubuntu')
+      run: |
+        sudo apt install build-essential libgmp-dev z3 cvc4 opam
+
+    - name: Restore cached opam
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.os }}-${{ matrix.version }}
+
+    - name: Setup opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      run: |
+        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+
+    - name: Save cached opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      id: cache-opam-save
+      uses: actions/cache/save@v4
+      with:
+        path: ~/.opam
+        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+
+    - name: Install Sail
+      run: |
+        eval $(opam env)
+        opam pin --yes --no-action add .
+        opam install sail --yes
+
+    - name: Build the `Sail RISCV Model with Lean`
+      run: |
+        git clone https://github.com/RaitoBezarius/sail-riscv.git
+        cd sail-riscv
+        git checkout lean
+        eval $(opam config env)
+        cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo
+        # This patch is needed to work around https://github.com/rems-project/sail/issues/1003.
+        patch -p1 < ../../sail/.github/workflows/build-riscv-lean-workaround-riscv.patch
+        cmake --build build/ --target generated_lean_rv64d_lean

src/sail_lean_backend/pretty_print_lean.ml

@@ -694,7 +694,11 @@ let doc_funcl_init global (FCL_aux (FCL_funcl (id, pexp), annot)) =
            match pat_is_plain_binder env pat with
            | Some (Some id, _) -> (id, typ)
            | Some (None, _) -> (Id_aux (Id "x", l), typ) (* TODO fresh name or wildcard instead of x *)
-           | _ -> failwith "Argument pattern not translatable yet."
+           | _ ->
+               ( Id_aux (Id "TODO_ARG_PATTERN", Unknown),
+                 Typ_aux (Typ_id (Id_aux (Id "TODO_ARG_PATTERN", Unknown)), Unknown)
+               )
+           (* failwith "Argument pattern not translatable yet." *)
        )
   in
   let ctx = context_init env global in