Skip to content

Fixes to align with recent HOL's change to rebinds #347

Fixes to align with recent HOL's change to rebinds

Fixes to align with recent HOL's change to rebinds #347

Workflow file for this run

# 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: 480
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/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