diff --git a/.devcontainer/fromscratch/minimal.Dockerfile b/.devcontainer/fromscratch/minimal.Dockerfile
index 90d828fa9..e2c4217ad 100644
--- a/.devcontainer/fromscratch/minimal.Dockerfile
+++ b/.devcontainer/fromscratch/minimal.Dockerfile
@@ -67,7 +67,7 @@ RUN eval $(opam env) \
  && .docker/build/install-other-deps.sh \
  && make -j$(nproc)
 
-ENV FSTAR_HOME $HOME/FStar
+ENV FSTAR_EXE  $HOME/FStar/bin/fstar.exe
 ENV KRML_HOME $HOME/karamel
 
 # Instrument .profile and .bashrc to set the opam switch. Note that this
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 62bc8f4cd..cc6dc645b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -48,7 +48,7 @@ jobs:
           path: FStar
           key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}
 
-      - run: echo "FSTAR_HOME=$(pwd)/FStar" | sudo tee -a $GITHUB_ENV
+      - run: echo "FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe" | sudo tee -a $GITHUB_ENV
 
       - uses: actions/checkout@master
         id: checkout-karamel
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 3628284f2..1f439d638 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -114,28 +114,6 @@ See F* PR https://github.com/FStarLang/FStar/pull/3363
 
 
 
-## Modifying the Pulse or PulseC extraction rules, or the syntax extension
-
-If you modify the Pulse or PulseC
-extraction rules in `src/extraction` (`ExtractPulse.fst` and
-`ExtractPulseC.fst` respectively), or the syntax extension in
-`src/syntax-extension`, you need to regenerate the corresponding OCaml
-snapshot.
-
-To do so, you need to clone the F* repository and set the `FSTAR_HOME`
-variable to your F* clone. Indeed, the extraction rules typecheck
-against the F* sources. An opam installation of F* (or a binary
-package) will not work.
-
-Optionally, to extract C code, you must set the `KRML_HOME` environment
-variable. This should point to your clone of the Karamel repository.
-
-Then, you can extract the rules and recompile everything with `make -j
-boot` from the Pulse root directory.
-
-Alternatively, you can do `make -j full-boot`, which will remove all
-generated OCaml files beforehand.
-
 ## Testing
 
 There are simple tests in `test/` and examples in `share/pulse`.
@@ -155,7 +133,5 @@ This will also verify all examples and tests, by moving them outside of
 the Pulse directory hierarchy beforehand, to make sure that the location
 of those examples does not need to depend on the location of Pulse.
 
-Finally, you can run `make -j ci` to re-extract, recompile and re-test
-everything. If you have Docker, you can run the `ci` rule with `docker
-build -f ci/ci.Dockerfile .` which will also install all dependencies
-automatically.
+Finally, you can run `make -j ci` to compile and re-test
+everything.
diff --git a/README.md b/README.md
index f915da043..57755c530 100644
--- a/README.md
+++ b/README.md
@@ -24,9 +24,8 @@ For documentation on how to use Pulse, see https://fstar-lang.org/tutorial/book/
 
 1. Make sure `fstar.exe` is in your `PATH`. If F* was installed with
    opam, you may need to run `eval $(opam env)`. If F* is not in your
-   `PATH`, set the `FSTAR_HOME` environment variable to the directory
-   where F* was installed (or to the F* source tree), so that the F*
-   executable should be in `$FSTAR_HOME/bin/fstar.exe`.
+   `PATH`, set the `FSTAR_EXE` environment variable to the location
+   of fstar.exe.
 2. Run `make` (possibly with `-j`). This will generate a local
    installation under the `out/` subdirectory, identical to the ones
    created by the other options below.
