build-windows.yml

name: Build F* (Windows)

# Build F* on Windows
# Note: this workflow is rather messy, prints a bunch of debugging info,
# and relies on a source package generated by a previous (Linux) job.
# Debugging Windows builds is a bit of a nightmare, and can fail in many
# subtle ways. Make sure to test any change thoroughly.
#
# At some point, this should just look exactly like the Linux and macos
# workflows, just running 'make package' in a proper environment, and
# doing a full bootstrapping build.

on:
  workflow_call:
  workflow_dispatch:

defaults:
  run:
    shell:
      bash

jobs:
  # We begin from a source package (built in Linux)
  build-src:
    uses: ./.github/workflows/build-src.yml

  build:
    needs: build-src
    runs-on: windows-latest
    steps:
      - uses: cygwin/cygwin-install-action@master

      # Print out some debug info
      - name: dbg
        continue-on-error: true
        run: |
          echo 'uname -a'
          uname -a || true
          echo 'uname -s'
          uname -s || true
          echo 'uname -m'
          uname -m || true
          echo env
          env || true
          echo OS=$OS
          which make || true
          make --version || true

      - uses: ocaml/setup-ocaml@v3
        with:
          ocaml-compiler: 4.14.2

      # - 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

      - 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

      # - 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

      # - uses: actions/upload-artifact@v4
      #   with:
      #     path: FStar\fstar-Windows_NT-x86_64.tar.gz
      #     name: fstar-Windows_NT-x86_64.tar.gz

      # Get source package, extract, install its OPAM deps.
      - uses: actions/download-artifact@v4
        with:
          name: package-src
      - run: tar xzf fstar-src.tar.gz
      - run: eval $(opam env) && opam install . --deps-only
        working-directory: fstar

      # Note: we admit queries here, like the OPAM build does.
      - name: Build
        run: |
          eval $(opam env)
          make ADMIT=1 -skj$(nproc)
        working-directory: fstar

      - 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

      - name: Make binary package
        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