diff --git a/.github/workflows/build-all.yml b/.github/workflows/build-all.yml index 09d68a3c41f..24dc9f8f063 100644 --- a/.github/workflows/build-all.yml +++ b/.github/workflows/build-all.yml @@ -12,3 +12,6 @@ jobs: build-macos: uses: ./.github/workflows/build-macos.yml + + build-windows: + uses: ./.github/workflows/build-windows.yml diff --git a/.github/workflows/build-src.yml b/.github/workflows/build-src.yml new file mode 100644 index 00000000000..8a4a4ca6b7d --- /dev/null +++ b/.github/workflows/build-src.yml @@ -0,0 +1,67 @@ +name: Build F* (src) + +on: + workflow_call: + workflow_dispatch: + +defaults: + run: + shell: bash + +jobs: + build-linux: + runs-on: ubuntu-22.04 + # We prefer slightly older Ubuntu so we get binaries that work on + # all more recent versions. + steps: + - uses: actions/checkout@master + id: checkout + + - name: Check cache + id: check-cache + uses: actions/cache/restore@v4 + with: + path: fstar-src.tar.gz + key: FStar-src-${{steps.checkout.outputs.commit}} + + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: 4.14.2 + + - name: Prepare + run: | + ./.scripts/get_fstar_z3.sh $HOME/bin + echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV + opam install --deps-only ./fstar.opam + + - name: Set version + run: | + # Setting FSTAR_VERSION for nightly and release builds. If unset, + # we use $(version.txt)~dev. Setting it avoids the ~dev. + 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 version.txt)" >> $GITHUB_ENV + echo FSTAR_RELEASE=1 >> $GITHUB_ENV + fi + + # NB: release workflow later adds version number to the name + - name: Build package + if: steps.check-cache.outputs.cache-hit != 'true' + run: | + eval $(opam env) + export FSTAR_TAG= + # ^ no tag in source package + make -skj$(nproc) package-src ADMIT=1 + + - name: Save + if: steps.check-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: fstar-src.tar.gz + key: FStar-src-${{steps.checkout.outputs.commit}} + + - uses: actions/upload-artifact@v4 + with: + path: fstar-src.tar.gz + name: package-src diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml new file mode 100644 index 00000000000..6aea607d28f --- /dev/null +++ b/.github/workflows/build-windows.yml @@ -0,0 +1,148 @@ +name: Build F* (Windows) + +# Build F* on Windows + +on: + workflow_call: + push: + schedule: + - cron: '*/5 * * * *' + +defaults: + run: + shell: + bash + +jobs: + build-src: + uses: ./.github/workflows/build-src.yml + + build-windows: + needs: build-src + runs-on: windows-latest + steps: + - run: echo "CYGWIN=" >>$GITHUB_ENV + - uses: cygwin/cygwin-install-action@master + - run: echo "CYGWIN=" >>$GITHUB_ENV + + - uses: actions/download-artifact@v4 + with: + name: package-src + + # Print out some debug info + - name: dbg + continue-on-error: true + run: | + echo 'uname -a' + uname -a + echo 'uname -s' + uname -s + echo 'uname -m' + uname -m + echo env + env + echo OS=$OS + which make + make --version + - run: echo "CYGWIN=" >>$GITHUB_ENV + + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: 4.14.2 + + # - run: echo "CYGWIN=" >>$GITHUB_ENV + # - name: Prepare + # shell: powershell # somehow in bash we fail to build ocamlfind? + # run: | + # ./FStar/.scripts/get_fstar_z3.sh $HOME/bin + # echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV + # opam install --deps-only FStar\fstar.opam + # - run: echo "CYGWIN=" >>$GITHUB_ENV + + # - name: Set version + # run: | + # # Setting FSTAR_VERSION for nightly and release builds. If unset, + # # we use $(version.txt)~dev. Setting it avoids the ~dev. + # 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 + # fi + + # - run: echo "CYGWIN=" >>$GITHUB_ENV + # - name: Build packages + # working-directory: FStar + # run: | + # eval $(opam env) + # KERNEL=Windows_NT + # # $(uname -s) + # # ^ uname-s prints something like CYGWIN_NT-10.0-26100 or MINGW64_NT-10.0-20348 + # ARCH=$(uname -m) + # export FSTAR_TAG=-$KERNEL-$ARCH + # make -kj$(nproc) 0 V=1 + # echo ------------------------------------------------- + # ./stage0/bin/fstar.exe --version + # ./stage0/bin/fstar.exe --locate + # ./stage0/bin/fstar.exe --locate_lib + # ./stage0/bin/fstar.exe --locate_ocaml + # ./stage0/bin/fstar.exe --include src --debug yes || true + # echo ------------------------------------------------- + # make -kj$(nproc) package V=1 + + - run: echo "CYGWIN=" >>$GITHUB_ENV + # - uses: actions/upload-artifact@v4 + # with: + # path: FStar\fstar-Windows_NT-x86_64.tar.gz + # name: fstar-Windows_NT-x86_64.tar.gz + + - run: tar xzf fstar-src.tar.gz + - run: opam install . --deps-only --with-test + working-directory: fstar + - run: echo "CYGWIN=" >>$GITHUB_ENV + + - name: test mk-package quick + run: | + .scripts/mk-package.sh ulib/ lib + working-directory: fstar + - uses: actions/upload-artifact@v4 + if: ${{ always () }} + with: + name: lib-package-test + path: fstar/lib.zip + + # Note: we admit queries here, like the OPAM build does. + - run: eval $(opam env) && make V=1 -kj$(nproc) ADMIT=1 + working-directory: fstar + - run: echo "CYGWIN=" >>$GITHUB_ENV + + - name: install z3? + run: | + mkdir -p bin + ./fstar/get_fstar_z3.sh bin + echo "$(realpath bin)" >>$GITHUB_PATH + + - name: Smoke test + continue-on-error: true + run: | + ./out/bin/fstar.exe out/lib/fstar/ulib/Prims.fst -f + echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst + ./out/bin/fstar.exe A.fst + working-directory: fstar + + - run: | + eval $(opam env) + KERNEL=Windows_NT + # $(uname -s) + # ^ uname-s prints something like CYGWIN_NT-10.0-26100 or MINGW64_NT-10.0-20348 + ARCH=$(uname -m) + export FSTAR_TAG=-$KERNEL-$ARCH + make package + working-directory: fstar + + - run: find . -name '*.zip' + + - uses: actions/upload-artifact@v4 + if: ${{ always () }} + with: + name: package-win + path: fstar/fstar-*.zip diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml deleted file mode 100644 index 959d1521602..00000000000 --- a/.github/workflows/windows.yml +++ /dev/null @@ -1,28 +0,0 @@ -name: FStar Windows Package - -on: - workflow_dispatch: - -jobs: - - build-windows: - - runs-on: [self-hosted, Windows, X64, opam-2-3] - - steps: - - name: Check out repo - uses: actions/checkout@v4 - - - name: Build a package - shell: C:\cygwin64\bin\bash.exe --login '{0}' - run: | - eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe make -C $GITHUB_WORKSPACE -j package && echo "There is a CR at the end of this line" - - name: Test the package - shell: C:\cygwin64\bin\bash.exe --login '{0}' - run: | - eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe CI_THREADS=24 $GITHUB_WORKSPACE/.scripts/test_package.sh && echo "There is a CR at the end of this line" - - name: Upload artifact - uses: actions/upload-artifact@v4 - with: - name: fstar-Windows_x86_64.zip - path: src\ocaml-output\fstar.zip