From 090c2a2267290212a7c737ac44a8d5bad702762e Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Fri, 23 Aug 2024 18:01:32 -0700
Subject: [PATCH 01/15] win32: Add setup-dkml.cmd

---
 .github/setup-dkml.cmd | 43 ++++++++++++++++++++++++++++++++++++++++++
 .gitignore             |  6 ++++++
 2 files changed, 49 insertions(+)
 create mode 100644 .github/setup-dkml.cmd

diff --git a/.github/setup-dkml.cmd b/.github/setup-dkml.cmd
new file mode 100644
index 00000000000..d5a23c5d0e6
--- /dev/null
+++ b/.github/setup-dkml.cmd
@@ -0,0 +1,43 @@
+@ECHO OFF
+
+REM Use PowerShell 7+ rather than built-in PowerShell 5 since, for Get-PackageProvider, the PowerShell 5 module path includes conflicting version 7 modules.
+
+REM     Find PWSH.EXE
+where.exe /q pwsh.exe >NUL 2>NUL
+if %ERRORLEVEL% neq 0 (
+    goto NeedPowershellExe
+)
+FOR /F "tokens=* usebackq" %%F IN (`where.exe pwsh.exe`) DO (
+SET "INTERNAL_PWSHEXE=%%F"
+)
+"%INTERNAL_PWSHEXE%" -NoLogo -Help >NUL 2>NUL
+if %ERRORLEVEL% equ 0 (
+    SET "INTERNAL_POWERSHELLEXE=%INTERNAL_PWSHEXE%"
+    goto HavePowershellExe
+)
+
+REM     Find Powershell.EXE
+:NeedPowershellExe
+FOR /F "tokens=* usebackq" %%F IN (`where.exe powershell.exe`) DO (
+SET "INTERNAL_POWERSHELLEXE=%%F"
+)
+"%INTERNAL_POWERSHELLEXE%" -NoLogo -Help >NUL 2>NUL
+if %ERRORLEVEL% neq 0 (
+	echo.
+	echo.Neither 'pwsh.exe' nor 'powershell.exe' were found. Make sure you have
+	echo.PowerShell installed.
+	echo.
+	exit /b 1
+)
+
+REM Install DkML compiler
+:HavePowershellExe
+SET OPAMYES=1
+REM     TODO: Use [dkml-workflows] not [dkml-workflows-prerelease] once 2.1.2 is merged
+if NOT EXIST dkml-workflows (
+    git clone --depth 1 --branch 2.1.2 https://github.com/diskuv/dkml-workflows-prerelease.git dkml-workflows
+)
+IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
+    "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1; exit $LASTEXITCODE"
+)
+exit /b %ERRORLEVEL%
diff --git a/.gitignore b/.gitignore
index e68737386ab..dd60de9b79f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,3 +101,9 @@ nuget/
 
 # devcontainer temp files
 /.devcontainer_build.log
+
+# DkML
+/dkml-workflows/
+/msys64/
+/.ci/o/
+/.ci/sd4/

From 07840c6fff29be588f83d80b2f4323943ef312ab Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Fri, 23 Aug 2024 20:03:42 -0700
Subject: [PATCH 02/15] win32: Add setup-vcpkg.cmd for GMP on Windows

---
 .github/setup-vcpkg.cmd | 18 ++++++++++++++++++
 .gitignore              |  4 ++++
 2 files changed, 22 insertions(+)
 create mode 100644 .github/setup-vcpkg.cmd

diff --git a/.github/setup-vcpkg.cmd b/.github/setup-vcpkg.cmd
new file mode 100644
index 00000000000..4296a87cbc7
--- /dev/null
+++ b/.github/setup-vcpkg.cmd
@@ -0,0 +1,18 @@
+@ECHO OFF
+
+if NOT EXIST vcpkg (
+    git clone https://github.com/microsoft/vcpkg.git
+)
+IF NOT EXIST vcpkg\vcpkg.exe (
+    cd vcpkg && CALL bootstrap-vcpkg.bat -disableMetrics && cd ..
+)
+
+REM Make CI-friendly binary cache at vcpkg\archive
+SET VCPKG_BINARY_SOURCES=clear;files,%CD%\vcpkg\archive,readwrite
+
+REM Install to vcpkg_installed (which is the primary thing to be cached in CI)
+REM     TODO: This uses the default x64-windows triplet, but that builds both Debug and Release.
+REM     Confer: https://github.com/microsoft/vcpkg/issues/10683#issuecomment-1968853554
+IF NOT EXIST vcpkg_installed\x64-windows\lib\pkgconfig\gmp.pc (
+    vcpkg\vcpkg install --x-install-root=%CD%\vcpkg_installed gmp
+)
diff --git a/.gitignore b/.gitignore
index dd60de9b79f..2be00dda854 100644
--- a/.gitignore
+++ b/.gitignore
@@ -107,3 +107,7 @@ nuget/
 /msys64/
 /.ci/o/
 /.ci/sd4/
