Skip to content

Commit

Permalink
Remove dependency on Stack (#988)
Browse files Browse the repository at this point in the history
This removes the dependency on Stack, in several ways:

* Removes the use of Stack in the test suite.
* Updates `build.sh` to use `cabal build`.
* Updates coverage.sh to use `cabal build --enable-coverage`.
* Updates the README to describe how to build with `cabal`.
* Removes Stack configuration files.

It also fixes a broken test along the way.
  • Loading branch information
Aaron Tomb committed Jan 13, 2021
1 parent d133abd commit 21565d7
Show file tree
Hide file tree
Showing 9 changed files with 53 additions and 296 deletions.
54 changes: 6 additions & 48 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,11 +38,9 @@ is on your PATH.

To build SAWScript and related utilities from source:

* Ensure that you have the
[Stack](https://github.com/commercialhaskell/stack) program on your
`PATH`. If you don't already have Stack, then `cabal install stack`,
or download a precompiled binary from
https://github.com/commercialhaskell/stack/releases.
* Ensure that you have the `cabal` and `ghc` executables in your
`PATH`. If you don't already have them, we recommend using `ghcup`
to install them: <https://www.haskell.org/ghcup/>

* Ensure that you have the C libraries and header files for
`terminfo`, which generally comes as part of `ncurses` on most
Expand All @@ -53,49 +51,15 @@ To build SAWScript and related utilities from source:
`PATH`. Z3 binaries are available at
https://github.com/Z3Prover/z3/releases

* Setup a `stack.yaml` for your OS and preferred GHC.
* Optionally, put in place dependency version freeze files:

Choose one of the Stack YAML config files and link it to
`stack.yaml`:

ln -s stack.<ghc version and os>.yaml stack.yaml

The `stack-<ghc version>-unix.yaml` files are for both Linux and
OS X.

(Alternatively, you can

export STACK_YAML=stack.<ghc version and os>.yaml

instead of creating a symlink.

**Developers**: defining a `STACK_YAML` env var also overrides the
`stack.yaml` file, if any, and so is useful for testing a
alternative build without permanently changing your default. You
can even define `STACK_YAML` only for the current command: e.g.

STACK_YAML=stack.<ghc version and os>.yaml stack build

will build SAWScript using the given Stack YAML.)
ln -s cabal.<ghc version>.config cabal.project.freeze

* Build SAWScript by running

./build.sh

The SAWScript executables will be created in

echo `stack path --local-install-root`/bin

a path under the SAWScript repo. You can install SAWScript into
a more predictable location by running

stack install

which installs into

stack path --local-bin-path

which is `$HOME/.local/bin` by default.
The SAWScript executables will be available in the `bin` directory.

* Optionally, run ./stage.sh to create a binary tarball.

Expand Down Expand Up @@ -139,12 +103,6 @@ If you are using `cabal` to build, select the `saw-script` target:
$ cabal new-repl saw-script
```

If you are using `stack` to build, select the `saw-script` *library* target:

```
$ stack repl saw-script:lib
```

In order to use interactive tools like `intero`, you need to configure them with
this target. You can configure `intero-mode` in Emacs to use the `saw-script`
library target by setting the variable `intero-targets` to the string
Expand Down
106 changes: 11 additions & 95 deletions build.sh
Original file line number Diff line number Diff line change
@@ -1,102 +1,18 @@
#!/bin/bash
set -x
set -v
set -e
git submodule update --init
(cd deps/abcBridge && git submodule update --init)

TESTABLE="abcBridge jvm-verifier parameterized-utils saw-core"
function install() {
cp $(find dist-newstyle -type f -name $1 | sort -g | tail -1) bin/
}

dotests="false"
jobs=""
while getopts "tpfj:" opt; do
case $opt in
t)
dotests="true"
;;
j)
jobs="-j$OPTARG"
;;
\?)
echo "Invalid option: -$OPTARG" >&2
exit 1
;;
esac
done
cabal build exe:cryptol exe:jss exe:saw exe:saw-remote-api

git submodule init
git submodule update
(cd deps/abcBridge && git submodule init && git submodule update)
rm -rf bin && mkdir bin
install cryptol
install jss
install saw
install saw-remote-api

if [ ! -e stack.yaml -a -z "$STACK_YAML" ] ; then
set +x
echo
echo "ERROR: no stack.yaml file found."
echo
echo "Select one of the given stack configuration files using:"
echo
echo " ln -s stack.<ghc version and os>.yaml stack.yaml"
exit 1
fi

stack setup

LOCALBINPATH=$(stack path --local-bin-path | tr -d '\r\n')
if [ "${OS}" == "Windows_NT" ] ; then
HERE=$(cygpath -w $(pwd))
PATH=$PATH:$(cygpath -u -a $LOCALBINPATH)
else
HERE=$(pwd)
PATH=$PATH:$LOCALBINPATH
fi

stack="stack $jobs"

${stack} install alex
${stack} install happy
${stack} install c2hs

which alex
which happy
which c2hs

if [ "${dotests}" == "true" ] ; then
if [ -z ${TEST_TIMEOUT} ]; then
TEST_TIMEOUT="120s"
fi

mkdir -p tmp
for pkg in ${TESTABLE}; do
test_arguments="--xml=${HERE}/tmp/${pkg}-test-results.xml --timeout=${TEST_TIMEOUT}"

if [ ! "${QC_TESTS}" == "" ]; then
test_arguments="${test_arguments} --quickcheck-tests=${QC_TESTS}"
fi

# Stack is returning 1 when a test fails, which kills the whole
# build. Presumably Cabal returned 0 in this case.
#
# If the build part of the test fails, there won't be any XML
# file, so we'll detect failure in that case when we check for the
# XML file below.
(
set +e
${stack} build --test --test-arguments="${test_arguments}" ${pkg}
exit 0
)

if [ -e tmp/${pkg}-test-results.xml ]; then
xsltproc jenkins-junit-munge.xsl tmp/${pkg}-test-results.xml > tmp/jenkins-${pkg}-test-results.xml
else
echo "Missing test results: tmp/${pkg}-test-results.xml"
exit 1
fi
done
else
${stack} build
fi

# Link bin directory to a more convenient location
rm -f bin
ln -s `stack path --local-install-root`/bin
set +x +v
echo
echo "COPIED EXECUTABLES TO `pwd`/bin."
31 changes: 27 additions & 4 deletions coverage.sh
Original file line number Diff line number Diff line change
@@ -1,9 +1,32 @@
#!/bin/bash

stack build --coverage
cabal build --enable-coverage exe:jss exe:saw

(cd intTests && ./runtests.sh)
# This conflicts with GitRev.mix in `saw-script`. Yuck.
rm -f ./dist-newstyle/build/*/ghc-*/cryptol-*/**/GitRev.mix

hpc sum --output=saw.tix --union --exclude=Main `find intTests -name "*.tix"`
(cd intTests && CABAL_FLAGS="--enable-coverage" ./runtests.sh)

stack hpc report --destdir=coverage saw.tix
hpc sum --output=saw.tix --union --exclude=Main $(find intTests -name saw.tix)

HPC_ARGS="--destdir=coverage"

# Collect up all the directories where `.mix` files might live. This is
# horrendous.
HPC_DIRS=$(find dist-newstyle -name "*.mix" | xargs -n 1 dirname | sort -u | grep -v dyn)
HPC_DIRS2=$(find dist-newstyle -name "*.mix" | xargs -n 1 dirname | xargs -n 1 dirname | sort -u | grep -v dyn)
for dir in ${HPC_DIRS}; do
HPC_ARGS="${HPC_ARGS} --hpcdir=${dir}"
done
for dir in ${HPC_DIRS2}; do
HPC_ARGS="${HPC_ARGS} --hpcdir=${dir}"
done

# Add the top-level directory of each dependency package to the source
# file search path.
HPC_ARGS="${HPC_ARGS} --srcdir=."
for dir in $(cat cabal.project | grep -v : | grep -v "\.cabal") ; do
HPC_ARGS="${HPC_ARGS} --srcdir=${dir}"
done

hpc markup ${HPC_ARGS} saw.tix
4 changes: 2 additions & 2 deletions examples/java/arrays.saw
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@ let main : TopLevel () = do {
sum_ms <- java_verify c "sum" [] sum_setup;
comp_ms <- java_verify c "comp" [unit_ms] comp_setup;
print "Extracting model of sum, which has type:";
sum_tm <- jvm_extract c "sum" sum_setup';
id_tm <- jvm_extract c "arr_id" id_setup;
sum_tm <- java_extract c "sum" sum_setup';
id_tm <- java_extract c "arr_id" id_setup;
check_term sum_tm;
print "Running sum on ten 1 inputs:";
print {{ sum_tm [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] }};
Expand Down
18 changes: 2 additions & 16 deletions intTests/runtests.sh
Original file line number Diff line number Diff line change
Expand Up @@ -28,27 +28,13 @@ fi

JSS_BASE=$TESTBASE/../deps/jvm-verifier

# define the BIN variable, if not already defined
if [ -z "$BIN" ]; then
# Workaround bug which prevents using `stack path --local-install-root`:
# https://github.com/commercialhaskell/stack/issues/604.
BIN="$(cd "$TESTBASE"/.. &&
stack path | sed -ne 's/local-install-root: //p')"/bin
if [ "$OS" = "Windows_NT" ]; then
# Stack returns Windows paths on Windows, but we're using Cygwin so
# we want Unix paths.
BIN=$(cygpath -u "$BIN")
fi
fi

if [ "${OS}" == "Windows_NT" ]; then
export CPSEP=";"
export DIRSEP="\\"
else
export CPSEP=":"
export DIRSEP="/"
fi
export PATH=$BIN:$PATH

# Build the class path. On Windows, Java requires Windows-style paths
# here, even in Cygwin.
Expand All @@ -68,8 +54,8 @@ export CP

# We need the 'eval's here to interpret the single quotes protecting
# the spaces and semi-colons in the Windows class path.
export SAW="eval saw -j '$CP'"
export JSS="eval jss -j '$CP' -c ."
export SAW="eval cabal run ${CABAL_FLAGS} saw -- -j '$CP'"
export JSS="eval cabal run ${CABAL_FLAGS} jss -- -j '$CP' -c ."

# Figure out what tests to run
if [[ -z "$*" ]]; then
Expand Down
7 changes: 4 additions & 3 deletions intTests/test0018_jss_class_load/test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ else
fi
cp=${BASE}${DIRSEP}a${CPSEP}${BASE}${DIRSEP}b${CPSEP}.
sawfile=${BASE}${DIRSEP}test.saw
(cd / && $JSS -c "'$cp'" org/example/Test)
(cd / && $JSS -c "'$cp'" com/example/Test)
(cd / && $SAW -c "'$cp'" "'$sawfile'")
rm -rf tmp?
(mkdir tmp1 && cd tmp1 && $JSS -c "'$cp'" org/example/Test)
(mkdir tmp2 && cd tmp2 && $JSS -c "'$cp'" com/example/Test)
(mkdir tmp3 && cd tmp3 && $SAW -c "'$cp'" "'$sawfile'")
66 changes: 0 additions & 66 deletions stack.ghc-8.6.yaml

This file was deleted.

Loading

0 comments on commit 21565d7

Please sign in to comment.