Merge pull request #2911 from FStarLang/guido_ci

Fix snapshot-diff detection for extraneous files

.docker/build/build_funs.sh

@@ -103,9 +103,18 @@ function fstar_default_build () {
     $gnutime make -j $threads -k ci-$localTarget && echo true >$status_file
     echo Done building FStar
 
-    # Make it a hard failure if there's a git diff. Note: FStar_Version.ml is in the
-    # .gitignore.
+    # Make it a hard failure if there's a git diff in the snapshot. First check for
+    # extraneous files, then for a diff.
     echo "Searching for a diff in ocaml/*/generated"
+    git status ocaml/*/generated # Print status for log
+
+    # If there's any output, i.e. any file not in HEAD, fail
+    if git ls-files --others --exclude-standard -- ocaml/*/generated | grep -q . ; then
+        echo " *** GIT DIFF: there are extraneous files in the snapshot"
+        echo false >$status_file
+    fi
+
+    # If there's a diff in existing files, fail
     if ! git diff --exit-code ocaml/*/generated ; then
         echo " *** GIT DIFF: the files in the list above have a git diff"
         echo false >$status_file

.docker/standalone.Dockerfile

@@ -72,8 +72,10 @@ RUN if [[ -n "$CI_TEST_MIN_OPAM_DEPS" ]] ; then \
 fi
 
 # F* dependencies
+RUN opam install --confirm-level=unsafe-yes menhir # needed to bootstrap
 RUN opam install --confirm-level=unsafe-yes --deps-only $HOME/FStar/fstar.opam
 
+
 # Configure the git user for hint refresh
 RUN git config --global user.name "Dzomo, the Everest Yak" && \
     git config --global user.email "[email protected]"

.github/workflows/linux-x64.yaml

@@ -67,7 +67,7 @@ jobs:
           echo "ci_docker_builder=$ci_docker_builder" >> $GITHUB_ENV
           docker buildx create --name $ci_docker_builder --driver-opt env.BUILDKIT_STEP_LOG_MAX_SIZE=500000000
           if [[ -z $CI_TARGET ]] ; then CI_TARGET=uregressions ; fi
-          docker buildx build --builder $ci_docker_builder --pull --load --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" $CI_DO_TEST_MIN_OPAM_DEPS $CI_DO_OCAML_VERSION $CI_DO_NO_KARAMEL .
+          docker buildx build --builder $ci_docker_builder --pull --load --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" $CI_DO_TEST_MIN_OPAM_DEPS $CI_DO_OCAML_VERSION $CI_DO_NO_KARAMEL . |& tee BUILDLOG
           ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
           if $ci_docker_status && [[ -z "$CI_SKIP_IMAGE_TAG" ]] ; then
             if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then
@@ -107,6 +107,13 @@ jobs:
           esac
           echo "CI_COMMIT=$(echo ${{ github.event.head_commit.id || github.event.pull_request.head.sha }} | grep -o '^........')" >> $GITHUB_ENV
           echo 'CI_STATUS='"$(docker run fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT /bin/bash -c 'cat $FSTAR_HOME/result.txt' || echo Failure)" >> $GITHUB_ENV
+      - name: Output build log error summary
+        if: ${{ always () }}
+        run: |
+          # Just outputs to the github snippet. Could be part of slack message.
+          # This command never triggers a failure
+          grep -C10 -Ew ' \*\*\* |\(Error' BUILDLOG || true
+
       - name: Post to the Slack channel
         if: ${{ always() && (github.event_name != 'workflow_dispatch') }}
         id: slack

Makefile

@@ -117,8 +117,7 @@ output:
 .PHONY: ci-utest-prelude
 
 ci-utest-prelude:
-	$(Q)+$(MAKE) dune FSTAR_BUILD_PROFILE=test
-	$(Q)+$(MAKE) dune-bootstrap
+	$(Q)+$(MAKE) dune-full-bootstrap FSTAR_BUILD_PROFILE=test
 	$(Q)+$(MAKE) -C src ocaml-unit-tests
 	$(Q)+$(MAKE) -C ulib ulib-in-fsharp    #build ulibfs
 

src/ocaml-output/.gitignore

@@ -26,7 +26,6 @@ FStar_ST.ml
 FStar_String.ml
 FStar_Unionfind.ml
 FStar_Util.ml
-FStar_Version.ml
 main.ml
 parse.ml
 parse.mli

src/ocaml-output/Makefile

@@ -50,7 +50,7 @@ else
 endif
 
 .PHONY: generated-files
-generated-files: $(FStar_Parser_Parse_ml) $(FStar_Version_ml)
+generated-files: $(FStar_Parser_Parse_ml)
 
 .PHONY: dune-stdlib-snapshot dune-snapshot dune-fstar-snapshot dune-verify-ulib source-files
 
@@ -204,7 +204,7 @@ endif
 # snapshot.
 clean:
 	$(call msg, "CLEAN", "src/ocaml-output")
-	$(Q)rm -f $(FStar_Version_ml) parse.mly
+	$(Q)rm -f parse.mly
 	$(Q)rm -f *.tar.gz *.zip
 	$(Q)rm -f version_platform.txt
 	$(Q)rm -f yac-log