+
+# vcpkg
+/vcpkg/
+/vcpkg_installed/

From ed88192fb40280e0f00dcf890e361ed96f60802a Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Fri, 23 Aug 2024 20:39:43 -0700
Subject: [PATCH 03/15] win32: Add conf-gmp.4+vcpkg

---
 ocaml/repo/dune                               |  1 +
 .../packages/conf-gmp/conf-gmp.4+vcpkg/opam   | 20 +++++++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 ocaml/repo/dune
 create mode 100644 ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam

diff --git a/ocaml/repo/dune b/ocaml/repo/dune
new file mode 100644
index 00000000000..c81f2e0f8fc
--- /dev/null
+++ b/ocaml/repo/dune
@@ -0,0 +1 @@
+(dirs) ; Disable Dune scanning this subtree
\ No newline at end of file
diff --git a/ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam b/ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam
new file mode 100644
index 00000000000..e6ef06806bc
--- /dev/null
+++ b/ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam
@@ -0,0 +1,20 @@
+opam-version: "2.0"
+maintainer: "nbraud"
+homepage: "http://gmplib.org/"
+bug-reports: "https://github.com/ocaml/opam-repository/issues"
+license: "GPL-1.0-or-later"
+synopsis: "Virtual package relying on a GMP lib system installation"
+description:
+  "This package can only install if the GMP lib is installed on the system. Requires the VCPKG_INSTALLED environment variable."
+authors: "nbraud"
+build: [
+  ["sh" "-exc" """`ocamlc -config-var c_compiler` -c $CFLAGS -I "$VCPKG_INSTALLED/include" test.c """]
+]
+extra-source "test.c" {
+  src:
+    "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/conf-gmp/test.c.4"
+  checksum: [
+    "sha256=54a30735f1f271a2531526747e75716f4490dd7bc1546efd6498ccfe3cc4d6fb"
+    "md5=2fd2970c293c36222a6d299ec155823f"
+  ]
+}
\ No newline at end of file

From 6057f21d358c3a982b4e505ad07ebdd0c3e76f0e Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Fri, 23 Aug 2024 22:05:46 -0700
Subject: [PATCH 04/15] win32: Add setup-z3.cmd

---
 .github/setup-z3.cmd | 11 +++++++++++
 .gitignore           |  4 ++++
 2 files changed, 15 insertions(+)
 create mode 100644 .github/setup-z3.cmd

diff --git a/.github/setup-z3.cmd b/.github/setup-z3.cmd
new file mode 100644
index 00000000000..d404419ba0f
--- /dev/null
+++ b/.github/setup-z3.cmd
@@ -0,0 +1,11 @@
+@ECHO OFF
+
+IF NOT EXIST z3-4.8.5-x64-win.zip (
+    powershell -NoProfile -ExecutionPolicy Bypass -Command "(New-Object Net.WebClient).DownloadFile('https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip', 'z3-4.8.5-x64-win.zip')"
+)
+
+IF NOT EXIST z3_installed\bin\z3.exe (
+    powershell -NoProfile -ExecutionPolicy Bypass -Command "Expand-Archive -Force 'z3-4.8.5-x64-win.zip' 'z3_installed'"
+    xcopy /s /e /y z3_installed\z3-4.8.5-x64-win z3_installed\
+    rmdir /s /q z3_installed\z3-4.8.5-x64-win
+)
diff --git a/.gitignore b/.gitignore
index 2be00dda854..5e07c54229f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -111,3 +111,7 @@ nuget/
 # vcpkg
 /vcpkg/
 /vcpkg_installed/
+
+# setup-z3.cmd
+/z3-4.8.5-x64-win.zip
+/z3_installed

From 6fc7d01cdd031f5ab21b680acaac5e1fc52206eb Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Mon, 26 Aug 2024 11:46:03 -0700
Subject: [PATCH 05/15] Add "make package DISABLE_FSHARP=1" option

---
 src/ocaml-output/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ocaml-output/Makefile b/src/ocaml-output/Makefile
index 3d9fe1bf7cf..5c6262f4dd3 100644
--- a/src/ocaml-output/Makefile
+++ b/src/ocaml-output/Makefile
@@ -122,7 +122,7 @@ package:
 	@# Install F* into the package
 	+PREFIX=$(package_prefix) $(MAKE) install
 	@# Make the F* ulib F# DLL (NOT the nuget package)
-	+PREFIX=$(package_prefix) $(MAKE) -C $(FSTAR_HOME)/ulib ulib-in-fsharp-dll
+	+[ "$(DISABLE_FSHARP)" = 1 ] || PREFIX=$(package_prefix) $(MAKE) -C $(FSTAR_HOME)/ulib ulib-in-fsharp-dll
 	@# Then the version file.
 	cp ../../version.txt $(package_prefix)/
 	@# Documentation and licenses

