Updating CI, removing old F* bootstrap step

FStarLang · Oct 24, 2024 · 48ba8d6 · 48ba8d6
1 parent f3bf15d
commit 48ba8d6
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 22 deletions.
diff --git a/src/ci/ci.Dockerfile b/src/ci/ci.Dockerfile
@@ -32,19 +32,9 @@ RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
     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
-
 # Steel CI proper
 ARG STEEL_NIGHTLY_CI
 ARG OTHERFLAGS=--use_hints
-RUN eval $(opam env) && . $HOME/.cargo/env && env STEEL_NIGHTLY_CI="$STEEL_NIGHTLY_CI" make -k -j $opamthreads -C steel/src ci
+RUN eval $(opam env) && . $HOME/.cargo/env && env STEEL_NIGHTLY_CI="$STEEL_NIGHTLY_CI" make -k -j $opamthreads -C steel ci
 
 ENV STEEL_HOME $HOME/steel
diff --git a/src/ci/hierarchic.Dockerfile b/src/ci/hierarchic.Dockerfile
@@ -24,6 +24,6 @@ RUN mkdir -p $HOME/steel_tools && \
 # Steel CI proper
 ARG STEEL_NIGHTLY_CI
 ARG OTHERFLAGS=--use_hints
-RUN eval $(opam env) && env STEEL_NIGHTLY_CI="$STEEL_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/steel/src ci
+RUN eval $(opam env) && env STEEL_NIGHTLY_CI="$STEEL_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/steel ci
 
 ENV STEEL_HOME $HOME/steel
diff --git a/src/ci/package.Dockerfile b/src/ci/package.Dockerfile
@@ -46,16 +46,6 @@ RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
     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 && steel/src/ci/package.sh -j $opamthreads