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@v3
        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: Install ubuntu dependencies
        run: sudo apt-get install libgmp-dev pkg-config libsqlite3-dev python3 z3 -y
        if: runner.os == 'Linux'
      - name: Build Gillian
        run: opam exec -- dune build @all
      - name: Basic tests
        run: opam exec -- dune test
      - name: Gillian-LLVM Tests
        run: opam exec -- dune exec gillian-llvm  -- bulk-wpst Gillian-LLVM/examples
      - 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/"

  gillian_c2_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: "Gillian-C2/scripts/setup_environment.sh"
        working-directory: "Gillian"
      - name: Test All
        run: "opam exec -- bash ./testAll.sh"
        working-directory: "Gillian/Gillian-C2/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: [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: .docker_opam_cache
          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 }}
          target: test
      - 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 .docker_opam_cache
          docker run --name deps ${{ env.DOCKER_TEST_TAG }} bash -c "opam clean"
          docker cp deps:/home/opam/.opam/5.2 ./.docker_opam_cache
          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