name: What4 CI
on:
  - push
  - pull_request

# The CACHE_VERSION can be updated to force the use of a new cache if
# the current cache contents become corrupted/invalid.  This can
# sometimes happen when (for example) the OS version is changed but
# older .so files are cached, which can have various effects
# (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
env:
  CACHE_VERSION: 1

jobs:
  linux:
    name: Testing ${{ matrix.os }} GHC-${{ matrix.ghc }}
    runs-on: ${{ matrix.os }}
    continue-on-error: ${{ matrix.allow-failure }}
    strategy:
      matrix:
        os: [ubuntu-latest]
        ghc: [8.10.4, 8.8.4, 8.6.5]
        allow-failure: [false]
      fail-fast: false
    steps:
      - uses: actions/checkout@v2
        with:
          submodules: true
      - uses: cachix/install-nix-action@v12
        with:
          nix_path: nixpkgs=channel:nixos-unstable
      - uses: actions/cache@v2
        name: Cache builds
        with:
          path: |
            ${{ steps.setup-haskell.outputs.cabal-store }}
            ~/.cabal/packages
            ~/.cabal/store
            dist-newstyle
          key: |
            ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ github.ref }}
          restore-keys: |
            ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-ghc${{ matrix.ghc }}-
      - name: Cabal update
        shell: bash
        run: nix-shell -p cabal-install --run 'cabal update'
      - name: Cabal check
        shell: bash
        run: |
          cd what4
          nix-shell -p cabal-install --run 'cabal check'
      - name: Setup Environment Vars
        run: |
          GHC=haskell.compiler.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g)
          echo GHC=$GHC >> $GITHUB_ENV
          echo GHCPKGS=haskell.packages.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g) >> $GITHUB_ENV
          echo ZLIB_LOC="$(nix eval --raw nixpkgs.zlib)/lib" >> $GITHUB_ENV
          echo NS="nix-shell -p cabal-install $GHC gmp zlib --run" >> $GITHUB_ENV

      - name: Package's Cabal/GHC compatibility
        shell: bash
        # Using setup will use the cabal library installed with GHC
        # instead of the cabal library of the Cabal-install tool to
        # verify the cabal file is compatible with the associated
        # GHC cabal library version.  Cannot run configure or build,
        # because dependencies aren't present, but a clean is
        # sufficient to cause parsing/validation of the cabal file.
        run: |
          defsetup()  { echo import Distribution.Simple; echo main = defaultMain; }
          setup_src() { if [ ! -f Setup.hs ] ; then defsetup > DefSetup.hs; fi; ls *Setup.hs; }
          setup_bin() { echo setup.${{ matrix.ghc }}; }
          with_ghc()  { nix-shell -p $GHC --run "$(echo ${@})"; }
          (cd what4;     with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
          (cd what4-abc; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
          (cd what4-blt; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)

      - name: Cabal check
        shell: bash
        run: |
          (cd what4;     $NS 'cabal check')
          (cd what4-abc; $NS 'cabal check')
          (cd what4-blt; $NS 'cabal check')

      - name: Cabal configure
        shell: bash
        # Note: the explicit LD_LIBRARY_PATH is needed for GHC 8.6.5
        # which doesn't seem to process the --extra-lib-dirs
        # correctly.  When only GHC 8.8 or later are supported, the
        # LD_LIBRARY_PATH manipulation may be removed for all steps.
        run: |
          cd what4
          $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal configure -fSTPTestDisable -fdRealTestDisable -fsolverTests --extra-lib-dirs="$ZLIB_LOC"'
      - name: Build
        shell: bash
        run: |
          cd what4
          $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal build --extra-lib-dirs="$ZLIB_LOC"'
      - name: Test
        shell: bash
        run: |
          cd what4
          echo Boolector version $(nix eval nixpkgs.boolector.version)
          echo CVC4 version $(nix eval nixpkgs.cvc4.version)
          echo Yices version $(nix eval nixpkgs.yices.version)
          echo Z3 version $(nix eval nixpkgs.z3.version)
          nix-shell -p cabal-install $GHC abc-verifier boolector cvc4 yices z3 zlib --run 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal test --extra-lib-dirs="$ZLIB_LOC"'
      - name: Documentation
        shell: bash
        run: |
          cd what4
          nix-shell -p cabal-install $GHC zlib --run 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal haddock what4 --extra-lib-dirs="$ZLIB_LOC"'