windows workflow test

.github/workflows/build-all.yml

@@ -2,7 +2,8 @@ name: Build F* binaries (all archs)
 
 on:
   workflow_call:
-  workflow_dispatch:
+  # workflow_dispatch:
+  push:
 
 jobs:
   build-linux:
@@ -12,3 +13,7 @@ jobs:
 
   build-macos:
     uses: ./.github/workflows/build-macos.yml
+
+  build-windows:
+    needs: build-linux # uses source package artifact
+    uses: ./.github/workflows/build-windows.yml

.github/workflows/build-linux.yml

@@ -12,7 +12,7 @@ defaults:
     shell: bash
 
 jobs:
-  build:
+  build-linux:
     runs-on: ubuntu-22.04
     # We prefer slightly older Ubuntu so we get binaries that work on
     # all more recent versions.
@@ -37,7 +37,6 @@ jobs:
             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
@@ -46,14 +45,16 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
-          make -skj$(nproc) package     FSTAR_TAG=-$KERNEL-$ARCH
-          make -skj$(nproc) package-src FSTAR_TAG=
-
-      - uses: actions/upload-artifact@v4
-        with:
-          path: fstar-Linux-*
-          name: package-linux
+          export FSTAR_TAG=-$KERNEL-$ARCH
+          # make -skj$(nproc) package
+          make -skj$(nproc) package-src-1 FSTAR_TAG= ADMIT=1
+          # ^ No binaries here, skip the tag
+
+      # - uses: actions/upload-artifact@v4
+      #   with:
+      #     path: fstar-Linux-*
+      #     name: package-linux
       - uses: actions/upload-artifact@v4
         with:
-          path: fstar-src.tar.gz
+          path: fstar-stage1-src.tar.gz
           name: package-src

.github/workflows/build-macos.yml

@@ -5,7 +5,7 @@ on:
   workflow_call:
 
 jobs:
-  build:
+  build-macos:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@master
@@ -29,7 +29,6 @@ jobs:
             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
 
       # Note *g*make below!
@@ -39,6 +38,7 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
+          export FSTAR_TAG=-$KERNEL-$ARCH
           gmake -skj$(nproc) package FSTAR_TAG=-$KERNEL-$ARCH
 
       - uses: actions/upload-artifact@v4

.github/workflows/build-windows.yml

@@ -0,0 +1,132 @@
+name: Build F* (Windows)
+
+# Build F* on Windows
+
+on:
+  workflow_call:
+  push:
+
+defaults:
+  run:
+    shell:
+      bash
+
+jobs:
+  build-windows:
+    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-stage1-src.tar.gz
+      - run: opam install . --deps-only --with-test
+        working-directory: fstar
+      - run: echo "CYGWIN=" >>$GITHUB_ENV
+      # 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

.github/workflows/ci.yml

@@ -1,7 +1,6 @@
 name: CI
 
 on:
-  push:
   pull_request:
   workflow_dispatch:
   merge_group:

.github/workflows/nightly.yml

@@ -11,7 +11,7 @@ name: F* nightly build
 
 on:
   schedule:
-    - cron: '0 0 * * *'
+    - cron: '*/10 * * * *'
   workflow_dispatch:
 
 jobs:
@@ -45,7 +45,7 @@ jobs:
 
           # We push nightly builds to a different repo (same org)
           REPO="${{github.repository}}-nightly"
-          TAG=nightly-$(date -I)
+          TAG=nightly-$(date -I)-$((RANDOM))
 
           # Create tag
           git tag $TAG ${{github.sha}}