Fix cross-platform build: replace symlinks with copy_files by elefthei · Pull Request #4085 · FStarLang/FStar

elefthei · 2026-01-16T00:08:40Z

Tested on Windows 11 pwsh and WSL (Arch). Replace symlinks with dune copy_files directives to fix build on Windows where symlinks are not well supported. Remove all symlinks from git and use copy_files to copy source files from ulib/ml to build directories.

Changes:

Replace symlinks in stage1/stage2 dune configs with copy_files
Generate integer modules (FStar_Int*, FStar_UInt*) using rules
Copy files from ulib/ml/{app,app-extra,plugin} and src/ml
Fix stats_record and with_error_context to avoid dependency issues
Create subdirectories for ulib.ml and ulib.pluginml with copy_files

This ensures the build works on both Windows and Linux without requiring symlink support.

mtzguido · 2026-01-20T23:47:31Z

mk/stage.mk

 	@# Seems to need one final build?
 	cd dune && $(DUNE) build $(FSTAR_DUNE_BUILD_OPTIONS)
-	cd dune && $(DUNE) install $(FSTAR_DUNE_OPTIONS) --prefix=$(PREFIX)
+	cd dune && $(DUNE) install $(FSTAR_DUNE_OPTIONS) --prefix=$(call cygpath,$(PREFIX))


Should this also be platform_path? What if cygpath is not present?

Also is cygpath really needed here and below? Do relative paths not work?

mtzguido · 2026-01-20T23:49:07Z

src/ml/FStarC_Extraction_ML_PrintML.ml

 open Ast_helper
 open Ast
 open Ppxlib.Ast_builder.Default
-open Longident


Are the changes in this file fixing the build with 5.4.0? That's great! Could it be put into a standalone PR?

mtzguido · 2026-01-20T23:51:36Z

stage1/dune/fstar-guts/dune

