feat(ci): add Lean testing in the CI (#871)

* 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.

Note: /bin/bash is not guaranteed to exist on all Linux distributions, NixOS
does not have one. We prefer `/usr/bin/env` which should really (empirically) always exist.

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

.github/workflows/coverage.yml

@@ -21,7 +21,31 @@ 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: Restore cached elan
+      id: cache-elan-restore
+      uses: actions/cache/restore@v3
+      with:
+        path: ~/.elan
+        key: ${{ matrix.os }}-${{ matrix.version }}-elan
+
+    - name: Install Lean version manager
+      if: steps.cache-elan-restore.outputs.cache-hit != 'true'
+      run: |
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+
+    - 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: Set elan path
+      run: |
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
     - name: Restore cached opam
       id: cache-opam-restore
@@ -43,7 +67,7 @@ jobs:
         path: ~/.opam
         key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
 
-    - name: Install Sail
+    - name: Install Sail dependencies
       run: |
         eval $(opam env)
         opam pin --yes --no-action add .

sail

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 SAIL_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 export SAIL_DIR

test/lean/run_tests.py

@@ -26,8 +26,10 @@ def test_lean():
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
-                step('mkdir {}'.format(basename))
+                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)