Add Lean disaster recovery specification and trace validation #13
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: "Lean Shallow Verification" | |
| on: | |
| pull_request: | |
| paths: | |
| - "lean/**" | |
| - "tla/disaster-recovery/**" | |
| - "include/ccf/node/startup_config.h" | |
| - "include/ccf/service/tables/self_healing_open.h" | |
| - "src/node/recovery_decision_protocol.cpp" | |
| - "src/node/recovery_decision_protocol.h" | |
| - "src/node/rpc/self_healing_open_handlers.h" | |
| - "tests/e2e_operations.py" | |
| - "tests/infra/recovery_trace.py" | |
| - "CMakeLists.txt" | |
| - ".github/workflows/ci.yml" | |
| - ".github/workflows/lean-shallow.yml" | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: read-all | |
| jobs: | |
| disaster-recovery: | |
| name: Disaster Recovery | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Install Lean | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update | |
| sudo apt-get install -y elan | |
| elan toolchain install "$(cat lean/disaster-recovery/lean-toolchain)" | |
| - name: Restore Mathlib cache | |
| working-directory: lean/disaster-recovery | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| lake exe cache get | |
| - name: Build and check Lean models | |
| working-directory: lean/disaster-recovery | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| lake build | |
| lake env lean -DwarningAsError=true AxiomChecks.lean | |
| lake exe semantic-checks | |
| lake exe canonical-checks | |
| lake exe disaster-recovery check --nodes 3 | |
| - name: Compare Lean and Stateright | |
| working-directory: lean/disaster-recovery | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| python3 compare.py --nodes 1 2 |