Merge pull request #3404 from mtzguido/ci

actions/docker: reworking ci to just run `make ci-post`
FStarLang · Aug 25, 2024 · 2d656d0 · 2d656d0
2 parents 2895ff4 + d443d13
commit 2d656d0
Show file tree

Hide file tree

Showing 7 changed files with 13 additions and 38 deletions.
diff --git a/.docker/build/build-standalone.sh b/.docker/build/build-standalone.sh
@@ -4,9 +4,8 @@ set -x
 
 set -e # abort on errors
 
-target=$1
-threads=$2
-branchname=$3
+threads=$1
+branchname=$2
 
 build_home="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 . "$build_home"/build_funs.sh
@@ -15,7 +14,7 @@ rootPath=$(pwd)
 result_file="result.txt"
 status_file="status.txt"
 ORANGE_FILE="orange_file.txt"
-build_fstar $target
+build_fstar ci
 
 # If RESOURCEMONITOR is defined, then make an rmon/ directory with
 # resource usage information

diff --git a/.docker/build/build_funs.sh b/.docker/build/build_funs.sh
@@ -43,16 +43,7 @@ function fetch_karamel() {
 }
 
 function make_karamel_pre() {
-    # Default build target is minimal, unless specified otherwise
-    local localTarget
-    if [[ $1 == "" ]]; then
-        localTarget="minimal"
-    else
-        localTarget="$1"
-    fi
-
-    make -C karamel -j $threads $localTarget ||
-        (cd karamel && git clean -fdx && make -j $threads $localTarget)
+    make -C karamel -j $threads minimal
 }
 
 function fstar_docs_build () {
@@ -64,9 +55,7 @@ function fstar_docs_build () {
 }
 
 function fstar_default_build () {
-    localTarget=$1
-
-    if [[ $localTarget == "uregressions-ulong" ]]; then
+    if [[ -n "$CI_RECORD_HINTS" ]]; then
         export OTHERFLAGS="--record_hints $OTHERFLAGS"
     fi
 
@@ -95,7 +84,7 @@ function fstar_default_build () {
 
     # Once F* is built, run its main regression suite. This also runs the karamel
     # test (unless CI_NO_KARAMEL is set).
-    $gnutime make -j $threads -k ci-$localTarget && echo true >$status_file
+    $gnutime make -j $threads -k ci-post && echo true >$status_file
     echo Done building FStar
 
     if [ -z "${FSTAR_CI_NO_GITDIFF}" ]; then
@@ -143,8 +132,8 @@ function build_fstar() {
 
     if [[ $localTarget == "fstar-docs" ]]; then
         fstar_docs_build
-    else
-        fstar_default_build $target
+    elif [[ $localTarget == "ci" ]]; then
+        fstar_default_build
     fi
 
     if [[ $(cat $status_file) != "true" ]]; then

diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile
@@ -14,13 +14,12 @@ WORKDIR $HOME/FStar
 RUN opam install --confirm-level=unsafe-yes --deps-only ./fstar.opam && opam clean
 
 # Run CI proper
-ARG CI_TARGET=uregressions
 ARG CI_THREADS=24
 ARG CI_BRANCH=master
 ARG CI_NO_KARAMEL=
 ARG RESOURCEMONITOR=
 ARG FSTAR_CI_NO_GITDIFF=
-RUN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_TARGET $CI_THREADS $CI_BRANCH
+RUN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH
 
 WORKDIR $HOME
 ENV FSTAR_HOME $HOME/FStar
diff --git a/.github/workflows/linux-x64-rebuild-base.yaml b/.github/workflows/linux-x64-rebuild-base.yaml
@@ -41,8 +41,7 @@ jobs:
           ci_docker_image_tag=fstar:update-base-test-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
           echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
 
-          CI_TARGET=uregressions
-          docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg CI_THREADS=$(nproc) . |& tee BUILDLOG
+          docker build --no-cache -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg FSTAR_CI_BASE=$TEMP_IMAGE_NAME --build-arg CI_THREADS=$(nproc) . |& tee BUILDLOG
           ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
           $ci_docker_status
 

diff --git a/.github/workflows/linux-x64.yaml b/.github/workflows/linux-x64.yaml
@@ -42,7 +42,7 @@ jobs:
         if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_refresh_hints }}
         run: |
           # NOTE: this causes the build to record hints
-          echo "CI_TARGET=uregressions-ulong" >> $GITHUB_ENV
+          echo "CI_RECORD_HINTS_ARG=--build-arg CI_RECORD_HINTS=1" >> $GITHUB_ENV
       - name: Populate no karamel arg
         if: ${{ (github.event_name == 'workflow_dispatch') && inputs.ci_no_karamel }}
         run: |
@@ -71,8 +71,7 @@ jobs:
         run: |
           ci_docker_image_tag=fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
           echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
-          if [[ -z $CI_TARGET ]] ; then CI_TARGET=uregressions ; fi
-          docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg CI_TARGET="$CI_TARGET" --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_DO_NO_KARAMEL . |& tee BUILDLOG
+          docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_RECORD_HINTS_ARG $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

diff --git a/Makefile b/Makefile
@@ -125,7 +125,7 @@ clean-intermediate:
 .PHONY: hints
 hints:
 	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) -C ulib/
-	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) ci-uregressions
+	+$(Q)OTHERFLAGS="${OTHERFLAGS} --record_hints" $(MAKE) ci-uregressions ci-ulib-extra
 
 .PHONY: bench
 bench:
@@ -209,10 +209,6 @@ ci-post:						\
 ci-uregressions:
 	+$(Q)$(MAKE) -C src uregressions
 
-.PHONY: ci-uregressions-ulong
-ci-uregressions-ulong:
-	+$(Q)$(MAKE) -C src uregressions-ulong
-
 .PHONY: ci-karamel-test
 ci-karamel-test: ci-krmllib
 	+$(Q)$(MAKE) -C examples krml_tests

diff --git a/src/Makefile b/src/Makefile
@@ -48,12 +48,6 @@ ulib-in-fsharp:
 .PHONY: uregressions
 uregressions: tutorial utests uexamples
 
-# This is a hook for nightly builds (on Linux)
-# But, at the moment, it tests the same files as get tested on every push
-# We may add more nightly tests here in the future
-.PHONY: uregressions-ulong
-uregressions-ulong: uregressions
-
 .PHONY: tutorial
 tutorial: book-code tutorial-old