Lean 4 Build #80
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
| # This workflow is managed by gh actions-lock. | |
| # SPDX-License-Identifier: MPL-2.0 | |
| name: Lean 4 Build | |
| on: | |
| pull_request: | |
| push: | |
| branches: [main] | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| name: Build and Test Lean 4 | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - uses: actions/checkout@v4.1.1 | |
| with: | |
| persist-credentials: false | |
| - name: Install pinned Lean toolchain | |
| uses: leanprover/lean-action@v1.6.0 | |
| with: | |
| auto-config: 'false' | |
| build: 'false' | |
| test: 'false' | |
| lint: 'false' | |
| use-mathlib-cache: 'false' | |
| use-github-cache: 'false' | |
| - name: Build library, executable suites and narration axiom audit | |
| run: | | |
| set -euo pipefail | |
| lake build 2>&1 | tee lake-build.log | |
| - name: Run every registered suite, including real narration processes | |
| run: | | |
| set -euo pipefail | |
| lake test 2>&1 | tee lake-test.log | |
| - name: Check Lean incomplete-proof diagnostics | |
| run: ./scripts/check-lean-proofs.sh --build-log lake-build.log | |
| - uses: actions/upload-artifact@v4.6.2 | |
| if: always() | |
| with: | |
| name: lean-validation | |
| path: | | |
| lake-build.log | |
| lake-test.log | |
| if-no-files-found: error | |
| zig-ffi: | |
| name: Build Zig FFI Bridge | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@v4.1.1 | |
| with: | |
| persist-credentials: false | |
| - uses: mlugg/setup-zig@v2.2.1 | |
| with: | |
| version: '0.16.0' | |
| - name: Build and test bridge | |
| working-directory: bridge | |
| run: | | |
| set -euo pipefail | |
| zig build | |
| zig build test | |
| test -f zig-out/lib/liblith_bridge.a | |
| spec-validation: | |
| name: Validate Specifications | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4.1.1 | |
| with: | |
| persist-credentials: false | |
| - name: Check implemented contract and private specification inventory | |
| run: | | |
| set -euo pipefail | |
| for file in docs/narration-slice.adoc test/NarrationTest.lean test/NarrationProofAudit.lean spec/GQLdt-Grammar.ebnf spec/GQL-DT-Lexical.adoc; do | |
| test -s "$file" | |
| done | |
| # Presence is an inventory check; executable conformance is tested above. | |
| grep -q '::=' spec/GQLdt-Grammar.ebnf |