| |
| |
| |
|
|
| name: Idris proof typecheck |
|
|
| on: |
| push: |
| pull_request: |
| workflow_dispatch: |
|
|
| permissions: |
| contents: read |
|
|
| jobs: |
| typecheck: |
| runs-on: ubuntu-24.04 |
| timeout-minutes: 35 |
| steps: |
| - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 |
| - name: Install bootstrap dependencies |
| run: | |
| sudo apt-get update |
| sudo apt-get install -y chezscheme build-essential libgmp-dev |
| - name: Cache pinned Idris installation |
| id: idris-cache |
| uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 |
| with: |
| path: ~/.idris2 |
| key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1 |
| - name: Bootstrap pinned Idris 2 |
| if: steps.idris-cache.outputs.cache-hit != 'true' |
| run: | |
| git clone https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2" |
| cd "$RUNNER_TEMP/Idris2" |
| git checkout 15a3e4e70843f7a34100f6470c04b791330788df |
| make bootstrap SCHEME=chezscheme |
| make install |
| - name: Save compiler before checking project proofs |
| if: steps.idris-cache.outputs.cache-hit != 'true' |
| uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 |
| with: |
| path: ~/.idris2 |
| key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1 |
| - name: Check handwritten proof terms and model |
| run: | |
| export PATH="$HOME/.idris2/bin:$PATH" |
| mkdir -p build/reports |
| idris2 --version | tee build/reports/idris-version.txt |
| set -o pipefail |
| cd idris |
| idris2 --total --check LambdaProofs.idr 2>&1 | tee ../build/reports/lambda-typecheck.txt |
| idris2 --total --check Main.idr 2>&1 | tee ../build/reports/model-typecheck.txt |
| - name: Compile and smoke-test the current control model |
| run: | |
| export PATH="$HOME/.idris2/bin:$PATH" |
| set -o pipefail |
| cd idris |
| idris2 --total -o control-model Main.idr 2>&1 | tee ../build/reports/model-build.txt |
| build/exec/control-model | tee ../build/reports/model-smoke.txt |
| test "$(cat ../build/reports/model-smoke.txt)" = 'step: advanced' |
| - name: Preserve typechecker evidence |
| if: always() |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 |
| with: |
| name: idris-typecheck-evidence |
| path: build/reports/ |
| - name: Preserve the prototype control-model executable |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 |
| with: |
| name: idris-control-model-ubuntu24 |
| path: idris/build/exec/ |
|
|
