Restoring self-hosted windows build

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

@@ -0,0 +1,91 @@
+name: Build F* (Windows, self-hosted)
+
+on:
+  workflow_call:
+  workflow_dispatch:
+  push:
+
+jobs:
+  # We begin from a source package (built in Linux)
+  build-src:
+    uses: ./.github/workflows/build-src.yml
+
+  build-windows:
+    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: clean
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: cd $GITHUB_WORKSPACE && ls -lR && rm -vrf fstar && echo "There is a CR at the end of this line"
+        # ^ remove the directory where the package extracts to and builds,
+        # all files from previous runs remain the runner's working directory
+        # otherwise.
+
+      - 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}'
+
+      - name: Set version
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: |
+          # Setting FSTAR_VERSION for nightly and release builds. If unset,
+          # we use $(version.txt)~dev. Setting it avoids the ~dev.
+          cd $GITHUB_WORKSPACE && 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; echo FSTAR_RELEASE=1 >> $GITHUB_ENV; fi && echo "There is a CR at the end of this line"
+
+      - 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 && 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"
+        # paranoid make clean above, seeing a bunch of these non predictably:
+        # File "libapp/dune", line 18, characters 13-56:
+        # 18 |  (preprocess (pps ppx_deriving.show ppx_deriving_yojson))
+        #                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+        # Error: failed to delete sandbox in
+        # _build/.sandbox/e99d5dd0c933464aff5f4e9946b620a8)
+
+      # - name: Test the package
+      #   shell: C:\cygwin64\bin\bash.exe --login '{0}'
+      #   run: |
+      #     cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && export CC=x86_64-w64-mingw32-gcc.exe && export CI_THREADS=$(nproc) && .scripts/test_package.sh && 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-windows
+    # 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
+          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          ./bin/fstar.exe A.fst -d

.github/workflows/ci.yml

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

mk/src_package_mk.mk

@@ -22,12 +22,14 @@
 # (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
+# LATER EDIT: For the self-hosted runner, this does not seem to be a problem,
+# so do not restrict parallelism.
+# ifeq ($(OS),Windows_NT)
+# .NOTPARALLEL:
+# MAYBEJ1=-j1
+# else
+# MAYBEJ1=
+# endif
 
 include mk/common.mk
 

mk/stage0.mk

@@ -1,4 +1,3 @@
-# This file is used (or created) by the bring-stage0 rule in the toplevel Makefile
 
 include $(FSTAR_ROOT)/mk/common.mk