diff --git a/ci/.gitignore b/ci/.gitignore
deleted file mode 100644
index 2bf1eb4f6..000000000
--- a/ci/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-pulse
-pulse.zip
-pulse.tar.gz
diff --git a/ci/ci.Dockerfile b/ci/ci.Dockerfile
deleted file mode 100644
index 9a79e8502..000000000
--- a/ci/ci.Dockerfile
+++ /dev/null
@@ -1,68 +0,0 @@
-# This Dockerfile should be run from the root Pulse directory
-
-ARG ocaml_version=4.14
-FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version
-
-RUN sudo apt-get install -y wget coreutils
-
-# Install the Z3 versions we want to use in CI (4.8.5, 4.13.3). Note: we
-# currently also have 4.8.5 in the opam switch, as it is a dependency of
-# in fstar.opam, but that should be removed.
-
-USER root
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
- && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
- && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 /usr/local/bin/z3-4.8.5 \
- && rm -r z3-4.8.5-*
-
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip \
- && unzip z3-4.13.3-x64-glibc-2.35 \
- && cp z3-4.13.3-x64-glibc-2.35/bin/z3 /usr/local/bin/z3-4.13.3 \
- && rm -r z3-4.13.3-*
-USER opam
-
-# CI dependencies for the Wasm11 test: node.js
-RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
-RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs libgmp-dev pkg-config
-
-# install rust
-RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang libgmp-dev pkg-config
-RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
-
-ARG opamthreads=24
-
-# Install F* and Karamel from the Karamel CI install script
-# FIXME: the `opam depext` command should be unnecessary with opam 2.1
-ADD --chown=opam:opam ci/config.json pulse/ci/config.json
-ENV FSTAR_HOME=$HOME/FStar
-ENV KRML_HOME=$HOME/karamel
-RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
-    wget \
-    jq \
-    && \
-    git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
-    eval $(opam env) && \
-    opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
-    opam install --deps-only $FSTAR_HOME/fstar.opam && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads && \
-    git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
-    eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads
-
-# FIXME: The recent changes to MLish and bootstrapping mean that we must
-# not try to check prims.fst or the rest of ulib in --MLish mode, since
-# some files fail to do so. This will happen when trying to extract the
-# files in src/syntax_extension, as there are no checked files for them.
-# So, call the F* makefile to bootstrap F* and generate the files. This
-# is probably only a bandaid... but I'm not sure what the best thing to
-# do is.
-RUN eval $(opam env) && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads bootstrap
-
-# Pulse CI proper
-ADD --chown=opam:opam ./ pulse/
-ARG OTHERFLAGS
-RUN eval $(opam env) && . $HOME/.cargo/env && make -k -j $opamthreads -C pulse ci
-
-ENV PULSE_HOME $HOME/pulse
diff --git a/ci/config.json b/ci/config.json
deleted file mode 100644
index a07864071..000000000
--- a/ci/config.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-    "RepoVersions" : {
-        "fstar": "master",
-        "karamel" : "master"
-    },
-    "NotificationChannel" : "#pulse-build"
-}
diff --git a/ci/hierarchic.Dockerfile b/ci/hierarchic.Dockerfile
deleted file mode 100644
index 9d586a16d..000000000
--- a/ci/hierarchic.Dockerfile
+++ /dev/null
@@ -1,31 +0,0 @@
-# This Dockerfile should be run from the root Pulse directory
-
-ARG FSTAR_BRANCH=master
-FROM fstar:local-branch-$FSTAR_BRANCH
-
-# CI dependencies for the Wasm11 test: node.js
-RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
-RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends nodejs libgmp-dev pkg-config
-
-# install rust
-RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang
-RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
-
-ADD --chown=opam:opam ./ $HOME/pulse
-WORKDIR $HOME/pulse
-
-ARG opamthreads=24
-
-# Install Karamel
-ENV KRML_HOME $HOME/pulse_tools/karamel
-RUN mkdir -p $HOME/pulse_tools && \
-    git clone --branch $(jq -c -r '.RepoVersions.karamel' $HOME/pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
-    eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads
-
-# Pulse CI proper
-ARG OTHERFLAGS
-RUN eval $(opam env) && . "$HOME/.cargo/env" && make -k -j $opamthreads -C $HOME/pulse ci
-
-ENV PULSE_HOME $HOME/pulse
diff --git a/ci/no-fstar-home.Dockerfile b/ci/no-fstar-home.Dockerfile
deleted file mode 100644
index 665c36041..000000000
--- a/ci/no-fstar-home.Dockerfile
+++ /dev/null
@@ -1,42 +0,0 @@
-# This Dockerfile should be run from the root Pulse directory
-
-ARG ocaml_version=4.14
-FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version
-
-ARG opamthreads=24
-
-# CI dependencies for the Wasm11 test: node.js
-# The sed call is a workaround for these upstream issues... sigh.
-# https://github.com/nodesource/distributions/issues/1576
-# https://github.com/nodesource/distributions/issues/1593
-# Remove when they are solved
-RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sed 's,https://deb.nodesource.com,http://deb.nodesource.com,' | sudo -E bash -
-RUN sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang
-RUN sudo apt-get install -y --no-install-recommends nodejs
-
-# install rust
-RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
-
-ADD --chown=opam:opam ./ pulse/
-
-# Install F* and Karamel from the Karamel CI install script
-# FIXME: the `opam depext` command should be unnecessary with opam 2.1
-ENV KRML_HOME=$HOME/karamel
-RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
-    jq \
-    && \
-    git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $HOME/FStar && \
-    eval $(opam env) && \
-    opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
-    opam install --deps-only $HOME/FStar/fstar.opam && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $HOME/FStar -j $opamthreads && \
-    git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
-    eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
-    env FSTAR_HOME=$HOME/FStar OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads
-
-ENV PATH=$HOME/FStar/bin:$PATH
-
-# Pulse CI proper
-ARG OTHERFLAGS
-RUN eval $(opam env) && . "$HOME/.cargo/env" && make -k -j $opamthreads -C pulse ci
diff --git a/ci/opam.Dockerfile b/ci/opam.Dockerfile
deleted file mode 100644
index ef4ed0ab8..000000000
--- a/ci/opam.Dockerfile
+++ /dev/null
@@ -1,29 +0,0 @@
-# This Dockerfile should be run from the root Pulse directory
-
-ARG ocaml_version=4.14
-FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version
-
-ARG opamthreads=24
-
-ADD --chown=opam:opam ./ pulse/
-
-# FIXME: the `opam depext` command should be unnecessary with opam 2.1
-RUN sudo apt-get update && \
-    sudo apt-get install --yes --no-install-recommends jq && \
-    opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
-    git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar FStar && \
-    opam install -j $opamthreads -v -v -v FStar/fstar.opam && \
-    rm -rf FStar
-
-RUN eval $(opam env) && \
-    opam install -j $opamthreads -v -v -v pulse/pulse.opam
-
-ARG OTHERFLAGS
-
-RUN cp -p -r pulse/share/pulse /tmp/pulse-share && \
-    rm -rf pulse /tmp/pulse-share/Makefile.include && \
-    eval $(opam env) && \
-    env PULSE_HOME=$(opam config var prefix) make -j $opamthreads -k -C /tmp/pulse-share
-
-RUN eval $(opam env) && \
-    opam uninstall pulse
diff --git a/ci/package-README.md b/ci/package-README.md
deleted file mode 100644
index 231c4b81b..000000000
--- a/ci/package-README.md
+++ /dev/null
@@ -1,85 +0,0 @@
-# The Pulse separation logic DSL for F*
-
-## Contents of this package
-
-This binary package contains z3 4.8.5, F*, Karamel, Pulse, and
-(except on Windows) Pulse2Rust:
-
-* in `bin`: the executables for z3, F* and Karamel
-
-* in `lib/pulse`:
-  * the Pulse F* plugin, `pulse.cmxs`, containing the Pulse checker,
-    and the Pulse and PulseC extraction rules to krml, is installed
-    here
-  * the Pulse standard library, of the `Pulse` and `PulseCore`
-    namespaces (including PulseC's `Pulse.C`)
-
-* in `share/pulse`: `Makefile.include`, the GNU Make rules to verify
-  Pulse code
-
-* in `pulse2rust`: the executable for Pulse2Rust. (Absent from the
-  Windows binary package)
-
-## Using Pulse
-
-### Writing a Makefile to verify Steel or Pulse code
-
-
-Pulse comes with `share/pulse/Makefile.include` (which is also
-properly installed by `make install` or via opam), which contains the
-GNU Make rules to call F* with the Pulse include path and the Pulse
-plugin loaded.
-
-1. Make sure `fstar.exe` is in your `PATH`. If F* was installed with
-   opam, you may need to run `eval $(opam env)`. Alternatively,
-   instead of having F* in your `PATH`, you can also set the
-   `FSTAR_HOME` environment variable to the directory where F* was
-   installed (or to the F* source tree), so that the F* executable
-   should be in `$FSTAR_HOME/bin/fstar.exe`.
-
-2. Define the `PULSE_HOME` environment variable. This should be one of the following:
-   * If used directly from source: The root directory of your clone of the Pulse repository
-   * If installed with `make install`: The PREFIX directory used when installing Pulse
-   * If installed with `opam`: The prefix directory of the opam
-     switch where Pulse was installed, obtained with `opam config var prefix`
- 
-3. (Optional) In your Makefile, define the following variables with `+=` or `:=` :
-   * `SRC_DIRS`: the directories containing the source `.fst` and
-     `.fsti` files of your project, in addition to the current
-     directory.
-   * `FSTAR_FILES`: the F* files to verify. By default, those are the
-     `*.fst` and `*.fsti` files from the directories in `SRC_DIRS`
-   * `INCLUDE_PATHS`: the paths to include for verification with F*'s
-     `--include` option. By default, those are the Pulse library
-     include paths and `SRC_DIRS`.
-     * If you want to use PulseC, add `$PULSE_HOME/lib/pulse/c` to
-       this variable.
-   * `ALREADY_CACHED_LIST`: the comma-separated list of namespaces
-     that are assumed to be already cached. By default
-     `Prims,FStar,PulseCore,Pulse`, but if all of your source files
-     are in the same namespace, you can override this variable with
-     something like `*,-MyNamespace`
-   * `OTHERFLAGS`: additional options to pass to F*.
-   * `FSTAR_DEP_OPTIONS`: additional options to pass to F* to compute
-     dependencies (in addition to `FSTAR_OPTIONS`), such as `--extract`
-   * `FSTAR_ML_CODEGEN`: useful only if you want to extract OCaml
-     code. If you want to extract a F* plugin, set this option to
-     `Plugin`. Otherwise, it is set by default to `OCaml`.
-
-4. After those variable definitions, insert `include
-   $PULSE_HOME/share/pulse/Makefile.include` to your Makefile.
-
-5. In your project directory, run `make -j verify`
-
-### Calling F* directly
-
-If you already have an existing `Makefile` for your Pulse-based
-project, you now need to pass new options to your Makefile to use
-Pulse from this repository, as described in this section.
-
-To call F* with Pulse:
-
-1. Make sure F* and Pulse are properly located, following steps 1 and 2 above.
-2. Pass the following options to F*:
-   * in all cases, `--include $PULSE_HOME`
-   * if you want to use PulseC, add `--include $PULSE_HOME/lib/pulse/c`
diff --git a/ci/package.Dockerfile b/ci/package.Dockerfile
deleted file mode 100644
index ab4887dd5..000000000
--- a/ci/package.Dockerfile
+++ /dev/null
@@ -1,62 +0,0 @@
-# This Dockerfile should be run from the root Pulse directory
-
-ARG ocaml_version=4.14
-FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version
-
-# CI dependencies for the Wasm11 test: node.js
-RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
-RUN sudo apt-get install -y --no-install-recommends nodejs
-
-# install rust
-RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-
-ARG opamthreads=24
-
-# (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
-# CI dependencies: .NET Core
-# Repository install may incur some (transient?) failures (see for instance https://github.com/dotnet/sdk/issues/27082 )
-# So, we use manual install instead, from https://docs.microsoft.com/en-us/dotnet/core/install/linux-scripted-manual#manual-install
-ENV DOTNET_ROOT /home/opam/dotnet
-RUN sudo apt-get install --yes --no-install-recommends \
-    libicu-dev \
-    wget \
-    && \
-    wget https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
-    mkdir -p $DOTNET_ROOT && \
-    tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT
-
-ENV PATH=${PATH}:$DOTNET_ROOT:$DOTNET_ROOT/tools
-
-ADD --chown=opam:opam ./ pulse/
-
-# Install F* and Karamel from the Karamel CI install script
-# FIXME: the `opam depext` command should be unnecessary with opam 2.1
-ENV FSTAR_HOME=$HOME/FStar
-ENV KRML_HOME=$HOME/karamel
-RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
-    wget \
-    jq \
-    && \
-    git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
-    eval $(opam env) && \
-    opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
-    opam install --deps-only $FSTAR_HOME/fstar.opam && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads && \
-    git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
-    eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads
-
-# FIXME: The recent changes to MLish and bootstrapping mean that we must
-# not try to check prims.fst or the rest of ulib in --MLish mode, since
-# some files fail to do so. This will happen when trying to extract the
-# files in src/syntax_extension, as there are no checked files for them.
-# So, call the F* makefile to bootstrap F* and generate the files. This
-# is probably only a bandaid... but I'm not sure what the best thing to
-# do is.
-RUN eval $(opam env) && \
-    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads bootstrap
-
-# Produce the binary package
-RUN eval $(opam env) && . $HOME/.cargo/env && pulse/ci/package.sh -j $opamthreads
-
-ENV PULSE_HOME $HOME/pulse
diff --git a/ci/package.sh b/ci/package.sh
deleted file mode 100755
index 35e751177..000000000
--- a/ci/package.sh
+++ /dev/null
@@ -1,91 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-set -x
-
-if [[ -z "$OS" ]] ; then
-    OS=$(uname)
-fi
-
-is_windows=false
-if [[ "$OS" = "Windows_NT" ]] ; then
-   is_windows=true
-fi
-
-fixpath () {
-    if $is_windows ; then
-        cygpath -m "$1"
-    else
-        echo "$1"
-    fi
-}
-
-cp0=$(which gcp >/dev/null 2>&1 && echo gcp || echo cp)
-cp="$cp0 --preserve=mode,timestamps"
-make="$(which gmake >/dev/null 2>&1 && echo gmake || echo make)"
-
-# make sure the package has not already been built
-cd $(cd `dirname $0` && pwd)
-[[ ! -e pulse ]]
-
-# download the z3 license file
-if ! [[ -f LICENSE-z3.txt ]] ; then
-    curl -o LICENSE-z3.txt https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt
-fi
-
-# build a F* package
-if [[ -z "$FSTAR_HOME" ]] ; then
-   if ! [[ -d FStar ]] ; then
-       git clone https://github.com/FStarLang/FStar
-   fi
-   FSTAR_HOME=$(pwd)/FStar
-fi
-export FSTAR_HOME=$(fixpath "$FSTAR_HOME")
-old_FSTAR_HOME="$FSTAR_HOME"
-fstar_package_dir=$(fixpath "$FSTAR_HOME"/src/ocaml-output/fstar)
-rm -rf "$fstar_package_dir"
-Z3_LICENSE=$(pwd)/LICENSE-z3.txt $make -C "$FSTAR_HOME" package "$@"
-
-# build Karamel and add it to the package
-if [[ -z "$KRML_HOME" ]] ; then
-    if ! [[ -d karamel ]] ; then
-        git clone https://github.com/FStarLang/karamel
-    fi
-    KRML_HOME=$(pwd)/karamel
-fi
-export KRML_HOME=$(fixpath "$KRML_HOME")
-$make -C "$KRML_HOME" minimal "$@"
-OTHERFLAGS='--admit_smt_queries true' $make -C "$KRML_HOME"/krmllib verify-all "$@"
-$cp -L $KRML_HOME/krml $fstar_package_dir/bin/krml$exe
-$cp -r $KRML_HOME/krmllib $fstar_package_dir/
-$cp -r $KRML_HOME/include $fstar_package_dir/
-$cp -r $KRML_HOME/misc $fstar_package_dir/
-
-# assume current directory is $PULSE_HOME/ci
-export PULSE_HOME=$(fixpath $(cd .. && pwd))
-
-# use the package to build Pulse
-export FSTAR_HOME="$fstar_package_dir"
-$make -C "$PULSE_HOME" "$@"
-mkdir -p "$old_FSTAR_HOME"/src/.cache.boot
-if ! $is_windows ; then
-    FSTAR_HOME="$old_FSTAR_HOME" $make -C "$PULSE_HOME"/pulse2rust "$@" build
-fi
-
-# install Pulse into the package directory
-export PREFIX="$FSTAR_HOME"
-$make -C "$PULSE_HOME" install "$@"
-if ! $is_windows ; then
-    mkdir -p "$PREFIX"/pulse2rust
-    $cp "$PULSE_HOME"/pulse2rust/main.exe "$PREFIX"/pulse2rust/
-fi
-
-# create the archive package
-mv "$PREFIX" pulse
-rm -rf pulse/share/fstar pulse/INSTALL.md pulse/README.md pulse/version.txt
-$cp package-README.md pulse/README.md
-if $is_windows ; then
-  zip -r -9 pulse.zip pulse
-else
-  tar czf pulse.tar.gz pulse
-fi
diff --git a/mk/common.mk b/mk/common.mk
index 83e93a1ac..34d0d9f4d 100644
--- a/mk/common.mk
+++ b/mk/common.mk
@@ -92,7 +92,9 @@ need_exe =											\
       $(if $(shell test -x $(value $(strip $1)) && echo 1),					\
         $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
         $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
-      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+      $(if $(shell which $(value $(strip $1))),							\
+        $(eval override $(strip $1):=$(shell which $(value $(strip $1)))),			\
+        $(error $(strip $1) ("$(value $(strip $1))") does not exist and is not in PATH (cwd = $(CURDIR))))),	\
     $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)"))))			\
 
 need_file =											\
diff --git a/mk/extraction.mk b/mk/extraction.mk
index bb6b62afb..d2e4283ff 100644
--- a/mk/extraction.mk
+++ b/mk/extraction.mk
@@ -7,8 +7,7 @@ CACHE_DIR := build/$(TAG).checked
 OUTPUT_DIR := build/$(TAG).ml
 CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/src
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/stage2/fstarc.checked
+FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+ExtractPulse,+ExtractPulseC,+ExtractPulseOCaml'
 FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
 
diff --git a/mk/locate.mk b/mk/locate.mk
index 555d1ed72..0eacae5c2 100644
--- a/mk/locate.mk
+++ b/mk/locate.mk
@@ -1,18 +1,7 @@
 # common.mk must be included before this file.
 
-ifeq ($(FSTAR_HOME),)
-$(error Pulse needs an FSTAR_HOME)
-endif
-
-ifeq ($(FSTAR_EXE),)
-ifneq ($(FSTAR_HOME),)
-FSTAR_EXE := $(FSTAR_HOME)/out/bin/fstar.exe
-endif
-endif
-
-FSTAR_EXE ?= $(shell which fstar.exe)
-FSTAR_EXE := $(FSTAR_EXE)
-export FSTAR_EXE
+FSTAR_EXE ?= fstar.exe
+$(call need_exe, FSTAR_EXE)
 
 ifeq ($(KRML_EXE),)
 ifneq ($(KRML_HOME),)
@@ -22,9 +11,6 @@ KRML_EXE := krml
 endif
 endif
 
-$(call need_exe, FSTAR_EXE)
-
-export FSTAR_HOME
 export KRML_EXE
 
 PULSE_ROOT := $(abspath $(PULSE_ROOT))
diff --git a/mk/syntax_extension.mk b/mk/syntax_extension.mk
index fc4057996..dea234862 100644
--- a/mk/syntax_extension.mk
+++ b/mk/syntax_extension.mk
@@ -7,8 +7,7 @@ CACHE_DIR := build/$(TAG).checked
 OUTPUT_DIR := build/$(TAG).ml
 CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/src
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/stage2/fstarc.checked
+FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+PulseSyntaxExtension'
 FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
 
diff --git a/pulse2rust/src/Makefile b/pulse2rust/src/Makefile
index 4186a0aad..edf2fa18a 100644
--- a/pulse2rust/src/Makefile
+++ b/pulse2rust/src/Makefile
@@ -7,8 +7,7 @@ CACHE_DIR := _cache
 OUTPUT_DIR := ocaml/generated
 CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/src
-FSTAR_OPTIONS += --include $(FSTAR_HOME)/stage2/fstarc.checked
+FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+Pulse2Rust'
 FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
 
diff --git a/pulse2rust/src/Pulse2Rust.fst.config.json b/pulse2rust/src/Pulse2Rust.fst.config.json
index b2185c127..0c25a1a14 100644
--- a/pulse2rust/src/Pulse2Rust.fst.config.json
+++ b/pulse2rust/src/Pulse2Rust.fst.config.json
@@ -5,15 +5,12 @@
     "--lax",
     "--MLish",
     "--MLish_effect", "FStarC.Compiler.Effect",
-    "--cache_dir",
-    "${FSTAR_HOME}/src/.cache.boot",
+    "--with_fstarc",
     "--z3version",
     "4.13.3",
     "--ext",
     "context_pruning"
   ],
   "include_dirs": [
-    ".",
-    "${FSTAR_HOME}/src/"
   ]
 }
