From a2efae1b2d75f3bfc44b2c8a753b1d414a440f45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 15 Jan 2025 10:41:27 -0800 Subject: [PATCH] Restoring self-hosted windows build --- .../workflows/build-windows-selfhosted.yml | 91 +++++++++++++++++++ .github/workflows/ci.yml | 2 + mk/src_package_mk.mk | 14 +-- mk/stage0.mk | 1 - 4 files changed, 101 insertions(+), 7 deletions(-) create mode 100644 .github/workflows/build-windows-selfhosted.yml diff --git a/.github/workflows/build-windows-selfhosted.yml b/.github/workflows/build-windows-selfhosted.yml new file mode 100644 index 00000000000..322fca898c8 --- /dev/null +++ b/.github/workflows/build-windows-selfhosted.yml @@ -0,0 +1,91 @@ +name: Build F* (Windows, self-hosted) + +on: + workflow_call: + workflow_dispatch: + push: + +jobs: + # We begin from a source package (built in Linux) + build-src: + uses: ./.github/workflows/build-src.yml + + build-windows: + needs: build-src + runs-on: [self-hosted, Windows, X64, opam-2-3] + # NOTE: no setup, the self-hosted runner already has all that is needed. + # This workflow also has many weird restrictions like + # having to set cygwin bash, cd into $GITHUB_WORKSPACE, and keep + # shell commands to a single line. + steps: + - name: clean + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: cd $GITHUB_WORKSPACE && ls -lR && rm -vrf fstar && echo "There is a CR at the end of this line" + # ^ remove the directory where the package extracts to and builds, + # all files from previous runs remain the runner's working directory + # otherwise. + + - uses: actions/download-artifact@v4 + with: + name: package-src + - run: cd $GITHUB_WORKSPACE && tar xzf fstar-src.tar.gz + shell: C:\cygwin64\bin\bash.exe --login '{0}' + + - name: Set version + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: | + # Setting FSTAR_VERSION for nightly and release builds. If unset, + # we use $(version.txt)~dev. Setting it avoids the ~dev. + cd $GITHUB_WORKSPACE && if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV; elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then echo FSTAR_VERSION="$(cat fstar/version.txt)" >> $GITHUB_ENV; echo FSTAR_RELEASE=1 >> $GITHUB_ENV; fi && echo "There is a CR at the end of this line" + + - name: Prepare environment + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: | + echo "CC=x86_64-w64-mingw32-gcc.exe" >> $GITHUB_ENV + echo "FSTAR_DUNE_OPTIONS=-j1" >> $GITHUB_ENV + echo "DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled" >> $GITHUB_ENV + # ^ Related issues: + # https://github.com/ocaml/dune/issues/2324 + # https://github.com/ocaml/dune/issues/10076 + + - name: Build a package + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: | + cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && make clean && make -j$(nproc) package V=1 ADMIT=1 && mv fstar.zip fstar-Windows_NT-x86_64.zip && echo "There is a CR at the end of this line" + # paranoid make clean above, seeing a bunch of these non predictably: + # File "libapp/dune", line 18, characters 13-56: + # 18 | (preprocess (pps ppx_deriving.show ppx_deriving_yojson)) + # ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + # Error: failed to delete sandbox in + # _build/.sandbox/e99d5dd0c933464aff5f4e9946b620a8) + + # - name: Test the package + # shell: C:\cygwin64\bin\bash.exe --login '{0}' + # run: | + # cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && export CC=x86_64-w64-mingw32-gcc.exe && export CI_THREADS=$(nproc) && .scripts/test_package.sh && echo "There is a CR at the end of this line" + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + path: fstar/fstar*.zip + name: package-win + + binary-smoke: + needs: build-windows + # This is a cloud job. + runs-on: windows-latest + steps: + - name: Get package + uses: actions/download-artifact@v4 + with: + name: package-win + + - run: unzip fstar*.zip + shell: bash + + - name: Smoke test + working-directory: fstar + run: | + ./bin/fstar.exe lib/fstar/ulib/Prims.fst -f -d + echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst + ./bin/fstar.exe A.fst -d diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e51bb02926a..53992ea86d0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,6 +2,8 @@ name: CI on: push: + branches-ignore: + - _** pull_request: workflow_dispatch: merge_group: diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index 480a857c9da..e3e3b7cabc3 100644 --- a/mk/src_package_mk.mk +++ b/mk/src_package_mk.mk @@ -22,12 +22,14 @@ # (version 4.4.1-1 at least) to (sometimes) freeze , and halt the build. # Not running this makefile (and sub-makes) in parallel *seems* to help, # though obviously makes this significantly slower in Windows. -ifeq ($(OS),Windows_NT) -.NOTPARALLEL: -MAYBEJ1=-j1 -else -MAYBEJ1= -endif +# LATER EDIT: For the self-hosted runner, this does not seem to be a problem, +# so do not restrict parallelism. +# ifeq ($(OS),Windows_NT) +# .NOTPARALLEL: +# MAYBEJ1=-j1 +# else +# MAYBEJ1= +# endif include mk/common.mk diff --git a/mk/stage0.mk b/mk/stage0.mk index ea9e676f35f..ba2786f5ab2 100644 --- a/mk/stage0.mk +++ b/mk/stage0.mk @@ -1,4 +1,3 @@ -# This file is used (or created) by the bring-stage0 rule in the toplevel Makefile include $(FSTAR_ROOT)/mk/common.mk