Skip to content
CI

Use SMTLIB instead of Z3 bindings; remove Z3 lib dependency (#303) #1081

Sign in to view logs

Use SMTLIB instead of Z3 bindings; remove Z3 lib dependency (#303)

Use SMTLIB instead of Z3 bindings; remove Z3 lib dependency (#303) #1081

Workflow file for this run

.github/workflows/ci.yml at 364bfdf
name: CI
on:
push:
branches: [master]
pull_request:
branches: [master]
merge_group:
workflow_dispatch:
env:
NODE_VERSION: 18
DOCKER_TEST_TAG: gillian:test
jobs:
build:
strategy:
fail-fast: false
matrix:
operating-system: [macos-latest, ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: actions/checkout@v4
- uses: actions/setup-python@v4
with:
python-version: "3.10"
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: Installing Python prerequisites
run: sudo pip install sphinx furo
- name: Restore Cache
id: restore-cache
uses: actions/cache@v3
env:
cache-name: cache-ocaml
with:
path: _opam
key: ${{ runner.os }}-${{ env.cache-name}}-ocaml-5.2.0-${{ hashFiles('**/*.opam') }}
restore-keys: |
${{ runner.os }}-${{ env.cache-name}}-ocaml-5.2.0
- name: Install dependencies
run: make init-ci
- name: Build Gillian
run: opam exec -- dune build @all
- name: Basic tests
run: opam exec -- dune test
- name: Wisl checks
run: "opam exec -- dune exec -- bash ./wisl/scripts/quicktests.sh"
- name: Format checking
run: opam exec -- dune fmt
- name: Installing to opam switch
run: |
opam exec -- dune build @install
opam install . -y
- name: Compressing artifact
run: tar czf opam.tar.gz _opam
- name: Sending artifact for next jobs
uses: actions/upload-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam.tar.gz
- name: Building docs
run: make docs
if: runner.os == 'Linux'
- name: Sending docs artifact
uses: actions/upload-artifact@v4
with:
name: ${{ runner.os }}-docs
path: _docs
if: runner.os == 'Linux'
- name: Setting dependency cache
run: opam clean
if: steps.restore-cache.outputs.cache-hit != 'true'
gillian_c_tests:
strategy:
matrix:
operating-system: [ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
needs: build
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: Checkout project
uses: actions/checkout@v3
with:
path: Gillian
- name: Download release
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam
- name: Extract release
run: |
tar xzf opam/opam.tar.gz
rm -rf opam
- name: init env
run: "Gillian-C/scripts/setup_environment.sh"
working-directory: "Gillian"
- name: Test All
run: "./testAll.sh"
working-directory: "Gillian/Gillian-C/environment/"
- name: Test Amazon
run: "make"
working-directory: "Gillian/Gillian-C/examples/amazon/"
gillian_js_tests:
strategy:
matrix:
operating-system: [ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
needs: build
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: Checkout project
uses: actions/checkout@v3
with:
path: Gillian
- name: Download release
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam
- name: Extract release
run: |
tar xzf opam/opam.tar.gz
rm opam -rf
- name: init env
run: "Gillian-JS/scripts/setup_environment.sh"
working-directory: "Gillian"
- name: Test JaVerT
run: "./testJaVerT.sh"
working-directory: "Gillian/Gillian-JS/environment/"
# - name: Test Amazon
# run: "make"
# working-directory: "Gillian/Gillian-JS/Examples/Amazon/"
kanillian_c_tests:
strategy:
matrix:
operating-system: [ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
needs: build
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: install CBMC
run: sudo apt install cbmc -y
- name: Checkout project
uses: actions/checkout@v3
with:
path: Gillian
- name: Download release
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam
- name: Extract release
run: |
tar xzf opam/opam.tar.gz
rm -rf opam
- name: init env
run: "kanillian/scripts/setup_environment.sh"
working-directory: "Gillian"
- name: Test All
run: "opam exec -- bash ./testAll.sh"
working-directory: "Gillian/kanillian/environment/"
test262:
if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')
strategy:
matrix:
operating-system: [ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
needs: build
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: Checkout project
uses: actions/checkout@v3
with:
repository: GillianPlatform/javert-test262
path: test262
ref: 93e0d0b04093cabc3234a776eec5cc3e165f3b1a
- name: Download release
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam
- name: Extract release
run: |
tar xzf opam/opam.tar.gz
rm -rf opam
- name: Test262
run: "opam exec -- gillian-js test262 test262/test --ci"
collections-c:
if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')
strategy:
matrix:
operating-system: [ubuntu-latest]
runs-on: ${{ matrix.operating-system }}
needs: build
steps:
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: "ocaml-variants.5.2.0+options"
- name: checkout project
uses: actions/checkout@v3
with:
repository: GillianPlatform/collections-c-for-gillian
path: collections-c
ref: ffa76e788a1fbdb67910bb7b794214ebc22c1b8c
- name: Download release
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-opam
path: opam
- name: Extract release
run: |
tar xzf opam/opam.tar.gz
rm -rf opam
- name: Symbolic Testing Collections-C
run: "opam exec -- bash ./scripts/gillian-compcert/runTests.sh"
working-directory: collections-c
# test-Buckets:
# if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')
# strategy:
# matrix:
# operating-system: [macos-latest]
# runs-on: ${{ matrix.operating-system }}
# needs: build
# steps:
# - name: Setup Z3
# id: z3
# uses: cda-tum/setup-z3@v1
# env:
# GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
# - uses: ocaml/setup-ocaml@v2
# with:
# ocaml-compiler: "ocaml-variants.5.2.0+options"
# - name: Checkout project
# uses: actions/checkout@v3
# with:
# path: Gillian
# - name: Download release
# uses: actions/download-artifact@v4
# with:
# name: ${{ runner.os }}-opam
# path: opam
# - name: Extract release
# run: |
# tar xzf opam/opam.tar.gz
# rm -rf opam
# - name: Symbolic Testing Buckets.js
# run: "opam exec -- gillian-js cosette-bulk Gillian/Gillian-JS/Examples/Cosette/Buckets --ci"
build-docker:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Set up docker buildx
uses: docker/setup-buildx-action@v2
with:
driver: docker
- name: Restore Cache
id: restore-cache
uses: actions/cache@v3
env:
cache-name: cache-ocaml
with:
path: _opam
key: docker-${{ env.cache-name }}-ocaml-5.2.0-${{ hashFiles('**/*.opam') }}
restore-keys: |
docker-${{ env.cache-name }}-ocaml-5.2.0
- name: Build and export docker image
uses: docker/build-push-action@v4
with:
context: .
load: true
tags: ${{ env.DOCKER_TEST_TAG }}
- name: Dune test
run: docker run --rm ${{ env.DOCKER_TEST_TAG }} opam exec -- dune test
- name: Extract cache
if: steps.restore-cache.outputs.cache-hit != 'true'
run: |
rm -rf _opam
docker run --name deps ${{ env.DOCKER_TEST_TAG }} bash -c "opam clean"
docker cp deps:/home/opam/.opam/5.2 ./
docker rm deps
deploy-docs:
if: github.ref == 'refs/heads/master'
runs-on: ubuntu-latest
needs: [build]
strategy:
fail-fast: false
matrix:
operating-system: [ubuntu-latest]
steps:
- name: Download built docs
uses: actions/download-artifact@v4
with:
name: ${{ runner.os }}-docs
path: docs
- name: Deploy docs
run: |
git config --global user.email "<>"
git config --global user.name "GitHub Actions"
git clone https://${{ secrets.DOCS_USER }}:${{ secrets.DOCS_TOKEN }}@github.com/GillianPlatform/GillianPlatform.github.io.git docs-repo --branch master
cd docs-repo
rm * -rf
cp -r ../docs/* .
git add -A
git commit -m "Deployment from $GITHUB_REPOSITORY@$GITHUB_SHA"
git push --force