Merge branch 'taramana_pulse_ci' of github.com:project-everest/everpa…

…rse into taramana_cbor

.docker/build/install-deps.sh

@@ -37,6 +37,7 @@ if ! $skip_z3 ; then
     export PATH="$FSTAR_HOME/z3-versions:$PATH"
 fi
 $skip_build || OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME"
+$skip_build || OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME" bootstrap
 
 # Install other EverParse deps
 "$build_home"/install-other-deps.sh "${args[@]}"

.docker/build/install-other-deps.sh

@@ -31,8 +31,9 @@ $skip_build || OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$KRML_HOME"
 PULSE_BRANCH=$(jq -c -r '.RepoVersions.pulse_version' "$build_home"/config.json | sed 's!^origin/!!')
 
 # Install Pulse and its dependencies
-[[ -n "$PULSE_HOME" ]]
-git clone --branch $PULSE_BRANCH https://github.com/FStarLang/pulse "$PULSE_HOME"
-$skip_build || OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$PULSE_HOME"
+# NOTE: $PULSE_HOME should now be $PULSE_REPO/out, cf. FStarLang/pulse#246
+[[ -n "$PULSE_REPO" ]]
+git clone --branch $PULSE_BRANCH https://github.com/FStarLang/pulse "$PULSE_REPO"
+$skip_build || OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$PULSE_REPO"
 
 opam install hex re ctypes sha sexplib

.docker/hierarchic.Dockerfile

@@ -10,8 +10,10 @@ WORKDIR $HOME/everparse
 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
 
 # Dependencies (opam packages)
+# NOTE: $PULSE_HOME is now $PULSE_REPO/out, cf. FStarLang/pulse#246
 ENV KRML_HOME=$HOME/everparse/karamel
-ENV PULSE_HOME=$HOME/everparse/pulse
+ENV PULSE_REPO=$HOME/everparse/pulse
+ENV PULSE_HOME=$PULSE_REPO/out
 RUN sudo apt-get update && eval $(opam env) && .docker/build/install-other-deps.sh
 
 # CI dependencies: sphinx (for the docs)

.docker/produce-binary.Dockerfile

@@ -15,9 +15,11 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
     && true
 
 # Dependencies (F*, Karamel and opam packages)
+# NOTE: $PULSE_HOME is now $PULSE_REPO/out, cf. FStarLang/pulse#246
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
-ENV PULSE_HOME=$HOME/pulse
+ENV PULSE_REPO=$HOME/pulse
+ENV PULSE_HOME=$PULSE_REPO/out
 RUN eval $(opam env) && .docker/build/install-deps.sh --skip-build --skip-z3
 
 # CI proper

.docker/standalone.Dockerfile

@@ -17,9 +17,11 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
 
 # Dependencies (F*, Karamel and opam packages)
+# NOTE: $PULSE_HOME is now $PULSE_REPO/out, cf. FStarLang/pulse#246
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
-ENV PULSE_HOME=$HOME/pulse
+ENV PULSE_REPO=$HOME/pulse
+ENV PULSE_HOME=$PULSE_REPO/out
 RUN eval $(opam env) && .docker/build/install-deps.sh
 
 # CI dependencies: sphinx (for the docs)

src/pulse.Makefile

@@ -8,7 +8,8 @@ ifeq (,$(PULSE_LIB))
     ifeq (,$(PULSE_LIB))
 #      $(error "Pulse should be installed and its lib/ subdirectory should be in ocamlpath; or PULSE_HOME should be defined in the enclosing Makefile as the prefix directory where Pulse was installed, or the root directory of its source repository")
       # assuming Everest layout
-      PULSE_LIB := $(realpath $(EVERPARSE_SRC_PATH)/../../pulse/lib/pulse)
+      # NOTE: $PULSE_HOME is now $PULSE_REPO/out, cf. FStarLang/pulse#246
+      PULSE_LIB := $(realpath $(EVERPARSE_SRC_PATH)/../../pulse/out/lib/pulse)
     endif
     PULSE_HOME := $(realpath $(PULSE_LIB)/../..)
   else