lexec_lnx

#!/bin/bash

# %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The server script

# usage: lexec_lnx
#   [build type] ([source prefix])? ([local sync information])? [remote command] [sync command] [remote command arguments]

# ========================= static configuration
# the directory on the remote machine source trees $HOMEDIR/cvc5-*
HOMEDIR="/space/ajreynol"
# the directory to install the result
INSTALLDIR="/tmp/ajreynol"
# the directory on the remote machine containing the build file structure
if [[ $1 = "debug" ]] || [[ $1 = "debug-unit" ]] || [[ $1 = "asan" ]]; then
  BASEBUILDDIR="/dev/shm/ajreynol/cmake"
else
  BASEBUILDDIR="/tmp/ajreynol"
fi
# the name of the server script (this script)
THISEXEC="lexec_lnx"
# ========================= end static configuration

# %%% BEGIN DO NOT MODIFY THIS COPY, USE CLIENT VERSION
# ================================================== shared method library
# Compute the git source info of directory $1
# Store result in $INFOSRC / $INFOSRCCOMMIT / $INFOSRCCHANGED / $INFOSTRING
function computeSrcInfo 
{
  echo "$THISEXEC: run: cd $1"
  cd $1
  echo "$THISEXEC: compute git information"
  INFOSRC=$(git status | grep -F "On branch ")
  INFOSRC=${INFOSRC#"On branch "}
  INFOSRCCOMMIT=$(git rev-parse HEAD)
  INFOSRCCHANGED=$(git status | grep -F "Changes not staged")
  if [ ! -z "$INFOSRCCHANGED" ]; then
    INFOSTRING="[$INFOSRC ${INFOSRCCOMMIT:0:8} (with modifications)]"
  else
    INFOSTRING="[$INFOSRC ${INFOSRCCOMMIT:0:8}]"
  fi
}
# Compute build information (binary name and configure options) for given build type $1 and optional source prefix $2
# Store result in $BINARYNAME / $CARGS
function computeBuildInfo
{
  BASEBINARYNAME="cvc5"
  if [ $1 = "prod" ]; then
    # production has the default prefix
    BINARYPREFIX=""
    CARGS="production --static"
  elif [ $1 = "debug" ]; then
    BINARYPREFIX="d-"
    CARGS="debug --static --no-unit-testing"
  elif [ $1 = "debug-unit" ]; then
    BINARYPREFIX="du-"
    CARGS="debug"
  elif [ $1 = "asan" ]; then
    BINARYPREFIX="da-"
    CARGS="debug --asan --no-proofs"
  elif [ $1 = "profile" ]; then
    BINARYPREFIX="prof-"
    CARGS="production --static --profiling"
  else
    echo "$THISEXEC: ERROR: unknown build type $1"
    exit 1
  fi
  # if there is a prefix
  if [ ! -z $2 ]; then
    # add the src prefix if it exists
    BINARYPREFIX="$BINARYPREFIX$2-"
  fi
  # add binary program prefix to configure arguments
  if [ ! -z $BINARYPREFIX ]; then
    CARGS="$CARGS --program-prefix=$BINARYPREFIX"
  fi
  CARGS="$CARGS --auto-download"
  # binary name is used for remote install and double checking git scm
  BINARYNAME="$BINARYPREFIX$BASEBINARYNAME"
}
# ================================================== end shared method library
# %%% END DO NOT MODIFY THIS COPY, USE CLIENT VERSION

# usage: lexec_lnx [build type] (-p [prefix])? [command] [sync options] [command options]
echo "=== $THISEXEC $@"
BUILDTYPE=$1
shift
echo "$THISEXEC: build type is $BUILDTYPE"

# ========================= get the source/build directory, local branch
if [ X$1 = X'-p' ]; then
  SRCPREFIX=$2;
  shift;
  shift;
  echo "$THISEXEC: Prefix is $SRCPREFIX"
  SRCDIR="$HOMEDIR/cvc5-$SRCPREFIX"
  BUILDDIR="$BASEBUILDDIR/$SRCPREFIX/$BUILDTYPE/"
else
  SRCDIR="$HOMEDIR/cvc5"
  BUILDDIR="$BASEBUILDDIR/$BUILDTYPE/"
fi
echo "$THISEXEC: source prefix is \"$SRCPREFIX\""
echo "$THISEXEC: source directory is $SRCDIR"
echo "$THISEXEC: install directory is $INSTALLDIR"
echo "$THISEXEC: build directory is $BUILDDIR"
# get information about the state of the local code, based on automatic command line args
# has local indicated that it has called a remote sync operation with this?
if [ X$1 = X'-lsync' ]; then
  shift;
  LOCALSYNC="true"
fi
if [ X$1 = X'-lbranch' ]; then
  LOCALBRANCHREF=$2;
  shift;
  shift;
  echo "$THISEXEC: local source branch reference $LOCALBRANCHREF"
  if [ X$1 = X'-lcommit' ]; then
    LOCALCOMMITREF=$2;
    shift;
    shift;
    echo "$THISEXEC: local source commit reference $LOCALCOMMITREF"
  fi
  # has local indicated that it has not been modified?
  if [ X$1 = X'-lnomod' ]; then
    shift;
    LOCALNOMODIFIED="true"
  fi
fi
# ========================= end get the source/build directory, local branch

COMMAND=$1
shift
# check command that warrant sanity information about src/binary
if [[ "$COMMAND" =~ ^(install|exec|regress|ctest|units|info)$ ]]; then
  REQUIRESSYNC="true"
  # compute source information, which will impact adaptive git syncronization below
  computeSrcInfo $SRCDIR
fi

# ========================= code syncronization
# switch branches if necessary
if [ X$1 = X'-b' ]; then
  BRANCH=$2;
  shift;
  shift;
fi
# rebase, if necessary
if [ X$1 = X'-r' ]; then
  REBASE="true"
  shift;
fi
# get the adaptive syncronization
if [ ! -z "$REQUIRESSYNC" ]; then
  if [ ! -z $LOCALBRANCHREF ]; then
    if [ $LOCALBRANCHREF != $INFOSRC ]; then
      # the remote branch doesn't match, so force a git branch
      echo "$THISEXEC: requires branch"
      if [ -z $BRANCH ]; then
        BRANCH=$LOCALBRANCHREF
        BRANCHFORCE="true"
      fi
    fi
    if [ ! -z $LOCALCOMMITREF ]; then
      if [ $LOCALCOMMITREF != ${INFOSRCCOMMIT:0:8} ]; then
        # the remote commit doesn't match, so force a git rebase
        echo "$THISEXEC: requires rebasing"
        if [ -z $REBASE ]; then
          REBASE="true"
          REBASEFORCE="true"
        fi
      fi
      if [ ! -z "$INFOSRCCHANGED" ]; then
        # local is clean but remote is dirty (case where local reverted to clean after sync in a dirty state, on the same commit)
        if [ ! -z $LOCALNOMODIFIED ]; then
          # just force rebasing to correct
          echo "$THISEXEC: requires rebasing (maybe local was reverted?)"
          if [ -z $REBASE ]; then
            REBASE="true"
            REBASEFORCE="true"
          fi
        fi
      fi
    fi
  fi
fi

# branch or rebase. notice these two options are mutually exclusive since branch subsumes rebase
if [ ! -z "$BRANCH" ]; then
  if [ ! -z $BRANCHFORCE ]; then
    echo "$THISEXEC: NOTICE: forcing git branch switch to $BRANCH"
  fi
  echo "$THISEXEC: run: cd $SRCDIR"
  cd $SRCDIR
  echo "$THISEXEC: run: git checkout ."
  git checkout .
  echo "$THISEXEC: run: git pull --rebase"
  git pull --rebase
  echo "$THISEXEC: run: git checkout $BRANCH"
  if ! git checkout $BRANCH; then
    echo "$THISEXEC:: ERROR: failed to checkout $BRANCH"
    exit 1;
  fi
  echo "$THISEXEC: run: git pull --rebase"
  git pull --rebase
  # ensure git information is up-to-date for check below
  computeSrcInfo $SRCDIR
elif [ ! -z $REBASE ]; then
  if [ ! -z $REBASEFORCE ]; then
    echo "$THISEXEC: NOTICE: forcing git rebase"
  fi
  echo "$THISEXEC: run: cd $SRCDIR"
  cd $SRCDIR
  echo "$THISEXEC: run: git checkout ."
  git checkout .
  echo "$THISEXEC: run: git pull --rebase"
  git pull --rebase
  # ensure git information is up-to-date for check below
  computeSrcInfo $SRCDIR
fi

# Now, check that we are syncronized for commands that warrant sanity information about src/binary.
if [ ! -z "$REQUIRESSYNC" ]; then
  # ensure the same branch as local, or else something went wrong
  if [ -z $LOCALBRANCHREF ]; then
    # internal error, something went wrong in rexec or this script?
    SYNCERROR="(internal error) local did not provide a branch name"
  else
    if [ $LOCALBRANCHREF != $INFOSRC ]; then
      # internal error, something went wrong with remote git?
      echo "$THISEXEC: ERROR: branch mismatch: local [$LOCALBRANCHREF], remote [$INFOSRC], use -B $LOCALBRANCHREF or -b $LOCALBRANCHREF to sync."
      exit 1
    fi
    if [ -z $LOCALCOMMITREF ]; then
      # internal error, something went wrong in rexec or this script?
      SYNCERROR="(internal error) local did not provide a commit number"
    else
      if [ $LOCALCOMMITREF != ${INFOSRCCOMMIT:0:8} ]; then
        # internal error, something went wrong with remote git?
        echo "$THISEXEC: ERROR: branch [$LOCALBRANCHREF] commit mismatch: local [$LOCALCOMMITREF], remote [${INFOSRCCOMMIT:0:8}], perhaps you have made a local commit, use git push to continue."
        exit 1
      fi
      # we are now ensured that the branch/commit matches on local and remote
      # now, ensure we are in the same source code modification state (clean/dirty)
      if [ ! -z "$INFOSRCCHANGED" ]; then
        # local is clean but remote is dirty
        if [ ! -z $LOCALNOMODIFIED ]; then
          # internal error, this case should always be corrected above
          SYNCERROR="(internal error) local is clean, but remote src is dirty"
        fi
        # incremental modifications should continue to use manual sync -s
        if [ -z $LOCALSYNC ]; then
          # the sync may have been correct if local did not have any further changes, hence this is a warning
          SYNCWARNING="local did not use sync -s and remote src is dirty"
        fi
      else
        # remote is clean, probably forgot to sync changes from local
        if [ -z $LOCALNOMODIFIED ]; then
          # we know the sync is wrong, so this is an error
          if [ -z $LOCALSYNC ]; then
            SYNCERROR="local is dirty, but remote src is clean, use -s X or commit changes locally to proceed"
          else
            # user did sync but we had to do a rebase, which dropped the sync
            SYNCERROR="local is dirty, but remote had to be rebased, use -s X again or commit changes locally to proceed"
          fi
        fi
      fi
    fi
  fi
  if [ ! -z "$SYNCERROR" ]; then
    echo "$THISEXEC: ERROR: $SYNCERROR (branch [$LOCALBRANCHREF] commit [$LOCALCOMMITREF])"
    exit 1;
  fi
  if [ ! -z "$SYNCWARNING" ]; then
    echo "$THISEXEC: WARNING: $SYNCWARNING (branch [$LOCALBRANCHREF] commit [$LOCALCOMMITREF])"
  fi
  echo "==============================================="
  echo "RUN COMMAND: $COMMAND"
  echo "REMOTE SOURCE: $INFOSTRING"
  echo "==============================================="
fi
# ========================= end code syncronization


# ========================= compute build and configuration information, again
computeBuildInfo $BUILDTYPE $SRCPREFIX
echo "$THISEXEC: binary name is $BINARYNAME"
# ========================= end compute build and configuration information, again

# ========================= run the command
if [ $COMMAND = "install" ]; then

  echo "$THISEXEC: run: cd $BUILDDIR"
  cd $BUILDDIR
  echo "$THISEXEC: run: ./run_install.sh"
  ./run_install.sh
  if [ $BUILDTYPE = "prod" ]; then
    # strip the binary (so that it is easier to scp from local)
    echo "$THISEXEC: run: strip $HOMEDIR/bin/$BINARYNAME"
    strip $HOMEDIR/bin/$BINARYNAME
  fi
elif [ $COMMAND = "regress" ] || [ $COMMAND = "units" ] || [ $COMMAND = "clean" ]; then

  # these commands are forwarded to make
  echo "$THISEXEC: run: cd $BUILDDIR"
  cd $BUILDDIR
  echo "$THISEXEC: run: make $COMMAND -j8 $@"
  make $COMMAND -j8 $@
  
elif [ $COMMAND = "exec" ]; then

  # a custom executable
  EXECNAME=$1
  shift
  echo "$THISEXEC: run: cd $BUILDDIR"
  cd $BUILDDIR
  echo "$THISEXEC: run: $EXECNAME $@"
  $EXECNAME $@
  
elif [ $COMMAND = "configure" ]; then

  echo "$THISEXEC: run: cd $SRCDIR"
  cd $SRCDIR
  echo "$THISEXEC: run: configure_local $BUILDTYPE"
  configure_local $BUILDTYPE
  
elif [ $COMMAND = "reset" ]; then

  echo "$THISEXEC: run: rm -rf $BUILDDIR"
  rm -rf $BUILDDIR
  
elif [ $COMMAND = "reset-all" ]; then

  echo "$THISEXEC: run: rm -rf $BASEBUILDDIR"
  rm -rf $BASEBUILDDIR
  
elif [ $COMMAND = "ctest" ]; then

  echo "$THISEXEC: run: cd $BUILDDIR"
  cd $BUILDDIR
  echo "$THISEXEC: run: ctest -j8 $@"
  ctest -j8 $@

elif [ $COMMAND = "info" ] || [ $COMMAND = "none" ]; then

  # do nothing
  echo "$THISEXEC: no action required for $COMMAND"
  
else

  echo "rexec: ERROR: unknown command $COMMAND"
  exit 1;
  
fi
# ========================= end run the command

# check command that warrant sanity information about src/binary
if [[ "$COMMAND" =~ ^(install|regress|ctest|units|info)$ ]]; then
  echo "$THISEXEC: run: cd $SRCDIR"
  cd $SRCDIR
  INFOFULLSTRING="REMOTE SOURCE: $INFOSTRING"
  if [[ "$COMMAND" =~ ^(install|info)$ ]]; then
    echo "$THISEXEC: run: $BINARYNAME --show-config | grep scm"
    INFOBINARY=$($BINARYNAME --show-config | grep scm)
    INFOBINARY=${INFOBINARY#"scm           : git "}
    INFOFULLSTRING="$INFOFULLSTRING, BINARY: $INFOBINARY"
  fi
  echo "==============================================="
  echo "FINISHED: $COMMAND"
  echo "$INFOFULLSTRING"
  echo "==============================================="
fi

echo "$THISEXEC: finished $@"