leo/.github/workflows/acl2.yml

name: Leo-ACL2
on: 
  pull_request:
    push:
      branches:
        - master
        - staging
        - trying
      paths-ignore:
        - 'docs/**'
        - 'documentation/**'
env: 
  RUST_BACKTRACE: 1

# This job can only be run on linux (Ubuntu)
jobs:
  acl2:
    name: leo-acl2
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        uses: actions/checkout@v2

      - name: Install Rust
        uses: actions-rs/toolchain@v1
        with:
          profile: minimal
          toolchain: stable
          override: true

      - name: Generate asts
        run: |
          cargo run -p leo-test-framework --bin tgc

      # Pull the latest release from the leo-acl2-bin repo, and put it into the
      # repo/acl2 directory. After it's done, unpack the tgz file locally.
      - name: Pull tgc executable
        run: |
          mkdir acl2 && cd acl2;
          wget $(curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
              | grep "browser_download_url.*.tgz"  \
              | cut -d : -f 2,3 \
              | tr -d \" \
              | xargs)

          tar -xvzf $(ls)
      
      # Using the prepared ASTs and the pulled and unzipped tgc run theorem generation.
      - name: Run tgc over ASTs
        run: |
          errors=();
          for dir in `ls tmp/tgc`;
          do
            cd tmp/tgc/$dir; # enter the directory
            ./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > result.out || errors+=("$dir");
            ./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp || errors+=("$dir");
            cd ../../..
          done;

          if [ ${#errors[@]} -eq 0 ]; then
            echo "Success!"
          else
            echo "Failures:";
            for i in ${errors[@]};
            do
              echo $i;
              cat tmp/tgc/$dir.out
            done;
            exit 1
          fi