diff --git a/qs/common.mk b/qs/common.mk
index 49e16828c..bf4a848ff 100644
--- a/qs/common.mk
+++ b/qs/common.mk
@@ -63,7 +63,9 @@ need_exe =											\
       $(if $(shell test -x $(value $(strip $1)) && echo 1),					\
         $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
         $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
-      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+      $(if $(shell which $(value $(strip $1))),							\
+        $(eval override $(strip $1):=$(shell which $(value $(strip $1)))),			\
+        $(error $(strip $1) ("$(value $(strip $1))") does not exist and is not in PATH (cwd = $(CURDIR))))),	\
     $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)"))))			\
 
 need_file =											\
diff --git a/qs/fstar.mk b/qs/fstar.mk
index 834fea048..80fe85143 100644
--- a/qs/fstar.mk
+++ b/qs/fstar.mk
@@ -20,9 +20,8 @@ include common.mk
 .DEFAULT_GOAL := all
 
 # Set a default FSTAR_EXE for most clients.
-$(call need,FSTAR_HOME)
-FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
-FSTAR_EXE := $(abspath $(FSTAR_EXE))
+FSTAR_EXE ?= fstar.exe
+$(call need_exe,FSTAR_EXE)
 export FSTAR_EXE
 
 HINTS_ENABLED?=--use_hints
diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
index a6d311fa7..0c25a1a14 100644
--- a/src/extraction/Extraction.fst.config.json
+++ b/src/extraction/Extraction.fst.config.json
@@ -5,15 +5,12 @@
     "--lax",
     "--MLish",
     "--MLish_effect", "FStarC.Compiler.Effect",
-    "--cache_dir",
-    "${FSTAR_HOME}/src/.cache.boot",
+    "--with_fstarc",
     "--z3version",
     "4.13.3",
     "--ext",
     "context_pruning"
   ],
   "include_dirs": [
-    ".",
-    "${FSTAR_HOME}/src"
   ]
 }
diff --git a/src/syntax_extension/PulseSyntaxExtension.fst.config.json b/src/syntax_extension/PulseSyntaxExtension.fst.config.json
index a6d311fa7..0c25a1a14 100644
--- a/src/syntax_extension/PulseSyntaxExtension.fst.config.json
+++ b/src/syntax_extension/PulseSyntaxExtension.fst.config.json
@@ -5,15 +5,12 @@
     "--lax",
     "--MLish",
     "--MLish_effect", "FStarC.Compiler.Effect",
-    "--cache_dir",
-    "${FSTAR_HOME}/src/.cache.boot",
+    "--with_fstarc",
     "--z3version",
     "4.13.3",
     "--ext",
     "context_pruning"
   ],
   "include_dirs": [
-    ".",
-    "${FSTAR_HOME}/src"
   ]
 }