Makefiles: no FSTAR_HOME, use --with_fstarc

.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

.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

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.

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.