Building a Windows package

.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

.github/workflows/build-linux.yml

@@ -48,14 +48,15 @@ jobs:
           ARCH=$(uname -m)
           export FSTAR_TAG=-$KERNEL-$ARCH
           make -skj$(nproc) package
-          make -skj$(nproc) package-src FSTAR_TAG=
-          # ^ no tag in source package
+          # Currently creating the source package in a separate job
+          # make -skj$(nproc) package-src FSTAR_TAG=
+          # # ^ no tag in source package
 
       - uses: actions/upload-artifact@v4
         with:
           path: fstar-Linux-*
           name: package-linux
-      - uses: actions/upload-artifact@v4
-        with:
-          path: fstar-src.tar.gz
-          name: package-src
+      # - uses: actions/upload-artifact@v4
+      #   with:
+      #     path: fstar-src.tar.gz
+      #     name: package-src

.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

.github/workflows/build-windows.yml

@@ -0,0 +1,134 @@
+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 being from a source package (built in Linux)
+  build-src:
+    uses: ./.github/workflows/build-src.yml
+
+  build-windows:
+    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

.scripts/make_fstar_version.sh

@@ -22,13 +22,17 @@ COMPILER="OCaml $(ocamlc -version)"
 # If a system does not have git, or we are not in a git repo, fallback with "unset"
 if [[ -z "$FSTAR_COMMIT" ]] ; then
    FSTAR_COMMIT=$(git describe --match="" --always --abbrev=40 --dirty 2>/dev/null || echo unset)
+   # NB: ^ has to be in-sync with src-install.sh
+fi
+if [[ -z "$FSTAR_COMMITDATE" ]] ; then
+   FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
+   # NB: ^ has to be in-sync with src-install.sh
 fi
-COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
 
 echo "let dummy () = ();;"
 echo "FStarC_Options._version := \"$FSTAR_VERSION\";;"
 echo "FStarC_Options._platform := \"$PLATFORM\";;"
 echo "FStarC_Options._compiler := \"$COMPILER\";;"
 # We deliberately use commitdate instead of date, so that rebuilds are no-ops
-echo "FStarC_Options._date := \"$COMMITDATE\";;"
+echo "FStarC_Options._date := \"$FSTAR_COMMITDATE\";;"
 echo "FStarC_Options._commit:= \"$FSTAR_COMMIT\";;"

.scripts/src-install.sh

@@ -41,7 +41,6 @@ cp version.txt "${PREFIX}"
 cp -H -r src "${PREFIX}/src"
 cp .scripts/get_fstar_z3.sh "${PREFIX}/get_fstar_z3.sh"
 cp fstar.opam "${PREFIX}/fstar.opam"
-cp mk/src_package_mk.mk "${PREFIX}/Makefile"
 mkdir "${PREFIX}/mk"
 cp mk/lib.mk "${PREFIX}/mk/lib.mk"
 cp mk/common.mk "${PREFIX}/mk/common.mk"
@@ -54,6 +53,16 @@ cp .scripts/mk-package.sh   "${PREFIX}/.scripts"
 cp .scripts/get_fstar_z3.sh "${PREFIX}/.scripts"
 cp .scripts/package_z3.sh   "${PREFIX}/.scripts"
 
+cp mk/src_package_mk.mk "${PREFIX}/Makefile"
+
+# Make sure the source package has a proper version.
+FSTAR_COMMIT=$(git describe --match="" --always --abbrev=40 --dirty 2>/dev/null || echo unset)
+FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
+# NB: ^ has to be in-sync with make_fstar_version.sh
+echo "## LINES BELOW ADDED BY src-install.sh" >> "${PREFIX}/Makefile"
+echo "export FSTAR_COMMITDATE=$FSTAR_COMMITDATE" >> "${PREFIX}/Makefile"
+echo "export FSTAR_COMMIT=$FSTAR_COMMIT" >> "${PREFIX}/Makefile"
+
 # Remove extra ML files, rsync has resolved the links
 # into the corresponding files already, and these would be
 # duplicates.