From 55701c8b1311518c70c942860604e7831e579f4b Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Mon, 26 Aug 2024 12:03:48 -0700
Subject: [PATCH 06/15] Check for Cygwin libgmp-10.dll or native gmp-10.dll

---
 src/ocaml-output/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ocaml-output/Makefile b/src/ocaml-output/Makefile
index 5c6262f4dd3..fb4f01e5b01 100644
--- a/src/ocaml-output/Makefile
+++ b/src/ocaml-output/Makefile
@@ -130,7 +130,7 @@ package:
 	cp $(Z3_LICENSE) $(package_prefix)/LICENSE-z3.txt
 	@# Z3
 ifeq ($(OS),Windows_NT)
-	cp $(shell which libgmp-10.dll) $(package_prefix)/bin
+	GMPDLL=`command -v libgmp-10.dll || command -v gmp-10.dll`; install "$$GMPDLL" $(package_prefix)/bin
 	cp $(Z3_DIR)/*.exe $(Z3_DIR)/*.dll $(Z3_DIR)/*.lib $(package_prefix)/bin
 	chmod a+x $(package_prefix)/bin/z3.exe $(package_prefix)/bin/*.dll
 	zip -r -9 $(PACKAGE_NAME).zip fstar

From 371ed2826e880e8624d09ba99315f213f1576559 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Mon, 26 Aug 2024 15:21:14 -0700
Subject: [PATCH 07/15] win32: Install zip

---
 .github/setup-dkml.cmd | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/setup-dkml.cmd b/.github/setup-dkml.cmd
index d5a23c5d0e6..7016323697c 100644
--- a/.github/setup-dkml.cmd
+++ b/.github/setup-dkml.cmd
@@ -30,7 +30,7 @@ if %ERRORLEVEL% neq 0 (
 	exit /b 1
 )
 
-REM Install DkML compiler
+REM Install DkML compiler including MSYS2
 :HavePowershellExe
 SET OPAMYES=1
 REM     TODO: Use [dkml-workflows] not [dkml-workflows-prerelease] once 2.1.2 is merged
@@ -40,4 +40,9 @@ if NOT EXIST dkml-workflows (
 IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
     "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1; exit $LASTEXITCODE"
 )
+
+REM Install MSYS2's zip.exe so `make package` works
+if NOT EXIST msys64\usr\bin\zip.exe (
+    msys64\usr\bin\pacman -Sy --noconfirm --needed zip
+)
 exit /b %ERRORLEVEL%

From b766e34cfb7890d60acbd32f0725ca0e84afe781 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Fri, 23 Aug 2024 22:48:20 -0700
Subject: [PATCH 08/15] win32: Add CI using DkML

Uses fstar CI machines not GitHub CI machines.
---
 .github/workflows/windows-dk.yml | 102 +++++++++++++++++++++++++++++++
 1 file changed, 102 insertions(+)
 create mode 100644 .github/workflows/windows-dk.yml

diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
new file mode 100644
index 00000000000..34f143baa62
--- /dev/null
+++ b/.github/workflows/windows-dk.yml
@@ -0,0 +1,102 @@
+name: FStar Windows Package built with Dk
+
+on:
+  push:
+    branches:
+      - 'main'
+      - 'dkml'
+  workflow_dispatch:
+
+jobs:
+
+  build-windows:
+
+    runs-on: [self-hosted, Windows, X64]
+    #runs-on: windows-2022
+
+    # Use POSIX shell as default.
+    defaults:
+      run:
+        shell: ${{ github.workspace }}\msys64\usr\bin\env.exe MSYS2_ARG_CONV_EXCL=* MSYSTEM=CLANG64 CHERE_INVOKING=yes OPAMYES=1 TRIPLET=x64-windows ${{ github.workspace }}\msys64\usr\bin\sh.exe -e {0}
+
+    steps:
+    - name: Check out repo
+      uses: actions/checkout@v3
+
+    - name: Restore GMP and z3 from cache
+      uses: actions/cache/restore@v4
+      id: cache-vcpkg-z3
+      with:
+        path: |
+          vcpkg_installed
+          z3_installed
+        key: vcpkg-z3-${{ runner.os }}
+
+    - name: Install GMP library and Z3 executable
+      if: steps.cache-vcpkg-z3.outputs.cache-hit != 'true'
+      run: |
+        .github/setup-vcpkg.cmd
+        .github/setup-z3.cmd
+
+    - name: Cache GMP and z3
+      uses: actions/cache/save@v4
+      # always save cache, even on failures
+      if: steps.cache-vcpkg-z3.outputs.cache-hit != 'true'
+      with:
+        path: |
+          vcpkg_installed
+          z3_installed
+        key: ${{ steps.cache-vcpkg-z3.outputs.cache-primary-key }}
+
+    - name: Restore DkML distribution from cache
+      uses: actions/cache/restore@v4
+      id: cache-dkml-dist
+      with:
+        path: |
+          .ci/o
+          .ci/sd4
+          msys64
+        key: dkml-dist-2-${{ runner.os }}
+
+    - name: Setup DkML distribution
+      if: steps.cache-dkml-dist.outputs.cache-hit != 'true'
+      shell: pwsh -command ". '{0}'"
+      run: |
+        .github/setup-dkml.cmd
+
+    - name: Cache DkML distribution
+      uses: actions/cache/save@v4
+      # always save cache, even on failures
+      if: steps.cache-dkml-dist.outputs.cache-hit != 'true'
+      with:
+        path: |
+          .ci/o
+          .ci/sd4
+          msys64
+        key: ${{ steps.cache-dkml-dist.outputs.cache-primary-key }}
+
+    - name: Build a package
+      # Test in PowerShell with:
+      #   $env:CHERE_INVOKING = "yes"; $env:MSYSTEM = "CLANG64"; msys64\usr\bin\dash.exe -lc 'export OPAMYES=1; export TRIPLET=x64-windows; export VCPKG_INSTALLED=$(cygpath -am vcpkg_installed/$TRIPLET); PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"; opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action && opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam && env "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig" opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries && opamrun exec -- make package DISABLE_FSHARP=1'
+      run: |
+          export VCPKG_INSTALLED=$(cygpath -am "vcpkg_installed/$TRIPLET")
+          PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"
+          opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action
+          opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg
+
+          export "TMP=$RUNNER_TEMP"
+          export "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig"
+          opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries
+          opamrun exec -- make -j package DISABLE_FSHARP=1 && echo "There is a CR at the end of this line"
+
+    - name: Test the package
+      run: |
+        PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"
+        export TMP=$RUNNER_TEMP
+        opamrun exec -- env CI_THREADS=24 bash -x .scripts/test_package.sh && echo "There is a CR at the end of this line"
+
+    - name: Upload artifact
+      uses: actions/upload-artifact@v3
+      with:
+        name: fstar-Windows_x86_64.zip
+        path: src\ocaml-output\fstar.zip

From cb1ba94c9df17238e646c93aa12f4c155e7e77d4 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Tue, 27 Aug 2024 02:11:49 -0700
Subject: [PATCH 09/15] win32: Install .NET

---
 .github/setup-dotnet.cmd         | 39 ++++++++++++++++++++++++++++++++
 .github/workflows/windows-dk.yml | 12 +++++++---
 .gitignore                       |  7 ++++++
 3 files changed, 55 insertions(+), 3 deletions(-)
 create mode 100644 .github/setup-dotnet.cmd

diff --git a/.github/setup-dotnet.cmd b/.github/setup-dotnet.cmd
new file mode 100644
index 00000000000..b7ab68b4312
--- /dev/null
+++ b/.github/setup-dotnet.cmd
@@ -0,0 +1,39 @@
+@ECHO OFF
+
+REM Use PowerShell 7+ rather than built-in PowerShell 5 since, for Get-PackageProvider, the PowerShell 5 module path includes conflicting version 7 modules.
+
+REM     Find PWSH.EXE
+where.exe /q pwsh.exe >NUL 2>NUL
+if %ERRORLEVEL% neq 0 (
+    goto NeedPowershellExe
+)
+FOR /F "tokens=* usebackq" %%F IN (`where.exe pwsh.exe`) DO (
+SET "INTERNAL_PWSHEXE=%%F"
+)
+"%INTERNAL_PWSHEXE%" -NoLogo -Help >NUL 2>NUL
+if %ERRORLEVEL% equ 0 (
+    SET "INTERNAL_POWERSHELLEXE=%INTERNAL_PWSHEXE%"
+    goto HavePowershellExe
+)
+
+REM     Find Powershell.EXE
+:NeedPowershellExe
+FOR /F "tokens=* usebackq" %%F IN (`where.exe powershell.exe`) DO (
+SET "INTERNAL_POWERSHELLEXE=%%F"
+)
+"%INTERNAL_POWERSHELLEXE%" -NoLogo -Help >NUL 2>NUL
+if %ERRORLEVEL% neq 0 (
+	echo.
+	echo.Neither 'pwsh.exe' nor 'powershell.exe' were found. Make sure you have
+	echo.PowerShell installed.
+	echo.
+	exit /b 1
+)
+
+REM Install Microsoft.DotNet.SDK.6 (major version of ulib\fs\VS\global.json)
+:HavePowershellExe
+IF NOT EXIST dotnet\dotnet.exe (
+    "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "Invoke-WebRequest 'https://dot.net/v1/dotnet-install.ps1' -OutFile dotnet-install.ps1"
+    REM     Use `winget search Microsoft.DotNet.SDK` to search versions
+    "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "./dotnet-install.ps1 -InstallDir 'dotnet' -Version '6.0.425'"
+)
diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
index 34f143baa62..883f6014895 100644
--- a/.github/workflows/windows-dk.yml
+++ b/.github/workflows/windows-dk.yml
@@ -17,7 +17,7 @@ jobs:
     # Use POSIX shell as default.
     defaults:
       run:
-        shell: ${{ github.workspace }}\msys64\usr\bin\env.exe MSYS2_ARG_CONV_EXCL=* MSYSTEM=CLANG64 CHERE_INVOKING=yes OPAMYES=1 TRIPLET=x64-windows ${{ github.workspace }}\msys64\usr\bin\sh.exe -e {0}
+        shell: ${{ github.workspace }}\msys64\usr\bin\env.exe MSYS2_ARG_CONV_EXCL=\* MSYSTEM=CLANG64 CHERE_INVOKING=yes OPAMYES=1 TRIPLET=x64-windows DOTNET_CLI_TELEMETRY_OPTOUT=1 ${{ github.workspace }}\msys64\usr\bin\sh.exe -e {0}
 
     steps:
     - name: Check out repo
@@ -75,11 +75,17 @@ jobs:
           msys64
         key: ${{ steps.cache-dkml-dist.outputs.cache-primary-key }}
 
+    - name: Setup .NET
+      shell: powershell -command ". '{0}'"
+      run: .github/setup-dotnet.cmd
+
     - name: Build a package
       # Test in PowerShell with:
-      #   $env:CHERE_INVOKING = "yes"; $env:MSYSTEM = "CLANG64"; msys64\usr\bin\dash.exe -lc 'export OPAMYES=1; export TRIPLET=x64-windows; export VCPKG_INSTALLED=$(cygpath -am vcpkg_installed/$TRIPLET); PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"; opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action && opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam && env "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig" opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries && opamrun exec -- make package DISABLE_FSHARP=1'
+      #   $env:CHERE_INVOKING = "yes"; $env:MSYSTEM = "CLANG64"; msys64\usr\bin\dash.exe -lc 'export OPAMYES=1 TRIPLET=x64-windows MSYS_NO_PATHCONV=1 MSYS2_ARG_CONV_EXCL=\*; export VCPKG_INSTALLED=$(cygpath -am vcpkg_installed/$TRIPLET); export FSTAR_HOME="$PWD/src/ocaml-output/fstar"; PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"; opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action && opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam && env "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig" opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries && opamrun exec -- make package DOTNET=$(cygpath -am dotnet/dotnet.exe)'
       run: |
+          env
           export VCPKG_INSTALLED=$(cygpath -am "vcpkg_installed/$TRIPLET")
+          export FSTAR_HOME=$PWD/src/ocaml-output/fstar
           PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"
           opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action
           opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg
@@ -87,7 +93,7 @@ jobs:
           export "TMP=$RUNNER_TEMP"
           export "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig"
           opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries
-          opamrun exec -- make -j package DISABLE_FSHARP=1 && echo "There is a CR at the end of this line"
+          opamrun exec -- make -j package DOTNET=$(cygpath -am dotnet/dotnet.exe) && echo "There is a CR at the end of this line"
 
     - name: Test the package
       run: |
diff --git a/.gitignore b/.gitignore
index 5e07c54229f..0c94fadd8de 100644
--- a/.gitignore
+++ b/.gitignore
@@ -102,6 +102,9 @@ nuget/
 # devcontainer temp files
 /.devcontainer_build.log
 
+# make package
+src/ocaml-output/fstar.zip
+
 # DkML
 /dkml-workflows/
 /msys64/
@@ -115,3 +118,7 @@ nuget/
 # setup-z3.cmd
 /z3-4.8.5-x64-win.zip
 /z3_installed
+
+# setup-dotnet.cmd
+/dotnet/
+/dotnet-install.ps1

From ba5080934690de0dc8827ba4ff76b655c3ee2161 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Tue, 27 Aug 2024 14:12:50 -0700
Subject: [PATCH 10/15] win32: Run Dk job on each pull request

---
 .github/workflows/windows-dk.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
index 883f6014895..a894488d66c 100644
--- a/.github/workflows/windows-dk.yml
+++ b/.github/workflows/windows-dk.yml
@@ -3,8 +3,8 @@ name: FStar Windows Package built with Dk
 on:
   push:
     branches:
-      - 'main'
       - 'dkml'
+  pull_request:
   workflow_dispatch:
 
 jobs:

From c12e503f1634e0bd72f6166c6de96b6a2895ee3c Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Tue, 27 Aug 2024 15:04:45 -0700
Subject: [PATCH 11/15] win32: Use PowerShell shell for installing GMP

+ Downgrade pwsh to powershell for self-hosted jobs
---
 .github/workflows/windows-dk.yml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
index a894488d66c..70df34bbd28 100644
--- a/.github/workflows/windows-dk.yml
+++ b/.github/workflows/windows-dk.yml
@@ -34,6 +34,7 @@ jobs:
 
     - name: Install GMP library and Z3 executable
       if: steps.cache-vcpkg-z3.outputs.cache-hit != 'true'
+      shell: powershell -command ". '{0}'"
       run: |
         .github/setup-vcpkg.cmd
         .github/setup-z3.cmd
@@ -50,7 +51,7 @@ jobs:
 
     - name: Restore DkML distribution from cache
       uses: actions/cache/restore@v4
-      id: cache-dkml-dist
+      id: cache-dkml-dist-2
       with:
         path: |
           .ci/o
@@ -59,21 +60,21 @@ jobs:
         key: dkml-dist-2-${{ runner.os }}
 
     - name: Setup DkML distribution
-      if: steps.cache-dkml-dist.outputs.cache-hit != 'true'
-      shell: pwsh -command ". '{0}'"
+      if: steps.cache-dkml-dist-2.outputs.cache-hit != 'true'
+      shell: powershell -command ". '{0}'"
       run: |
         .github/setup-dkml.cmd
 
     - name: Cache DkML distribution
       uses: actions/cache/save@v4
       # always save cache, even on failures
-      if: steps.cache-dkml-dist.outputs.cache-hit != 'true'
+      if: steps.cache-dkml-dist-2.outputs.cache-hit != 'true'
       with:
         path: |
           .ci/o
           .ci/sd4
           msys64
-        key: ${{ steps.cache-dkml-dist.outputs.cache-primary-key }}
+        key: ${{ steps.cache-dkml-dist-2.outputs.cache-primary-key }}
 
     - name: Setup .NET
       shell: powershell -command ". '{0}'"

From e71d3eeac75a7f89b5f2ad2458446d454f16c98f Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Wed, 28 Aug 2024 21:31:36 -0700
Subject: [PATCH 12/15] win32: Download tarball rather than use git

There is no 'git' on 'self-hosted' CI machines.
---
 .github/setup-dkml.cmd | 7 ++++++-
 .gitignore             | 4 +++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/.github/setup-dkml.cmd b/.github/setup-dkml.cmd
index 7016323697c..f398fa44611 100644
--- a/.github/setup-dkml.cmd
+++ b/.github/setup-dkml.cmd
@@ -35,7 +35,12 @@ REM Install DkML compiler including MSYS2
 SET OPAMYES=1
 REM     TODO: Use [dkml-workflows] not [dkml-workflows-prerelease] once 2.1.2 is merged
 if NOT EXIST dkml-workflows (
-    git clone --depth 1 --branch 2.1.2 https://github.com/diskuv/dkml-workflows-prerelease.git dkml-workflows
+    IF NOT EXIST dkml-workflows-2.1.2.zip (
+        powershell -NoProfile -ExecutionPolicy Bypass -Command "(New-Object Net.WebClient).DownloadFile('https://github.com/diskuv/dkml-workflows-prerelease/archive/refs/tags/2.1.2.zip', 'dkml-workflows-2.1.2.zip')"
+    )
+    powershell -NoProfile -ExecutionPolicy Bypass -Command "Expand-Archive -Force dkml-workflows-2.1.2.zip"
+    move dkml-workflows-2.1.2\dkml-workflows-prerelease-2.1.2 dkml-workflows
+    rmdir dkml-workflows-2.1.2
 )
 IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
     "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1; exit $LASTEXITCODE"
diff --git a/.gitignore b/.gitignore
index 0c94fadd8de..76a5c473fdc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -105,8 +105,10 @@ nuget/
 # make package
 src/ocaml-output/fstar.zip
 
-# DkML
+# setup-dkml.cmd
 /dkml-workflows/
+/dkml-workflows-*/
+/dkml-workflows-*.zip
 /msys64/
 /.ci/o/
 /.ci/sd4/

From 5ea7631b222e0a75e0ac832aa106ce23c570ace1 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Wed, 28 Aug 2024 21:27:04 -0700
Subject: [PATCH 13/15] win32: Fail the job if ocamlc.exe is not generated
 during DkML build

---
 .github/setup-dkml.cmd | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/setup-dkml.cmd b/.github/setup-dkml.cmd
index f398fa44611..48b001850c4 100644
--- a/.github/setup-dkml.cmd
+++ b/.github/setup-dkml.cmd
@@ -45,6 +45,12 @@ if NOT EXIST dkml-workflows (
 IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
     "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1; exit $LASTEXITCODE"
 )
+IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
+	echo.
+	echo.Failed to build OCaml compiler from DkML distribution.
+	echo.
+	exit /b 1
+)
 
 REM Install MSYS2's zip.exe so `make package` works
 if NOT EXIST msys64\usr\bin\zip.exe (

From 01e5d1ae7b602cff9befdd155d5ca06e183415e1 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Wed, 28 Aug 2024 11:51:54 -0700
Subject: [PATCH 14/15] win32: DkML runs on GitHub Actions runner

---
 .github/workflows/windows-dk.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
index 70df34bbd28..6dbc89d45c3 100644
--- a/.github/workflows/windows-dk.yml
+++ b/.github/workflows/windows-dk.yml
@@ -11,8 +11,8 @@ jobs:
 
   build-windows:
 
-    runs-on: [self-hosted, Windows, X64]
-    #runs-on: windows-2022
+    # runs-on: [self-hosted, Windows, X64]
+    runs-on: windows-2022
 
     # Use POSIX shell as default.
     defaults:

From 5c1849f503e655ff5171be7eb9dfb51a79c2a8c2 Mon Sep 17 00:00:00 2001
From: Jonah Beckford <9566106-jonahbeckford@users.noreply.gitlab.com>
Date: Wed, 28 Aug 2024 13:11:28 -0700
Subject: [PATCH 15/15] win32: MSVC version as DkML cache key. Cache .NET

---
 .github/setup-dkml.cmd           | 23 +++++-----
 .github/workflows/windows-dk.yml | 77 ++++++++++++++++++++++++++------
 2 files changed, 76 insertions(+), 24 deletions(-)

diff --git a/.github/setup-dkml.cmd b/.github/setup-dkml.cmd
index 48b001850c4..9e6e951c6e5 100644
--- a/.github/setup-dkml.cmd
+++ b/.github/setup-dkml.cmd
@@ -23,11 +23,11 @@ SET "INTERNAL_POWERSHELLEXE=%%F"
 )
 "%INTERNAL_POWERSHELLEXE%" -NoLogo -Help >NUL 2>NUL
 if %ERRORLEVEL% neq 0 (
-	echo.
-	echo.Neither 'pwsh.exe' nor 'powershell.exe' were found. Make sure you have
-	echo.PowerShell installed.
-	echo.
-	exit /b 1
+    echo.
+    echo.Neither 'pwsh.exe' nor 'powershell.exe' were found. Make sure you have
+    echo.PowerShell installed.
+    echo.
+    exit /b 1
 )
 
 REM Install DkML compiler including MSYS2
@@ -43,13 +43,14 @@ if NOT EXIST dkml-workflows (
     rmdir dkml-workflows-2.1.2
 )
 IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
-    "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1; exit $LASTEXITCODE"
+    "%INTERNAL_POWERSHELLEXE%" -NoProfile -ExecutionPolicy Bypass -Command "& dkml-workflows\test\pc\setup-dkml-windows_x86_64.ps1 %*; exit $LASTEXITCODE"
 )
-IF NOT EXIST .ci\o\dkml\bin\ocamlc.exe (
-	echo.
-	echo.Failed to build OCaml compiler from DkML distribution.
-	echo.
-	exit /b 1
+if %ERRORLEVEL% neq 0 (
+    echo.
+    echo.Failed to build OCaml compiler from DkML distribution.
+    echo.Exit code: %ERRORLEVEL%
+    echo.
+    exit /b 1
 )
 
 REM Install MSYS2's zip.exe so `make package` works
diff --git a/.github/workflows/windows-dk.yml b/.github/workflows/windows-dk.yml
index 6dbc89d45c3..29fe14d5c2d 100644
--- a/.github/workflows/windows-dk.yml
+++ b/.github/workflows/windows-dk.yml
@@ -3,7 +3,7 @@ name: FStar Windows Package built with Dk
 on:
   push:
     branches:
-      - 'dkml'
+      - 'dkml*'
   pull_request:
   workflow_dispatch:
 
@@ -14,10 +14,20 @@ jobs:
     # runs-on: [self-hosted, Windows, X64]
     runs-on: windows-2022
 
-    # Use POSIX shell as default.
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      TRIPLET: x64-windows
+      OPAMYES: 1
+
+      # Settings for MSYS2
+      CHERE_INVOKING: yes
+      MSYSTEM: CLANG64
+      MSYS2_ARG_CONV_EXCL: '*'
+
+    # Use bash shell as default.
     defaults:
       run:
-        shell: ${{ github.workspace }}\msys64\usr\bin\env.exe MSYS2_ARG_CONV_EXCL=\* MSYSTEM=CLANG64 CHERE_INVOKING=yes OPAMYES=1 TRIPLET=x64-windows DOTNET_CLI_TELEMETRY_OPTOUT=1 ${{ github.workspace }}\msys64\usr\bin\sh.exe -e {0}
+        shell: ${{ github.workspace }}\msys64\usr\bin\bash.exe --login --noprofile --norc -eo pipefail {0}
 
     steps:
     - name: Check out repo
@@ -49,45 +59,86 @@ jobs:
           z3_installed
         key: ${{ steps.cache-vcpkg-z3.outputs.cache-primary-key }}
 
+    - name: Cache MSYS2
+      uses: actions/cache@v4
+      id: cache-msys2
+      with:
+        path: msys64
+        key: msys2-${{ runner.os }}
+
+    - name: Get DkML cache key
+      # Because GitHub public runners have indeterminate MSVC versions (ex. 14.41.34120 or 14.40.33807), or
+      # more accurately multiple runner versions (ex. 20240825.1.0) can be active in the GitHub runner fleet,
+      # we have to cache OCaml specific to the MSVC version. For example, one on runner the libraries
+      # can be in C:\VS\VC\Tools\MSVC\14.40.33807\lib\x64 while another is at
+      # C:\VS\VC\Tools\MSVC\14.40.34120\lib\x64.
+      #
+      # Hardcoded MSVC versions are in:
+      # 1. The values in .ci/sd4/msvcenv (from setup-dkml) are specific to the MSVC minor version.
+      # 2. Worse, OCaml is not relocatable, so ocamlopt.exe is specific to the MSVC minor version.
+      #
+      # Artifacts:
+      # - msys64/ (cached in prior step)
+      # - .ci/sd4/ (.ci/sd4/msvcenv is used as a cache key 1-to-1 with MSVC version)
+      shell: powershell -command ". '{0}'"
+      run: |
+        .github/setup-dkml.cmd -SKIP_OPAM_MODIFICATIONS true
+        Get-Content .ci\sd4\msvcenv
+
     - name: Restore DkML distribution from cache
       uses: actions/cache/restore@v4
-      id: cache-dkml-dist-2
+      id: cache-dkml
       with:
         path: |
           .ci/o
           .ci/sd4
-          msys64
-        key: dkml-dist-2-${{ runner.os }}
+        key: dkml-1-${{ runner.os }}-${{ hashFiles('.ci/sd4/msvcenv') }}
 
     - name: Setup DkML distribution
-      if: steps.cache-dkml-dist-2.outputs.cache-hit != 'true'
+      if: steps.cache-dkml.outputs.cache-hit != 'true'
       shell: powershell -command ". '{0}'"
-      run: |
-        .github/setup-dkml.cmd
+      run: .github/setup-dkml.cmd
 
     - name: Cache DkML distribution
       uses: actions/cache/save@v4
       # always save cache, even on failures
-      if: steps.cache-dkml-dist-2.outputs.cache-hit != 'true'
+      if: steps.cache-dkml.outputs.cache-hit != 'true'
       with:
         path: |
           .ci/o
           .ci/sd4
-          msys64
-        key: ${{ steps.cache-dkml-dist-2.outputs.cache-primary-key }}
+        key: ${{ steps.cache-dkml.outputs.cache-primary-key }}
+
+    - name: Restore .NET
+      uses: actions/cache/restore@v4
+      id: cache-dotnet
+      with:
+        path: dotnet
+        key: dotnet-${{ runner.os }}
 
     - name: Setup .NET
+      if: steps.cache-dotnet.outputs.cache-hit != 'true'
       shell: powershell -command ". '{0}'"
       run: .github/setup-dotnet.cmd
 
+    - name: Cache .NET
+      uses: actions/cache/save@v4
+      # always save cache, even on failures
+      if: steps.cache-dotnet.outputs.cache-hit != 'true'
+      with:
+        path: dotnet
+        key: ${{ steps.cache-dotnet.outputs.cache-primary-key }}
+
     - name: Build a package
       # Test in PowerShell with:
       #   $env:CHERE_INVOKING = "yes"; $env:MSYSTEM = "CLANG64"; msys64\usr\bin\dash.exe -lc 'export OPAMYES=1 TRIPLET=x64-windows MSYS_NO_PATHCONV=1 MSYS2_ARG_CONV_EXCL=\*; export VCPKG_INSTALLED=$(cygpath -am vcpkg_installed/$TRIPLET); export FSTAR_HOME="$PWD/src/ocaml-output/fstar"; PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"; opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action && opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg/opam && env "PKG_CONFIG_PATH=$VCPKG_INSTALLED/lib/pkgconfig" opamrun install dune sedlex memtrace ppx_deriving ppx_deriving_yojson menhir process pprint stdint zarith batteries && opamrun exec -- make package DOTNET=$(cygpath -am dotnet/dotnet.exe)'
       run: |
-          env
           export VCPKG_INSTALLED=$(cygpath -am "vcpkg_installed/$TRIPLET")
           export FSTAR_HOME=$PWD/src/ocaml-output/fstar
           PATH="$PWD/.ci/sd4/opamrun:$PWD/vcpkg_installed/$TRIPLET/bin:$PWD/z3_installed/bin:$PATH"
+          opamrun exec -- sh -c 'echo $PATH'
+          opamrun exec -- sh -c 'echo $VCToolsRedistDir'
+          opamrun exec -- sh -c 'command -v cl'
           opamrun pin process git+https://github.com/tahina-pro/ocaml-process.git#taramana_dune --no-action
           opamrun install ./ocaml/repo/packages/conf-gmp/conf-gmp.4+vcpkg