ci.yml

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 --allow-empty -m "Deployment from $GITHUB_REPOSITORY@$GITHUB_SHA"
          git push --force