Windows CI using DkML

.github/setup-dkml.cmd

@@ -0,0 +1,60 @@
+@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 including MSYS2
+:HavePowershellExe
+SET OPAMYES=1
+REM     TODO: Use [dkml-workflows] not [dkml-workflows-prerelease] once 2.1.2 is merged
+if NOT EXIST 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"
+)
+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
+if NOT EXIST msys64\usr\bin\zip.exe (
+    msys64\usr\bin\pacman -Sy --noconfirm --needed zip
+)
+exit /b %ERRORLEVEL%

.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'"
+)

.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
+)

.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
+)

.github/workflows/windows-dk.yml

@@ -0,0 +1,160 @@
+name: FStar Windows Package built with Dk
+
+on:
+  push:
+    branches:
+      - 'dkml*'
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+
+  build-windows:
+
+    # runs-on: [self-hosted, Windows, X64]
+    runs-on: windows-2022
+
+    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\bash.exe --login --noprofile --norc -eo pipefail {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'
+      shell: powershell -command ". '{0}'"
+      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: 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
+      with:
+        path: |
+          .ci/o
+          .ci/sd4
+        key: dkml-1-${{ runner.os }}-${{ hashFiles('.ci/sd4/msvcenv') }}
+
+    - name: Setup DkML distribution
+      if: steps.cache-dkml.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.outputs.cache-hit != 'true'
+      with:
+        path: |
+          .ci/o
+          .ci/sd4
+        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: |
+          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
+
+          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 DOTNET=$(cygpath -am dotnet/dotnet.exe) && 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

.gitignore

@@ -101,3 +101,26 @@ nuget/
 
 # devcontainer temp files
 /.devcontainer_build.log
+
+# make package
+src/ocaml-output/fstar.zip
+
+# setup-dkml.cmd
+/dkml-workflows/
+/dkml-workflows-*/
+/dkml-workflows-*.zip
+/msys64/
+/.ci/o/
+/.ci/sd4/
+
+# vcpkg
+/vcpkg/
+/vcpkg_installed/
+
+# setup-z3.cmd
+/z3-4.8.5-x64-win.zip
+/z3_installed
+
+# setup-dotnet.cmd
+/dotnet/
+/dotnet-install.ps1

ocaml/repo/dune

@@ -0,0 +1 @@
+(dirs) ; Disable Dune scanning this subtree

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"
+  ]
+}

src/ocaml-output/Makefile

@@ -122,15 +122,15 @@ 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
 	cp ../../README.md ../../INSTALL.md ../../LICENSE ../../LICENSE-fsharp.txt $(package_prefix)
 	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