name: Leo-ACL2
on: workflow_dispatch
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 -q 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 \
                  | jq -r '.assets[0].browser_download_url' )

          echo "Unpacking $(ls):"
          tar -xvzf $(ls)

      # Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
      - name: Run tgc over ASTs
        run: |
          canonicalization_errors=();
          type_inference_errors=();
          num_dirs=0;
          for dir in `ls tmp/tgc`;
          do
            cd tmp/tgc/$dir; # enter the directory
            num_dirs=$((num_dirs + 1));
            ./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
            ./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
            cd ../../..
          done;

          echo "----------------"
          echo "Ran tgc in ${num_dirs} directories."
          echo "----------------"
          if [ ${#canonicalization_errors[@]} -eq 0 ]; then
            echo "Canonicalization - Success!"
          else
            echo "Canonicalization Failures (total: ${#canonicalization_errors[@]}):"
            for dir in ${canonicalization_errors[@]};
            do
              echo $dir
            done;

            #echo "Attaching logs:"
            #for dir in ${canonicalization_errors[@]};
            #do
            # cat tmp/tgc/$dir/canonicalization_result.out
            # cat tmp/tgc/$dir/canonicalization-theorem.lisp
            #done;
          fi

          echo "----------------"
          if [ ${#type_inference_errors[@]} -eq 0 ]; then
            echo "Type Inference - Success!"
          else
            echo "Type Inference Failures (total: ${#type_inference_errors[@]}):"
            for dir in ${type_inference_errors[@]};
            do
              echo $dir
            done;

            #echo "Attaching logs:"
            #for dir in ${type_inference_errors[@]};
            #do
            # cat tmp/tgc/$dir/type_inference_result.out
            #done;
          fi

          if [[ ${#canonicalization_errors[@]} -ne 0 || ${#type_inference_errors[@]} -ne 0 ]]; then
            echo "----------------"
            echo "Exiting with status 1 due to at least one tgc error."
            exit 1
          fi