Update for new way of doing in-logic compilation #396
This file contains 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 is a basic workflow to help you get started with Actions | |
| name: CI | |
| on: | |
| push: | |
| branches: | |
| - master | |
| paths: | |
| - '**.sml' | |
| - 'Holmakefile' | |
| - '**.hs' | |
| pull_request: | |
| branches: | |
| - master | |
| schedule: | |
| - cron: '0 0 * * Fri' | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| runs-on: self-hosted | |
| container: ubuntu:20.04 | |
| timeout-minutes: 600 | |
| env: | |
| HOLDIR: ${{ github.workspace }}/HOL | |
| CAKEMLDIR: ${{ github.workspace }}/cakeml | |
| LD_LIBRARY_PATH: /usr/local/lib:$LD_LIBRARY_PATH | |
| outputs: | |
| hol_sha: ${{ steps.shas.outputs.HOL_SHA }} | |
| cakeml_sha: ${{ steps.shas.outputs.CAKEML_SHA }} | |
| hol_short_sha: ${{ steps.shas.outputs.HOL_SHORT_SHA }} | |
| cakeml_short_sha: ${{ steps.shas.outputs.CAKEML_SHORT_SHA }} | |
| steps: | |
| - name: Update PATH | |
| run: | | |
| echo "$HOLDIR/bin" >> $GITHUB_PATH | |
| - name: Get build-essentials | |
| run: | | |
| apt update | |
| apt install -y git build-essential gcc-10 libffi-dev wget mlton | |
| - name: Checkout Poly/ML | |
| uses: actions/checkout@v2 | |
| with: | |
| repository: polyml/polyml | |
| ref: fixes-5.9 | |
| path: polyml | |
| - name: Build Poly/ML | |
| run: | | |
| cd polyml | |
| ./configure | |
| make | |
| make install | |
| - name: Checkout HOL4 | |
| uses: actions/checkout@v2 | |
| with: | |
| repository: HOL-Theorem-Prover/HOL | |
| ref: master | |
| path: HOL | |
| - name: Checkout pure | |
| uses: actions/checkout@v2 | |
| with: | |
| path: pure | |
| - name: Checkout CakeML | |
| uses: actions/checkout@v2 | |
| with: | |
| repository: CakeML/CakeML | |
| path: cakeml | |
| - name: Record HOL/CakeML checkouts | |
| id: shas | |
| run: | | |
| cd $HOLDIR | |
| echo "HOL_SHA=$(git rev-parse HEAD)" >> $GITHUB_OUTPUT | |
| echo "HOL_SHORT_SHA=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT | |
| cd $CAKEMLDIR | |
| echo "CAKEML_SHA=$(git rev-parse HEAD)" >> $GITHUB_OUTPUT | |
| echo "CAKEML_SHORT_SHA=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT | |
| - name: Build HOL4 | |
| run: | | |
| cd $HOLDIR | |
| poly < tools/smart-configure.sml | |
| bin/build | |
| - name: Build CakeML misc | |
| run: | | |
| cd $CAKEMLDIR/misc | |
| Holmake | |
| - name: Build CakeML semantics | |
| run: | | |
| cd $CAKEMLDIR/semantics | |
| Holmake | |
| - name: Build CakeML semantics/proofs | |
| run: | | |
| cd $CAKEMLDIR/semantics/proofs | |
| Holmake | |
| - name: Build CakeML semantics/alt_semantics | |
| run: | | |
| cd $CAKEMLDIR/semantics/alt_semantics | |
| Holmake | |
| - name: Build CakeML semantics/alt_semantics/proofs | |
| run: | | |
| cd $CAKEMLDIR/semantics/alt_semantics/proofs | |
| Holmake | |
| - name: Build CakeML basis/pure | |
| run: | | |
| cd $CAKEMLDIR/basis/pure | |
| Holmake | |
| - name: Build misc | |
| run: | | |
| cd pure/misc | |
| Holmake | |
| - name: Build language | |
| run: | | |
| cd pure/language | |
| Holmake | |
| - name: Build meta-theory | |
| run: | | |
| cd pure/meta-theory | |
| Holmake | |
| - name: Build compiler/backend | |
| run: | | |
| cd pure/compiler/backend | |
| Holmake | |
| - name: Build compiler/backend/languages | |
| run: | | |
| cd pure/compiler/backend/languages | |
| Holmake | |
| - name: Build compiler/backend/languages/semantics | |
| run: | | |
| cd pure/compiler/backend/languages/semantics | |
| Holmake | |
| - name: Build compiler/backend/languages/properties | |
| run: | | |
| cd pure/compiler/backend/languages/properties | |
| Holmake | |
| - name: Build typing | |
| run: | | |
| cd pure/typing | |
| Holmake | |
| - name: Build compiler/backend/passes | |
| run: | | |
| cd pure/compiler/backend/passes | |
| Holmake | |
| - name: Build compiler/backend/passes/proofs | |
| run: | | |
| cd pure/compiler/backend/passes/proofs | |
| Holmake | |
| - name: Build compiler/backend/languages/relations | |
| run: | | |
| cd pure/compiler/backend/languages/relations | |
| Holmake | |
| - name: Build compiler/parsing | |
| run: | | |
| cd pure/compiler/parsing | |
| Holmake | |
| - name: Build compiler | |
| run: | | |
| cd pure/compiler | |
| Holmake | |
| - name: Build CakeML compiler/backend/proofs | |
| run: | | |
| cd $CAKEMLDIR/compiler/backend/proofs | |
| Holmake | |
| - name: Build compiler/proofs | |
| run: | | |
| cd pure/compiler/proofs | |
| Holmake | |
| - name: Build compiler/binary | |
| run: | | |
| cd pure/compiler/binary | |
| Holmake | |
| - name: Save build artifact | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: pure.S | |
| path: pure/compiler/binary/pure.S | |
| - name: Build examples | |
| run: | | |
| cd pure/examples | |
| make check | |
| - name: Check that benchmarks compile | |
| run: | | |
| apt install -y python3 python3-pip | |
| pip install parse matplotlib pandas | |
| cd pure/examples | |
| git apply benchmark/benchmark.patch | |
| touch lib/basis_ffi.c | |
| cd benchmark && ./benchmark.py --mode compile | |
| release: | |
| if: github.event_name == 'workflow_dispatch' && github.ref == 'refs/heads/master' | |
| needs: build | |
| permissions: | |
| contents: write | |
| runs-on: self-hosted | |
| container: ubuntu:20.04 | |
| env: | |
| COMMITS: ${{ github.workspace }}/commits.txt | |
| steps: | |
| - name: Install GitHub CLI | |
| run: | | |
| apt update && apt install -y curl | |
| curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg | dd of=/usr/share/keyrings/githubcli-archive-keyring.gpg | |
| chmod go+r /usr/share/keyrings/githubcli-archive-keyring.gpg | |
| echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" | tee /etc/apt/sources.list.d/github-cli.list > /dev/null | |
| apt update && apt install -y gh | |
| - name: Create release tag and release notes | |
| run: | | |
| echo "VERSION=v$(date +'%Y.%m.%d')" >> $GITHUB_ENV | |
| echo "HOL checkout: HOL-Theorem-Prover/HOL@${{ needs.build.outputs.hol_sha }}" >> $COMMITS | |
| echo "CakeML checkout: CakeML/CakeML@${{ needs.build.outputs.cakeml_sha }}" >> $COMMITS | |
| - name: Download build artifact | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: pure.S | |
| - name: Create GitHub release | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| gh release create ${{ env.VERSION }} --repo cakeml/pure --latest --notes-file $COMMITS pure.S | |
| rm -f pure.S $COMMITS | |
| notify: | |
| needs: build | |
| runs-on: self-hosted | |
| container: ubuntu:20.04 | |
| if: ${{ always() }} | |
| steps: | |
| - name: Get curl | |
| run: | | |
| apt update | |
| apt install -y curl | |
| - name: Notify CakeML Discord | |
| run: > | |
| curl --silent --show-error --request POST | |
| --header "Content-type: application/json;charset=utf-8" | |
| --data "{\"embeds\": [{ | |
| \"title\": \"CI #${{ github.run_number }}\", | |
| \"description\": \"${{ needs.build.result == 'success' && 'Passed' || 'Failed' }}\", | |
| \"url\": \"https://github.com/CakeML/pure/actions/runs/${{ github.run_id }}\", | |
| \"color\": ${{ needs.build.result == 'success' && 8311585 || 13632027 }}, | |
| \"author\": { | |
| \"name\": \"PureCake CI\", | |
| \"url\": \"https://github.com/CakeML/pure/actions/workflows/pure.yml\"}, | |
| \"fields\": [ | |
| {\"name\": \"HOL commit\", \"inline\": true, | |
| \"value\": \"[${{ needs.build.outputs.hol_short_sha }}](https://github.com/HOL-Theorem-Prover/HOL/commit/${{ needs.build.outputs.hol_sha }})\"}, | |
| {\"name\": \"CakeML commit\", \"inline\": true, | |
| \"value\": \"[${{ needs.build.outputs.cakeml_short_sha }}](https://github.com/CakeML/cakeml/commit/${{ needs.build.outputs.cakeml_sha }})\"}] | |
| }]}" | |
| ${{ secrets.DISCORD_WEBHOOK }} |