don't depend on cabal sandboxes; add travis

.gitignore

@@ -23,3 +23,6 @@
 /external/ocamlgraph/src/dot_parser.output
 /external/ocamlgraph/src/gml.ml
 /external/ocamlgraph/src/version.ml
+/tests/neg/.liquid/
+/tests/pos/.liquid/
+/external/ocamlgraph/config.log

.travis.yml

@@ -0,0 +1,35 @@
+language: c
+env:
+  - SMT="z3"   GHC="7.8.4"  CABAL="1.18"
+  - SMT="z3"   GHC="7.10.1" CABAL="1.22"
+  - SMT="cvc4" GHC="7.8.4"  CABAL="1.18"
+  - SMT="cvc4" GHC="7.10.1" CABAL="1.22"
+
+branches:
+  only:
+    - master
+
+cache:
+  apt: true
+  directories:
+  - $HOME/.cabal
+  - $HOME/.ghc
+
+before_install:
+ - travis_retry sudo add-apt-repository -y ppa:hvr/ghc
+ - travis_retry sudo apt-get update
+ - travis_retry sudo apt-get install cabal-install-$CABAL ghc-$GHC
+ - export PATH=/opt/ghc/$GHC/bin:/opt/cabal/$CABAL/bin:$PATH
+ - scripts/travis clean_cache "$SMT"
+
+install:
+ - scripts/travis install_cabal_deps
+ - scripts/travis install_smt "$SMT"
+
+script:
+ - scripts/travis do_build && scripts/travis do_test "$SMT" && scripts/travis test_source_pkg
+ - scripts/travis clean_cache "$SMT"
+
+after_failure:
+ - scripts/travis dump_fail_logs
+

Setup.hs

@@ -40,7 +40,7 @@ buildFixpoint _ _ pkg lbi = when build $ do
   setEnv "Z3MEM" (show z3mem)
   executeShellCommand "./configure"
   executeShellCommand "./build.sh"
-  executeShellCommand "chmod a+x external/fixpoint/fixpoint.native "
+  executeShellCommand "chmod a+x external/fixpoint/fixpoint.native"
   where
   allDirs     = absoluteInstallDirs pkg lbi NoCopyDest
   binDir      = bindir allDirs ++ "/"

scripts/travis

@@ -0,0 +1,139 @@
+#!/bin/bash
+
+set -eu
+set -o pipefail
+
+## Helper Functions
+
+function loud {
+  echo "$ $@"
+  $@
+}
+
+# Source: https://github.com/travis-ci/travis-build/blob/fc4ae8a2ffa1f2b3a2f62533bbc4f8a9be19a8ae/lib/travis/build/script/templates/header.sh#L104-L123
+RED="\033[31;1m"
+GREEN="\033[32;1m"
+RESET="\033[0m"
+function travis_retry {
+  local result=0
+  local count=1
+  while [ $count -le 3 ]; do
+    [ $result -ne 0 ] && {
+      echo -e "\n${RED}The command \"$@\" failed. Retrying, $count of 3.${RESET}\n" >&2
+    }
+    set +e
+    "$@"
+    result=$?
+    set -e
+    [ $result -eq 0 ] && break
+    count=$(($count + 1))
+    sleep 1
+  done
+
+  [ $count -eq 4 ] && {
+    echo "\n${RED}The command \"$@\" failed 3 times.${RESET}\n" >&2
+  }
+
+  return $result
+}
+
+function prevent_timeout {
+  local cmd="$@"
+
+  $cmd &
+  local cmd_pid=$!
+
+  poke_stdout &
+  local poke_pid=$!
+
+  wait $cmd_pid
+  exit_code=$?
+
+  kill $poke_pid
+  (wait $poke_pid 2>/dev/null) || true
+
+  return $exit_code
+}
+
+function poke_stdout {
+  # Print an invisible character every minute
+  while true; do
+    echo -ne "\xE2\x80\x8B"
+    sleep 60
+  done
+}
+
+function pastebin {
+  curl -s -F 'clbin=<-' https://clbin.com
+}
+
+## Testing Stages
+
+function clean_cache {
+  local smt="$1"
+
+  loud ghc-pkg unregister liquid-fixpoint --force || true
+  loud rm "$HOME/.cabal/bin/$smt" || true
+}
+
+function install_smt {
+  local smt="$1"
+
+  mkdir -p "$HOME/.cabal/bin"
+  loud curl "http://goto.ucsd.edu/~gridaphobe/$smt" -o "$HOME/.cabal/bin/$smt"
+  loud chmod a+x "$HOME/.cabal/bin/$smt"
+}
+
+function install_cabal_deps {
+  if ! _install_cabal_deps; then
+    echo " ==> Cabal install failed. Clearing dependency cache and retrying."
+    loud rm -rf "$HOME/.cabal"
+    loud rm -rf "$HOME/.ghc"
+    _install_cabal_deps
+  fi
+}
+
+function _install_cabal_deps {
+  loud travis_retry cabal update || return 1
+  loud travis_retry cabal install --reorder-goals --only-dependencies --upgrade-dependencies --enable-tests || return 1
+}
+
+function do_build {
+  loud cabal configure -fbuild-external --enable-tests -v2
+  loud prevent_timeout cabal build -j2
+}
+
+function do_test {
+  local tests="$1"
+  local smt="$2"
+
+  loud prevent_timeout ./dist/build/test/test --smtsolver "$smt" -j2 +RTS -N2 -RTS
+}
+
+function dump_fail_logs {
+  find . -type f -wholename '*/.liquid/*' -name '*.log.fail' -print0 | while IFS= read -r -d $'\0' file; do
+    echo "${file}:"
+    echo "    $(pastebin < "${file}")"
+  done
+}
+
+function test_source_pkg {
+  loud cabal sdist
+
+  local src_tgz="dist/$(cabal info . | awk '{print $2 ".tar.gz";exit}')"
+
+  if [ -f "$src_tgz" ]; then
+    loud prevent_timeout cabal install -j4 "$src_tgz"
+  else
+    echo "expected '$src_tgz' not found"
+    return 1
+  fi
+}
+
+## Run Test Stage
+
+stage="$1"
+shift
+
+$stage "$@"
+

src/Language/Fixpoint/Files.hs

@@ -46,8 +46,11 @@ import           Language.Fixpoint.Misc
 getFixpointPath = fromMaybe msg . msum <$>
                   sequence [ findExecutable "fixpoint.native"
                            , findExecutable "fixpoint.native.exe"
+                             -- fallback for developing in-tree...
+                           , findFile ["external/fixpoint"] "fixpoint.native"
                            ]
-  where msg     = errorstar "Cannot find fixpoint binary [fixpoint.native]"
+  where
+    msg = errorstar "Cannot find fixpoint binary [fixpoint.native]"
 
 getZ3LibPath    = dropFileName <$> getFixpointPath
 

tests/test.hs

@@ -73,7 +73,7 @@ mkTest code dir file
         assertEqual "" True True
       else do
         createDirectoryIfMissing True $ takeDirectory log
-        bin <- canonicalizePath ".cabal-sandbox/bin/fixpoint"
+        bin <- canonicalizePath "dist/build/fixpoint/fixpoint"
         withFile log WriteMode $ \h -> do
           let cmd     = testCmd bin dir file
           (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}