Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

actions/docker: reworking ci to just run make ci-post #3404

Merged
merged 1 commit into from
Aug 25, 2024
Merged

actions/docker: reworking ci to just run make ci-post #3404

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions .docker/build/build-standalone.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
21 changes: 5 additions & 16 deletions .docker/build/build_funs.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 () {
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions .docker/standalone.Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 1 addition & 2 deletions .github/workflows/linux-x64-rebuild-base.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
5 changes: 2 additions & 3 deletions .github/workflows/linux-x64.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: |
Expand Down Expand Up @@ -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
Expand Down
6 changes: 1 addition & 5 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
6 changes: 0 additions & 6 deletions src/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading