diff --git a/README.md b/README.md
index 38502af095..4e22789d34 100644
--- a/README.md
+++ b/README.md
@@ -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
@@ -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.
 
@@ -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
diff --git a/build.sh b/build.sh
index 889f3ffd7e..4c1539db7c 100755
--- a/build.sh
+++ b/build.sh
@@ -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."
diff --git a/coverage.sh b/coverage.sh
index a49fcd75f1..e86781578b 100755
--- a/coverage.sh
+++ b/coverage.sh
@@ -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
diff --git a/examples/java/arrays.saw b/examples/java/arrays.saw
index ed31f9b163..0adc1a5647 100644
--- a/examples/java/arrays.saw
+++ b/examples/java/arrays.saw
@@ -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] }};
diff --git a/intTests/runtests.sh b/intTests/runtests.sh
index 69fac26e24..362aacb246 100755
--- a/intTests/runtests.sh
+++ b/intTests/runtests.sh
@@ -28,19 +28,6 @@ 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="\\"
@@ -48,7 +35,6 @@ 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.
@@ -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
diff --git a/intTests/test0018_jss_class_load/test.sh b/intTests/test0018_jss_class_load/test.sh
index 430f55d238..ce652b7a2f 100644
--- a/intTests/test0018_jss_class_load/test.sh
+++ b/intTests/test0018_jss_class_load/test.sh
@@ -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'")
diff --git a/stack.ghc-8.6.yaml b/stack.ghc-8.6.yaml
deleted file mode 100644
index aeab9db3cb..0000000000
--- a/stack.ghc-8.6.yaml
+++ /dev/null
@@ -1,66 +0,0 @@
-flags: {}
-packages:
-  - deps/llvm-pretty/
-  - deps/llvm-pretty-bc-parser/
-  - deps/jvm-parser/
-  - deps/aig/
-  - deps/abcBridge/
-  - deps/argo/argo/
-  - deps/cryptol/
-  - deps/cryptol/cryptol-remote-api/
-  - deps/saw-core/cryptol-saw-core/
-  - deps/saw-core/rme/
-  - deps/saw-core/saw-core/
-  - deps/saw-core/saw-core-aig/
-  - deps/saw-core/saw-core-sbv/
-  - deps/saw-core/saw-core-what4/
-  - deps/saw-core-coq/
-  - deps/jvm-verifier/
-  - deps/what4/what4/
-  - deps/what4/what4-abc/
-  - deps/crucible/crucible/
-  - deps/crucible/crucible-jvm/
-  - deps/crucible/crucible-llvm/
-  - deps/crucible/crucible-saw/
-  - deps/crucible/crux/
-  - deps/parameterized-utils/
-  - deps/dwarf/
-  - deps/elf-edit/
-  - deps/flexdis86/
-  - deps/flexdis86/binary-symbols/
-  - deps/macaw/base
-  - deps/macaw/symbolic
-  - deps/macaw/x86
-  - deps/macaw/x86_symbolic
-  - .
-  - saw-remote-api
-extra-deps:
-  - zenc-0.1.1@sha256:e4be3e5e9fe1a1ade05910909c6e5b5a8eff72e697868b03955c9781b0443947
-  - IfElse-0.85
-  - QuickCheck-2.14
-  - splitmix-0.0.4
-  - fgl-visualize-0.1.0.1
-  - simple-smt-0.9.4
-  - GraphSCC-1.0.4
-  - monadLib-3.10
-  - panic-0.4.0.1
-  - itanium-abi-0.1.1.1
-  - boomerang-1.4.6
-  - config-schema-1.2.0.0
-  - config-value-0.7.0.1
-  - simple-get-opt-0.3
-  - base-orphans-0.8.2
-  - splitmix-0.0.4
-  - bv-sized-1.0.1
-  - bitwise-1.0.0.1
-  - sbv-8.6
-  - libBF-0.5.1
-  - hashable-1.3.0.0
-  - lens-4.19.2
-  - network-3.1.1.1
-  - scotty-0.12
-  - modern-uri-0.3.3.0
-  - prettyprinter-1.7.0
-  - prettyprinter-ansi-terminal-1.1.2
-resolver: lts-14.27
-allow-newer: false
diff --git a/stack.ghc-8.8.yaml b/stack.ghc-8.8.yaml
deleted file mode 100644
index a3fab9657f..0000000000
--- a/stack.ghc-8.8.yaml
+++ /dev/null
@@ -1,59 +0,0 @@
-flags: {}
-packages:
-  - deps/llvm-pretty/
-  - deps/llvm-pretty-bc-parser/
-  - deps/jvm-parser/
-  - deps/aig/
-  - deps/abcBridge/
-  - deps/argo/argo/
-  - deps/cryptol/
-  - deps/cryptol/cryptol-remote-api/
-  - deps/saw-core/cryptol-saw-core/
-  - deps/saw-core/rme/
-  - deps/saw-core/saw-core/
-  - deps/saw-core/saw-core-aig/
-  - deps/saw-core/saw-core-sbv/
-  - deps/saw-core/saw-core-what4/
-  - deps/saw-core-coq/
-  - deps/jvm-verifier/
-  - deps/what4/what4/
-  - deps/what4/what4-abc/
-  - deps/crucible/crucible/
-  - deps/crucible/crucible-jvm/
-  - deps/crucible/crucible-llvm/
-  - deps/crucible/crucible-saw/
-  - deps/crucible/crux/
-  - deps/parameterized-utils/
-  - deps/dwarf/
-  - deps/elf-edit/
-  - deps/flexdis86/
-  - deps/flexdis86/binary-symbols/
-  - deps/macaw/base
-  - deps/macaw/symbolic
-  - deps/macaw/x86
-  - deps/macaw/x86_symbolic
-  - .
-  - saw-remote-api
-extra-deps:
-  - zenc-0.1.1@sha256:e4be3e5e9fe1a1ade05910909c6e5b5a8eff72e697868b03955c9781b0443947
-  - IfElse-0.85
-  - fgl-visualize-0.1.0.1
-  - simple-smt-0.9.4
-  - GraphSCC-1.0.4
-  - monadLib-3.10
-  - sbv-8.6
-  - panic-0.4.0.1
-  - itanium-abi-0.1.1.1
-  - boomerang-1.4.6
-  - config-schema-1.2.0.0
-  - config-value-0.7.0.1
-  - simple-get-opt-0.4
-  - json-0.10
-  - bv-sized-1.0.1
-  - bitwise-1.0.0.1
-  - libBF-0.5.1
-  - scotty-0.12
-  - prettyprinter-1.7.0
-  - prettyprinter-ansi-terminal-1.1.2
-resolver: lts-16.2
-allow-newer: false
diff --git a/stage.sh b/stage.sh
index 810c5dc6ab..661b75487f 100755
--- a/stage.sh
+++ b/stage.sh
@@ -42,9 +42,7 @@ mkdir -p ${TARGET}/lib
 
 echo Staging ...
 
-# Workaround bug which prevents using `stack path --local-install-root`:
-# https://github.com/commercialhaskell/stack/issues/604.
-BIN=$(stack path | sed -ne 's/local-install-root: //p')/bin
+BIN=`pwd`/bin
 
 if [ "${OS}" != "Windows_NT" ]; then
   strip "$BIN"/*