Windows build (with self-hosted runner)

.github/workflows/build-all.yml

@@ -5,15 +5,15 @@ on:
   workflow_dispatch:
 
 jobs:
-  # Disable when Windows is reenabled.
-  build-src:
-    uses: ./.github/workflows/build-src.yml
+  # Windows build call this as a substep
+  # src:
+  #   uses: ./.github/workflows/build-src.yml
 
-  build-linux:
+  linux:
     uses: ./.github/workflows/build-linux.yml
 
-  build-macos:
+  macos:
     uses: ./.github/workflows/build-macos.yml
 
-  # build-windows:
-  #   uses: ./.github/workflows/build-windows.yml
+  windows:
+    uses: ./.github/workflows/build-windows-selfhosted.yml

.github/workflows/build-linux.yml

@@ -12,7 +12,7 @@ defaults:
     shell: bash
 
 jobs:
-  build-linux:
+  build:
     runs-on: ubuntu-22.04
     # We prefer slightly older Ubuntu so we get binaries that work on
     # all more recent versions.

.github/workflows/build-macos.yml

@@ -5,7 +5,7 @@ on:
   workflow_call:
 
 jobs:
-  build-macos:
+  build:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@master

.github/workflows/build-src.yml

@@ -9,7 +9,7 @@ defaults:
     shell: bash
 
 jobs:
-  build-linux:
+  build:
     runs-on: ubuntu-22.04
     # We prefer slightly older Ubuntu so we get binaries that work on
     # all more recent versions.

.github/workflows/build-windows-selfhosted.yml

@@ -0,0 +1,74 @@
+name: Build F* (Windows, self-hosted)
+
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  # We begin from a source package (built in Linux)
+  build-src:
+    uses: ./.github/workflows/build-src.yml
+
+  build:
+    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: test
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: echo "GITHUB_WORKSPACE=$GITHUB_WORKSPACE"
+
+      - name: clean
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: cd $GITHUB_WORKSPACE/ && rm -rf * && echo "There is a CR at the end of this line"
+        # ^ clean the workspace
+
+      - 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}'
+
+      # DO NOT DO THIS. These variables will be lost since bash will
+      # not look at the environment of the calling cmd shell.
+      # - 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 && CC=x86_64-w64-mingw32-gcc.exe DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled 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"
+
+      - name: Upload artifact
+        uses: actions/upload-artifact@v4
+        with:
+          path: fstar/fstar*.zip
+          name: package-win
+
+  binary-smoke:
+    needs: build
+    # 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

.github/workflows/build-windows.yml

@@ -20,11 +20,11 @@ defaults:
       bash
 
 jobs:
-  # We being from a source package (built in Linux)
+  # We begin from a source package (built in Linux)
   build-src:
     uses: ./.github/workflows/build-src.yml
 
-  build-windows:
+  build:
     needs: build-src
     runs-on: windows-latest
     steps:

.github/workflows/ci.yml

@@ -2,6 +2,8 @@ name: CI
 
 on:
   push:
+    branches-ignore:
+    - _**
   pull_request:
   workflow_dispatch:
   merge_group:

.scripts/package_z3.sh

@@ -19,10 +19,14 @@ inst1 () {
 	cp "$1" "$TGT"
 }
 
-inst1 ./z3-4.8.5/bin/z3
-inst1 ./z3-4.8.5/LICENSE.txt
-inst1 ./z3-4.13.3/bin/z3
-inst1 ./z3-4.13.3/LICENSE.txt
+for dir in z3-4.8.5 z3-4.13.3; do
+  inst1 ./$dir/bin/z3
+  inst1 ./$dir/LICENSE.txt
+  for dll in ./$dir/bin/*dll; do
+    # Needed for Windows packages.
+    inst1 "$dll"
+  done
+done
 
 popd > /dev/null
 

.scripts/src-install.sh

@@ -62,6 +62,9 @@ FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
 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"
+if [[ -n "${FSTAR_VERSION:-}" ]]; then
+  echo "export FSTAR_VERSION=$FSTAR_VERSION" >> "${PREFIX}/Makefile"
+fi
 
 # Remove extra ML files, rsync has resolved the links
 # into the corresponding files already, and these would be

mk/src_package_mk.mk

@@ -18,17 +18,6 @@
 #
 # I think this is probably a dune bug.
 
-# NOTE: (Guido 2025-01-13) For whatever undebuggable reason, Cygwin make
-# (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
-
 include mk/common.mk
 
 FSTAR_DUNE_OPTIONS += --no-print-directory
@@ -67,7 +56,7 @@ check_lib: install_bin
 	  CODEGEN=none \
 	  OUTPUT_DIR=none \
 	  FSTAR_ROOT=$(CURDIR) \
-	  $(MAKE) -f mk/lib.mk verify $(MAYBEJ1)
+	  $(MAKE) -f mk/lib.mk verify
 
 install_lib: check_lib
 	$(call msg, "INSTALL LIB")
@@ -88,7 +77,7 @@ check_fstarc: install_bin
 	  TAG=fstarc \
 	  FSTAR_LIB=$(call cygpath,ulib) \
 	  FSTAR_ROOT=$(CURDIR) \
-	  $(MAKE) -f mk/fstar-12.mk verify $(MAYBEJ1)
+	  $(MAKE) -f mk/fstar-12.mk verify
 	$(call msg, "DONE CHECK FSTARC")
 
 install_fstarc: check_fstarc
@@ -106,8 +95,8 @@ trim: .force
 
 clean: trim
 	rm -rf $(CURDIR)/out
-	rm -r ulib.checked
-	rm -r fstarc.checked
+	rm -rf ulib.checked
+	rm -rf fstarc.checked
 
 all: install_lib install_fstarc
 
@@ -124,7 +113,8 @@ install: install_lib install_fstarc
 	cp -r out/* $(PREFIX)
 
 package:
-	mkdir pkgtmp
+	rm -rf pkgtmp
+	mkdir -p pkgtmp
 	$(MAKE) install PREFIX=pkgtmp/fstar
 	.scripts/bin-install.sh pkgtmp/fstar
 	.scripts/mk-package.sh pkgtmp fstar$(FSTAR_TAG)

ulib/ml/app/FStar_String.ml

@@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i))
 let collect f s =
   let r = ref "" in
   BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r
-let lowercase = BatString.lowercase
-let uppercase = BatString.uppercase
+let lowercase = BatString.lowercase_ascii
+let uppercase = BatString.uppercase_ascii
 let escaped = BatString.escaped
 let index = get
 exception Found of int