pure.yml

# 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
  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 }}

    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: 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

    - name: Record HOL/CakeML checkouts
      id: shas
      run: |
        cd $HOLDIR
        echo "HOL_SHA=$(git rev-parse HEAD)" >> $GITHUB_OUTPUT
        cd $CAKEMLDIR
        echo "CAKEML_SHA=$(git rev-parse HEAD)" >> $GITHUB_OUTPUT

  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