+(copy_files ../../../stage0/dune/fstar-guts/fstarc.ml/*.ml)
+(copy_files ../../../stage0/dune/fstar-guts/fstarc.ml/*.mli)
+(copy_files ../../../stage0/dune/fstar-guts/app/*.ml)
+(copy_files ../../../stage0/dune/fstar-guts/app/*.mli)


There won't be any *.mli files generated, so those lines could be removed. We could also just use * I think.

Also, the first two lines are wrong I think. The fstarc.ml we should use is the one in stage1.

I think this change would also mean that, when a file is deleted from F* sources, the .ml file will be retained in this directory. There is logic in the makefile to delete these spurious files from the fstarc.ml directory, but the copy here would not take that into account. Is that right? It's not terrible, but we should maybe write a small note.

mtzguido · 2026-01-22T18:33:59Z

stage1/dune/fstar-guts/dune

+(rule
+  (target FStar_UInt16.ml)
+  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 16))))


This logic seems to be repeated around 9 times now. Can it be simplified?

mtzguido · 2026-01-22T18:35:14Z

stage1/dune/fstar-plugins/dune

+  (target FStar_UInt16.ml)
+  (deps mk_int_file.sh FStar_Ints.ml.body)
+  (action (with-stdout-to %{target}
+    (bash "echo 'module M = Stdint.Uint16'; echo 'type uint16 = M.t'; echo 'let n = Prims.of_int 16'; echo ''; echo 'let uint_to_t x = M.of_string (Z.to_string x)'; echo 'let __uint_to_t = uint_to_t'; cat FStar_Ints.ml.body"))))


Shouldn't this just call the mk_int_file.sh script?

mtzguido · 2026-01-22T18:36:10Z

ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml.disabled

@@ -162,7 +162,7 @@ let call_subtac g (t : unit -> unit __tac) u ty =
 let call_subtac_tm               = from_tac_4 "B.call_subtac_tm" B.call_subtac_tm

 let stats_record (s : string) (f : unit -> 'c __tac) : 'c __tac =
-  from_tac_2 "B.stats_record" (B.stats_record () ()) s (to_tac_0 (f ()))
+  TM.mk_tac (fun ps -> FStarC_Stats.record s (fun _ -> TM.run (f ()) ps))


Spurious changes here?

This is for 5.4.0 compatibility, maybe this should be a separate change

mtzguido · 2026-01-22T18:41:42Z

Thanks Lef, I left some comments. In general I'm slightly concerned about duplication, but if that's what it takes to get a native Windows build then so be it : ).

…flaky proof

- Windows CI now uses ocaml/setup-ocaml@v3 with bash (Cygwin) instead of winget+PowerShell - this automatically handles zarith/GMP dependencies - Makefile now detects Cygwin/MSYS environments via uname and uses Unix commands when running in those environments - USE_UNIX_CMDS variable controls whether to use Unix or PowerShell commands - Package target handles CYGWIN/MINGW in OS name for correct package naming

The kernel.org mirror used by ocaml/setup-ocaml@v3's built-in Cygwin setup has signature verification issues. Following the upstream pattern, we use cygwin/cygwin-install-action@master which handles mirror fallback better and installs the required GMP/libffi packages for zarith.

The kernel.org Cygwin mirror is having signature verification issues. Using a known reliable mirror from the official Cygwin mirror list.

…m\.last-env\env-af1c662855dbfe768f60cb2a65c64014-0' $env:OPAM_SWITCH_PREFIX = 'C:\Users\eioannidis\AppData\Local\opam\default' $env:OCAMLTOP_INCLUDE_PATH = 'C:\Users\eioannidis\AppData\Local\opam\default\lib\toplevel' $env:CAML_LD_LIBRARY_PATH = 'C:\Users\eioannidis\AppData\Local\opam\default\lib\stublibs;C:\Users\eioannidis\AppData\Local\opam\default\lib\ocaml\stublibs;C:\Users\eioannidis\AppData\Local\opam\default\lib\ocaml' $env:OCAML_TOPLEVEL_PATH = 'C:\Users\eioannidis\AppData\Local\opam\default\lib\toplevel' $env:MANPATH = ':/cygdrive/c/Users/eioannidis/AppData/Local/opam/default/man' $env:Path = 'C:\Users\eioannidis\AppData\Local\opam\default\bin;C:\Users\eioannidis\AppData\Local\opam\.cygwin\root\usr\x86_64-w64-mingw32\sys-root\mingw\bin;C:\Program Files\PowerShell\7;C:\Program Files\glzr.io\GlazeWM\\cli;C:\Program Files\Microsoft SDKs\Azure\CLI2\wbin;C:\Windows\system32;C:\Windows;C:\Windows\System32\Wbem;C:\Windows\System32\WindowsPowerShell\v1.0\;C:\Windows\System32\OpenSSH\;C:\Program Files\Azure Dev CLI;C:\Program Files\GitHub CLI\;C:\Users\vmadmin\AppData\Local\Microsoft\WindowsApps;C:\Program Files\Microsoft SQL Server\Client SDK\ODBC\170\Tools\Binn\;C:\Program Files\Microsoft SQL Server\150\Tools\Binn\;C:\.tools\dotnet;C:\.tools\.npm-global;C:\Windows\system32\config\systemprofile\AppData\Local\Microsoft\WindowsApps;C:\Program Files\Microsoft Dev Box Agent\Scripts;C:\Program Files\PowerShell\7\;C:\Program Files\VFS for Git;C:\Program Files\dotnet\;C:\Program Files\nodejs\;C:\Program Files\Graphviz\bin;C:\Program Files (x86)\Windows Kits\10\Windows Performance Toolkit\;C:\Program Files\Microsoft SQL Server\170\Tools\Binn\;C:\ProgramData\chocolatey\bin;C:\Program Files\CMake\bin;C:\Program Files\Git\cmd;C:\Program Files\Go\bin;C:\Program Files\Docker\Docker\resources\bin;C:\Program Files\PowerShell\7;C:\Program Files\glzr.io\GlazeWM\\cli;C:\Program Files\Microsoft SDKs\Azure\CLI2\wbin;C:\Windows\system32;C:\Windows;C:\Windows\System32\Wbem;C:\Windows\System32\WindowsPowerShell\v1.0\;C:\Windows\System32\OpenSSH\;C:\Program Files\Azure Dev CLI;C:\Program Files\GitHub CLI\;C:\Users\vmadmin\AppData\Local\Microsoft\WindowsApps;C:\Program Files\Microsoft SQL Server\Client SDK\ODBC\170\Tools\Binn\;C:\Program Files\Microsoft SQL Server\150\Tools\Binn\;C:\.tools\dotnet;C:\.tools\.npm-global;C:\Windows\system32\config\systemprofile\AppData\Local\Microsoft\WindowsApps;C:\Program Files\Microsoft Dev Box Agent\Scripts;C:\Program Files\PowerShell\7\;C:\Program Files\VFS for Git;C:\Program Files\dotnet\;C:\Program Files\nodejs\;C:\Program Files\Graphviz\bin;C:\Program Files (x86)\Windows Kits\10\Windows Performance Toolkit\;C:\Program Files\Microsoft SQL Server\170\Tools\Binn\;C:\ProgramData\chocolatey\bin;C:\Program Files\CMake\bin;C:\Program Files\Docker\Docker\resources\bin;C:\Program Files\Git\cmd;C:\Users\eioannidis\.local\bin;C:\Users\eioannidis\AppData\Roaming\agency\CurrentVersion;C:\Users\eioannidis\.cargo\bin;C:\Users\eioannidis\AppData\Local\Microsoft\WindowsApps;C:\Users\eioannidis\.dotnet\tools;C:\Users\eioannidis\AppData\Roaming\npm;C:\Users\eioannidis\AppData\Local\Programs\Microsoft VS Code Insiders\bin;C:\tools\neovim\nvim-win64\bin;C:\Users\eioannidis\AppData\Local\PowerToys\DSCModules\;C:\Users\eioannidis\AppData\Local\Microsoft\WinGet\Links;C:\Users\eioannidis\AppData\Local\Pandoc\;C:\Users\eioannidis\AppData\Local\Programs\MiKTeX\miktex\bin\x64\;C:\Users\eioannidis\AppData\Local\Programs\Microsoft VS Code Insiders\bin;C:\Program Files\Git\mingw64\bin;C:\Users\eioannidis\AppData\Local\opam\default\bin;C:\Users\eioannidis\.bun\bin;C:\Users\eioannidis\go\bin;C:\Users\eioannidis\.dotnet\tools' before make commands The dune binary is installed in the opam switch, so we need to source the opam environment before running make commands.

Dune is a Windows binary that doesn't understand Cygwin paths like /cygdrive/d/... Use cygpath -w to convert to Windows paths.

setup-ocaml@v3 has a hardcoded Cygwin mirror (kernel.org) that frequently fails with signature verification errors. Pre-installing all packages it needs via cygwin-install-action with a working mirror (dotsrc.org) so setup-ocaml will find them already installed.

The previous cache contained references to D:\cygwin but we now install Cygwin to C:\cygwin to match setup-ocaml's default location. Invalidate the cache to fix opam path conflicts.

cygpath -w produces backslash paths (D:\\a\\...) which are interpreted as escape sequences by /bin/sh. Use cygpath -m for mixed-mode paths (D:/a/...) with forward slashes that work in both shell commands and Windows-native tools like dune.

The stage2 target only builds the executable in _build/default/, it doesn't copy it to out/bin/. Add make setlink-2 to create the out/bin/fstar symlink that the verify step expects.

mtzguido reviewed Jan 22, 2026

View reviewed changes

elefthei force-pushed the fix/windows-misc branch 28 times, most recently from 220503d to 66b0fb3 Compare February 2, 2026 02:47

elefthei force-pushed the fix/windows-misc branch from 9f83193 to 72f2e93 Compare February 2, 2026 23:28

Lef Ioannidis added 29 commits February 2, 2026 15:53

Retry CI

36d5a4b

Add --proof_recovery for flaky alloc_ proof in LowStar.RVector

be1e461

Make Windows CI do full native build (stage0-stage2) with tests

1f7c9d3

Add Windows build to main CI workflow

fe5046c

Remove --proof_recovery pragma (not settable), keep --z3rlimit 20

870e08b

Fix Windows FSTAR_EXE path: use cygpath -m for dune compatibility

9851ec0

Use bash commands (mkdir, cp) on Windows CI since we run in Cygwin

bc8cfe5

Switch Windows CI to PowerShell, remove Cygwin dependency

5fe8eaf

Windows CI: use winget opam + MSYS2 GMP; increase z3rlimit to 80 for …

3c3fd4b

…flaky proof

Fix Windows PATH after winget install, add missing CP variable for Linux

8f8d836

Use MSVC via opam install system-msvc, fix opam env setup

cbc4f3c

Remove strict out/ check in setlink-2 - just recreate with symlinks

dce9679

Fix Windows CI: add -y flags and remove --switch=default

e9e0f00

Remove duplicate test target definition

bf2504a

Bump OCaml version from 5.3 to 5.4 in opam CI

168e847

Use ocaml/setup-ocaml@v2 for Windows CI (v3 has Cygwin path issues)

11e5372

Use ocaml/setup-ocaml@v3 with main opam-repository for zarith >= 1.14

ef69523

Add opam depext for gcc make flexdll on Windows

0b64e8e

Remove opam depext step (deprecated in opam 2.1+)

2f1dfd8

Use mirrors.dotsrc.org for Cygwin instead of kernel.org

e21a3dc

The kernel.org Cygwin mirror is having signature verification issues. Using a known reliable mirror from the official Cygwin mirror list.

Add debugging output to Windows build

012b20a

Fix FSTAR_EXE path for Cygwin: convert to Windows path for dune

70695e5

Dune is a Windows binary that doesn't understand Cygwin paths like /cygdrive/d/... Use cygpath -w to convert to Windows paths.

chore(ci): use cache-prefix v2 to force fresh opam cache

65dc15a

The previous cache contained references to D:\cygwin but we now install Cygwin to C:\cygwin to match setup-ocaml's default location. Invalidate the cache to fix opam path conflicts.

fix(ci): run setlink-2 to set up out/bin directory after build

7c3cb1f

The stage2 target only builds the executable in _build/default/, it doesn't copy it to out/bin/. Add make setlink-2 to create the out/bin/fstar symlink that the verify step expects.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix cross-platform build: replace symlinks with copy_files#4085

Fix cross-platform build: replace symlinks with copy_files#4085
elefthei wants to merge 33 commits intoFStarLang:masterfrom
elefthei:fix/windows-misc

elefthei commented Jan 16, 2026

Uh oh!

mtzguido Jan 20, 2026

Uh oh!

mtzguido Jan 20, 2026

Uh oh!

mtzguido Jan 20, 2026

Uh oh!

mtzguido Jan 20, 2026

Uh oh!

mtzguido Jan 22, 2026

Uh oh!

mtzguido Jan 22, 2026

Uh oh!

mtzguido Jan 22, 2026

Uh oh!

mtzguido Jan 22, 2026

Uh oh!

elefthei Jan 22, 2026

Uh oh!

mtzguido commented Jan 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

elefthei commented Jan 16, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mtzguido commented Jan 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants