feat(lean/run_tests): Test generated Lean code using Lean itself

This reuses the various lean-toolchain information and download an
ad-hoc Lean version based on this.

Signed-off-by: Raito Bezarius <[email protected]>

.github/workflows/coverage.yml

@@ -21,7 +21,26 @@ jobs:
     - name: System dependencies
       run: |
         sudo apt-get update
-        sudo apt-get -o Acquire::Retries=3 install build-essential libgmp-dev z3 cvc4 opam cargo verilator
+        sudo apt-get -o Acquire::Retries=3 install build-essential libgmp-dev z3 cvc4 opam cargo verilator git curl
+
+    - name: Install Lean version manager
+      run: |
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
+
+    - name: Restore cached elan
+      id: cache-elan-restore
+      uses: actions/cache/restore@v3
+      with:
+        path: ~/.elan
+        key: ${{ matrix.os }}-${{ matrix.version }}-cov
+
+    - name: Save cached elan
+      if: steps.cache-elan-restore.outputs.cache-hit != 'true'
+      id: cache-elan-save
+      uses: actions/cache/save@v3
+      with:
+        path: ~/.elan
+        key: ${{ steps.cache-elan-restore.outputs.cache-primary-key }}
 
     - name: Restore cached opam
       id: cache-opam-restore

test/lean/run_tests.py

@@ -29,6 +29,7 @@ def test_lean():
                 step('rm -r {} || true'.format(basename))
                 step('mkdir -p {}'.format(basename))
                 step('\'{}\' {} --lean --lean-output-dir {}'.format(sail, filename, basename))
+                step(f'lake --dir {basename}/out build')
                 step('diff {}/out/Out.lean {}.expected.lean'.format(basename, basename))
                 step('rm -r {}'.format(basename))
                 print_ok(filename)