release.yml

# Taken from Herbie:
# https://github.com/herbie-fp/herbie/blob/400891fe4c89f0cee051b8e03089a01ab9016f4b/.github/workflows/release.yml
name: Generate Lakeroad release

on:
  push:
    tags:
    - 'v*'
  workflow_dispatch:
  # DO NOT MERGE: we are just including this so that we can test the release
  # while working on the PR.
  pull_request:

env:
  LAKEROAD_DIR: ${{ github.workspace }}/lakeroad_checkout
  RELEASE_DIR: ${{ github.workspace }}/lakeroad
  MAKE_JOBS: 2

jobs:
  build:
    name: Build
    strategy:
      # manual matrix: I think this was an easy way to make (os, os-name) pairs.
      matrix:
        include:
          # - os: windows-latest
          #   os-name: windows
          - os: ubuntu-latest
            os-name: ubuntu
            RACKET_PKG_DIR: /home/runner/.local/share/racket/8.11/pkgs
            arch: x64
          - os: macos-13
            os-name: macOS
            RACKET_PKG_DIR: /Users/runner/Library/Racket/8.11/pkgs
            coreutils_gnubin_path: /usr/local/opt/coreutils/libexec/gnubin
            arch: x64
          - os: macos-14
            os-name: macOS
            RACKET_PKG_DIR: /Users/runner/Library/Racket/8.11/pkgs
            coreutils_gnubin_path: /opt/homebrew/opt/coreutils/libexec/gnubin
            arch: arm64

    runs-on: ${{ matrix.os }}

    steps:
      - uses: actions/checkout@v4
        with:
          path: ${{ env.LAKEROAD_DIR }}

      - name: Install Racket
        uses: Bogdanp/setup-racket@v1.11
        with:
          version: 8.11
      
      - name: Set up Racket dependencies
        run: raco pkg install --no-docs --auto --batch rosette yaml

      - name: Install Python
        uses: actions/setup-python@v5
        with:
          python-version: '3.10' 

      - name: Install Python dependencies
        run: pip install -r ${{ env.LAKEROAD_DIR }}/requirements.txt && pip install pyinstaller

      - name: Build solvers and copy into Rosette (Ubuntu)
        if: matrix.os-name == 'ubuntu'
        run: |
          source ${{ env.LAKEROAD_DIR }}/dependencies.sh
          
          sudo apt-get update

          # Put dummy versions of cvc4 and boolector into Rosette.
          mkdir -p ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/
          cat >${{ matrix.RACKET_PKG_DIR }}/rosette/bin/cvc4 <<'EOF'
          #!/bin/bash
          echo "Please do not use cvc4 with Lakeroad."
          exit 1
          EOF
          chmod +x ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/cvc4
          cat >${{ matrix.RACKET_PKG_DIR }}/rosette/bin/boolector <<'EOF'
          #!/bin/bash
          echo "Please do not use boolector with Lakeroad."
          exit 1
          EOF
          chmod +x ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/boolector

          # Build Bitwuzla.
          sudo apt-get install -y ninja-build
          mkdir bitwuzla
          wget -qO- https://github.com/bitwuzla/bitwuzla/archive/$BITWUZLA_COMMIT_HASH.tar.gz | tar xz -C bitwuzla --strip-components=1
          cd bitwuzla
          ./configure.py --prefix=${{ env.RELEASE_DIR }}/deps/bitwuzla/
          cd build
          ninja -j${{ env.MAKE_JOBS }}
          ninja -j${{ env.MAKE_JOBS }} install
          cd ../..

          # Build STP.
          sudo apt install -y patchelf
          sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl
          mkdir stp && cd stp
          wget -qO- https://github.com/stp/stp/archive/$STP_COMMIT_HASH.tar.gz | tar xz --strip-components=1
          ./scripts/deps/setup-gtest.sh
          ./scripts/deps/setup-outputcheck.sh
          ### TODO(@gussmith23): Remove this once https://github.com/stp/stp/pull/482 is merged and you update to new STP.
          cd deps/
          git clone https://github.com/meelgroup/cadical
          cd cadical
          git checkout c90592e
          ./configure 
          make -j"$(nproc)"
          cd ..
          git clone https://github.com/meelgroup/cadiback
          cd cadiback
          git checkout 34236f1 
          ./configure 
          make -j"$(nproc)"
          cd ..
          cd ..
          ### end code to delete.
          ./scripts/deps/setup-cms.sh
          ./scripts/deps/setup-minisat.sh
          mkdir build
          cd build
          cmake -DCMAKE_INSTALL_PREFIX=${{ env.RELEASE_DIR }}/deps/stp/ ..
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ../..
          # It seems wrong that we need to do this manually. Shouldn't they be
          # installed during install?
          cp stp/deps/install/lib/*.so* ${{ env.RELEASE_DIR }}/deps/stp/lib/
          patchelf --set-rpath '$ORIGIN/../lib' ${{ env.RELEASE_DIR }}/deps/stp/lib/*so*
          patchelf --set-rpath '$ORIGIN/../lib' ${{ env.RELEASE_DIR }}/deps/stp/bin/stp

          # Build CVC5.
          pip install pyparsing
          mkdir cvc5 && cd cvc5
          wget -qO- https://github.com/cvc5/cvc5/archive/$CVC5_COMMIT_HASH.tar.gz  | tar xz --strip-components=1
          ./configure.sh --auto-download --prefix=${{ env.RELEASE_DIR }}/deps/cvc5/
          cd ./build
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ../..
          # Manually set the RPATH. Would be nice to do this in a cleaner way.
          patchelf --set-rpath '$ORIGIN/../lib' ${{ env.RELEASE_DIR }}/deps/cvc5/lib/*so*
          patchelf --set-rpath '$ORIGIN/../lib' ${{ env.RELEASE_DIR }}/deps/cvc5/bin/cvc5

        
          # Build Yices2.
          sudo apt-get install -y gperf
          mkdir yices2 && cd yices2
          wget -qO- https://github.com/SRI-CSL/yices2/archive/$YICES2_COMMIT_HASH.tar.gz | tar xz --strip-components=1
          autoconf
          ./configure --prefix=${{ env.RELEASE_DIR }}/deps/yices/
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ..
  
      - name: Build solvers and copy into Rosette (MacOS)
        if: matrix.os-name == 'macOS'
        run: |
          set -x

          source ${{ env.LAKEROAD_DIR }}/dependencies.sh
          
          # Put dummy versions of cvc4 and boolector into Rosette.
          mkdir -p ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/
          cat >${{ matrix.RACKET_PKG_DIR }}/rosette/bin/cvc4 <<'EOF'
          #!/bin/bash
          echo "Please do not use cvc4 with Lakeroad."
          exit 1
          EOF
          chmod +x ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/cvc4
          cat >${{ matrix.RACKET_PKG_DIR }}/rosette/bin/boolector <<'EOF'
          #!/bin/bash
          echo "Please do not use boolector with Lakeroad."
          exit 1
          EOF
          chmod +x ${{ matrix.RACKET_PKG_DIR }}/rosette/bin/boolector

          # Build Bitwuzla.
          NONINTERACTIVE=1 brew install ninja
          mkdir bitwuzla
          wget -qO- https://github.com/bitwuzla/bitwuzla/archive/$BITWUZLA_COMMIT_HASH.tar.gz | tar xz -C bitwuzla --strip-components=1
          cd bitwuzla
          ./configure.py --prefix=${{ env.RELEASE_DIR }}/deps/bitwuzla/
          cd build
          ninja -j${{ env.MAKE_JOBS }}
          ninja -j${{ env.MAKE_JOBS }} install
          cd ../..

          # Install coreutils and make them visible over default mac tools.
          NONINTERACTIVE=1 brew install coreutils
          export PATH="${{ matrix.coreutils_gnubin_path }}:$PATH"

          # Build STP.
          NONINTERACTIVE=1 brew install bison flex boost gmp
          mkdir stp && cd stp
          # TODO(@gussmith23): Change back to normal STP once https://github.com/stp/stp/pull/482 merged.
          #wget -qO- https://github.com/stp/stp/archive/$STP_COMMIT_HASH.tar.gz | tar xz --strip-components=1
          wget -qO- https://github.com/gussmith23/stp/archive/4570d4e8671cd8e4ee872b9a4bdc8bc48a690457.tar.gz | tar xz --strip-components=1
          ./scripts/deps/setup-gtest.sh
          ./scripts/deps/setup-outputcheck.sh
          ./scripts/deps/setup-cms.sh
          ./scripts/deps/setup-minisat.sh
          mkdir build
          cd build
          cmake -DCMAKE_INSTALL_PREFIX=${{ env.RELEASE_DIR }}/deps/stp/ ..
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ../..
          # It seems wrong that we need to do this manually. Shouldn't they be
          # installed during install?
          cp stp/deps/install/lib/*dylib* ${{ env.RELEASE_DIR }}/deps/stp/lib/
          install_name_tool -add_rpath '@executable_path/../lib' ${{ env.RELEASE_DIR }}/deps/stp/bin/stp
          cp stp/deps/cadiback/libcadiback.so ${{ env.RELEASE_DIR }}/deps/stp/lib
          cp stp/deps/cadical/build/libcadical.so ${{ env.RELEASE_DIR }}/deps/stp/lib
          install_name_tool -change libcadiback.so @rpath/libcadiback.so ${{ env.RELEASE_DIR }}/deps/stp/bin/stp
          install_name_tool -change libcadical.so @rpath/libcadical.so ${{ env.RELEASE_DIR }}/deps/stp/bin/stp
          install_name_tool -change libcadical.so @rpath/libcadical.so ${{ env.RELEASE_DIR }}/deps/stp/lib/libcadiback.so

          # Build CVC5.
          pip install pyparsing
          mkdir cvc5 && cd cvc5
          wget -qO- https://github.com/cvc5/cvc5/archive/$CVC5_COMMIT_HASH.tar.gz  | tar xz --strip-components=1
          ./configure.sh --auto-download --prefix=${{ env.RELEASE_DIR }}/deps/cvc5/
          cd ./build
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ../..
          # Manually set the RPATH. Would be nice to do this in a cleaner way.
          install_name_tool -add_rpath '@executable_path/../lib' ${{ env.RELEASE_DIR }}/deps/cvc5/lib/libcvc5.dylib
          # Apparently this one already has this rpath, which will throw an error from install_name_tool.
          #install_name_tool -add_rpath '@executable_path/../lib' ${{ env.RELEASE_DIR }}/deps/cvc5/lib/libcvc5.1.dylib
          install_name_tool -add_rpath '@executable_path/../lib' ${{ env.RELEASE_DIR }}/deps/cvc5/bin/cvc5
          # TODO(@gussmith23): Remove when https://github.com/cvc5/cvc5/issues/10681 resolved.
          install_name_tool -change "/Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpoly.0.dylib" @rpath/libpoly.0.dylib "${{ env.RELEASE_DIR }}/deps/cvc5/lib/libcvc5.1.dylib"
          install_name_tool -change "/Users/runner/work/lakeroad/lakeroad/cvc5/build/deps/lib/libpolyxx.0.dylib" @rpath/libpolyxx.0.dylib "${{ env.RELEASE_DIR }}/deps/cvc5/lib/libcvc5.1.dylib"
        
          # Build Yices2.
          # TODO(@gussmith23): hardcoded versions will break eventually.
          export LDFLAGS="-L/opt/homebrew/Cellar/gmp/6.3.0/lib"
          export CPPFLAGS="-I/opt/homebrew/Cellar/gmp/6.3.0/include"
          NONINTERACTIVE=1 brew install gperf autoconf
          mkdir yices2 && cd yices2
          wget -qO- https://github.com/SRI-CSL/yices2/archive/$YICES2_COMMIT_HASH.tar.gz | tar xz --strip-components=1
          autoconf
          ./configure --prefix=${{ env.RELEASE_DIR }}/deps/yices/
          make -j ${{ env.MAKE_JOBS }}
          make -j ${{ env.MAKE_JOBS }} install
          cd ..

          # Insert an "activate" script (taken from oss-cad-suite)
          cat >${{ env.RELEASE_DIR }}/activate <<'EOF'
          #!/bin/bash
          echo "Please wait"
          echo "Removing quarantine flag from all files ..."
          sudo find . -type f -exec xattr -d com.apple.quarantine {} 2> /dev/null \;
          echo "Done"
          EOF
          chmod +x ${{ env.RELEASE_DIR }}/activate

      - name: Run PyInstaller
        run: pyinstaller --onefile --name lakeroad ${{ env.LAKEROAD_DIR }}/bin/lakeroad-portfolio.py

      - name: Run `raco exe` and `raco distribute` on `bin/main.rkt`
        run: |
          mkdir -p ${{ env.RELEASE_DIR }}/deps/lakeroad/

          # Make a placeholder for the solver binaries. In a later step, we will
          # delete and replace them with symbolic links to the actual binaries,
          # but `raco distribute` expects the files to exist here.
          touch "${{ matrix.RACKET_PKG_DIR }}/rosette/bin/yices-smt2"
          touch "${{ matrix.RACKET_PKG_DIR }}/rosette/bin/stp"
          touch "${{ matrix.RACKET_PKG_DIR }}/rosette/bin/cvc5"
          touch "${{ matrix.RACKET_PKG_DIR }}/rosette/bin/bitwuzla"

          raco exe -v -o lakeroad-single-solver ${{ env.LAKEROAD_DIR }}/bin/main.rkt
          raco distribute -v ${{ env.RELEASE_DIR }}/deps/lakeroad/ lakeroad-single-solver

      - name: Clean up issues after `raco distribute` (Ubuntu, MacOS)
        if: matrix.os-name == 'ubuntu' || matrix.os-name == 'macOS'
        run: |
          # Re-link the solvers.
          # Due to this behavior in Racket:
          # https://github.com/racket/racket/issues/4945
          # we need to re-link the solvers after `raco distribute`. Distribute
          # copies the solvers into the `bin` directory, but it copies the
          # executables themselves, not the symbolic links. The copied
          # executables have broken RPATHS. So simply re-link.
          #
          # Also it's important that these links are relative so that they're
          # relocatable.
          rm ${{ env.RELEASE_DIR }}/deps/lakeroad/lib/plt/lakeroad-single-solver/exts/ert/r1/bin/{stp,yices-smt2,cvc5,bitwuzla}
          ln -f -s ../../../../../../../../yices/bin/yices-smt2  "${{ env.RELEASE_DIR }}/deps/lakeroad/lib/plt/lakeroad-single-solver/exts/ert/r1/bin/yices-smt2"
          ln -f -s ../../../../../../../../stp/bin/stp  "${{ env.RELEASE_DIR }}/deps/lakeroad/lib/plt/lakeroad-single-solver/exts/ert/r1/bin/stp"
          ln -f -s ../../../../../../../../cvc5/bin/cvc5  "${{ env.RELEASE_DIR }}/deps/lakeroad/lib/plt/lakeroad-single-solver/exts/ert/r1/bin/cvc5"
          ln -f -s ../../../../../../../../bitwuzla/bin/bitwuzla  "${{ env.RELEASE_DIR }}/deps/lakeroad/lib/plt/lakeroad-single-solver/exts/ert/r1/bin/bitwuzla"

      - name: Create zip (Windows)
        if: matrix.os-name == 'windows'
        run: |
          7z a lakeroad-${{ matrix.os-name }}.zip lakeroad-single-solver.exe
          # TODO(@gussmith23): Get SHA on Windows.
          # sha256sum lakeroad-${{ matrix.os-name }}.zip > lakeroad-${{ matrix.os-name }}.zip.CHECKSUM

      - name: Create zip (Linux, macOS)
        if: matrix.os-name == 'ubuntu' || matrix.os-name == 'macOS'
        run: |
          mkdir -p ${{ env.RELEASE_DIR }}

          mkdir -p ${{ env.RELEASE_DIR }}/bin
          cat >${{ env.RELEASE_DIR }}/bin/lakeroad <<'EOF'
          #!/bin/bash
          SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
          "$SCRIPT_DIR/../deps/lakeroad/bin/lakeroad" \
            --lakeroad-executable-filepath "$SCRIPT_DIR/../deps/lakeroad/bin/lakeroad-single-solver" \
            $@
          EOF
          chmod +x ${{ env.RELEASE_DIR }}/bin/lakeroad

          cp dist/lakeroad ${{ env.RELEASE_DIR }}/deps/lakeroad/bin/lakeroad

          # Important to preserve symbolic links here, otherwise the work we do
          # to fix the RPATH in the solvers is useless.
          zip --symlinks -r lakeroad-${{ matrix.os-name }}-${{ matrix.arch }}.zip lakeroad
          # TODO(@gussmith23): Doesn't work on Mac, may need to have one case for each OS.
          # sha256sum lakeroad-${{ matrix.os-name }}-${{ matrix.arch }}.zip > lakeroad-${{ matrix.os-name }}-${{ matrix.arch }}.zip.CHECKSUM

      - name: Upload artifact
        uses: actions/upload-artifact@v4
        with:
          path: lakeroad-${{ matrix.os-name }}-${{ matrix.arch }}.zip
          name: lakeroad-${{ matrix.os-name }}-${{ matrix.arch }}.zip
          if-no-files-found: error

      # TODO(@gussmith23): Re-enable once we generate SHA on Windows.
      # - name: Upload checksum
      #   uses: actions/upload-artifact@v4
      #   with:
      #     path: lakeroad-${{ matrix.os-name }}.zip.CHECKSUM
      #     name: lakeroad-${{ matrix.os-name }}.zip.CHECKSUM
      #     if-no-files-found: error

  release:
    name: Create Initial Release
    runs-on: ubuntu-latest
    needs: build
    
    steps:
      - name: Download pre-built artifacts
        uses: actions/download-artifact@v4
        with:
          path: artifacts
          pattern: lakeroad-*
          merge-multiple: true

      - name: Create Release
        uses: ncipollo/release-action@v1
        with:
          tag: ${{ github.ref }}
          name: ${{ github.ref }}
          commit: ${{ github.commit }}
          draft: true
          prerelease: false
          artifactErrorsFailBuild: true
          artifacts: "artifacts/*"