From b5dea9e8470296e96f7bbe747dbae9ce509b4b4f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:48:20 -0800
Subject: [PATCH 01/14] Makefile: factor out binary package creation

---
 .scripts/bin-install.sh | 27 +++++++++++++++++++++++++++
 .scripts/mk-package.sh  |  5 +++++
 Makefile                | 13 ++-----------
 3 files changed, 34 insertions(+), 11 deletions(-)
 create mode 100755 .scripts/bin-install.sh

diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh
new file mode 100755
index 00000000000..14a098f36e6
--- /dev/null
+++ b/.scripts/bin-install.sh
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+# This is called by the Makefile *after* an installation into the
+# prefix, so we add the rest of the files that go into a binary pacakge.
+
+set -eu
+
+if [ $# -ne 1 ]; then
+	echo "Usage: $0 <prefix>" >&2
+	exit 1
+fi
+
+# $1 will usually exist, but mkdir it if not
+PREFIX="$(realpath -m "$1")" # -m: leading dirs allowed to not exist
+
+mkdir -p "${PREFIX}"
+
+if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then
+  .scripts/package_z3.sh "$PREFIX"
+fi
+
+# License and extra files. Not there on normal installs, but present in
+# package.
+cp LICENSE* "$PREFIX"
+cp README.md "$PREFIX"
+cp INSTALL.md "$PREFIX"
+cp version.txt "$PREFIX"
diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh
index 04837dc9aa3..401c2cdef17 100755
--- a/.scripts/mk-package.sh
+++ b/.scripts/mk-package.sh
@@ -1,5 +1,10 @@
 #!/bin/bash
 
+# This will just create a tar.gz or zip out of a directory.
+# You may want to look at src-install.sh and bin-install.sh
+# that generate the layouts for a source and binary package,
+# and are then packaged up with this script.
+
 if [ $# -ne 2 ]; then
 	echo "usage: $0 <install_root> <package_basename>" >&2
 	echo "Default format is tar.gz. Optionally set FSTAR_PACKAGE_FORMAT=zip to generate a zip instead." >&2
diff --git a/Makefile b/Makefile
index 893c290ab51..ab48d7d6d20 100644
--- a/Makefile
+++ b/Makefile
@@ -316,19 +316,10 @@ install: __do-install-stage2
 __do-archive: _force
 	rm -rf $(PKGTMP)
 	# add an 'fstar' top-level directory to the archive
-	$(MAKE) $(INSTALL_RULE) PREFIX=$(abspath $(PKGTMP)/fstar)
-ifneq ($(FSTAR_PACKAGE_Z3),false)
-	.scripts/package_z3.sh $(PKGTMP)/fstar/
-endif
-	@# License and extra files. Not there on normal installs, but present
-	@# in package.
-	cp LICENSE* $(PKGTMP)/fstar/
-	cp README.md $(PKGTMP)/fstar/
-	cp INSTALL.md $(PKGTMP)/fstar/
-	cp version.txt $(PKGTMP)/fstar/
+	$(MAKE) $(INSTALL_RULE) PREFIX="$(abspath $(PKGTMP)/fstar)"
 	$(call bold_msg, "PACKAGE", $(ARCHIVE))
+	.scripts/bin-install.sh "$(PKGTMP)/fstar"
 	.scripts/mk-package.sh "$(PKGTMP)" "$(ARCHIVE)"
-	# tar czf $(ARCHIVE) -h -C $(PKGTMP) --exclude='lib/**/*.fst.config.json' .
 	rm -rf $(PKGTMP)
 
 __do-src-archive: _force

From f8a04299b4242623ecb88b93d132297cacda8933 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 21:07:10 -0800
Subject: [PATCH 02/14] bin-install.sh: strip binaries

---
 .scripts/bin-install.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh
index 14a098f36e6..2adfafb98ba 100755
--- a/.scripts/bin-install.sh
+++ b/.scripts/bin-install.sh
@@ -5,6 +5,10 @@
 
 set -eu
 
+windows () {
+  [ -v OS ] && [ "$OS" = "Windows_NT" ]
+}
+
 if [ $# -ne 1 ]; then
 	echo "Usage: $0 <prefix>" >&2
 	exit 1
@@ -25,3 +29,13 @@ cp LICENSE* "$PREFIX"
 cp README.md "$PREFIX"
 cp INSTALL.md "$PREFIX"
 cp version.txt "$PREFIX"
+
+# Save the megabytes! Strip binaries
+STRIP=strip
+
+if windows; then
+  STRIP="$(pwd)/mk/winwrap.sh $STRIP"
+fi
+
+$STRIP "$PREFIX"/bin/* || true
+$STRIP "$PREFIX"/lib/fstar/z3-*/bin/* || true

From bba989da413e9c3517c508d8c8c9a48e93708af2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:49:25 -0800
Subject: [PATCH 03/14] Remove old check-snapshot-diff script

---
 .scripts/check-snapshot-diff.sh | 36 ---------------------------------
 1 file changed, 36 deletions(-)
 delete mode 100755 .scripts/check-snapshot-diff.sh

diff --git a/.scripts/check-snapshot-diff.sh b/.scripts/check-snapshot-diff.sh
deleted file mode 100755
index ff320d94554..00000000000
--- a/.scripts/check-snapshot-diff.sh
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/bin/bash
-
-set -eu
-
-# This is run by CI to check that the snapshot has not changed after
-# bootstrapping. Must run from the root of the Pulse git repo.
-
-SUCCESS=true
-DIR=ocaml/*/generated # globs are OK
-export GIT_PAGER=cat
-
-# If there's any output, i.e. any file not in HEAD, fail
-if git ls-files --others --exclude-standard -- $DIR | grep -q . &>/dev/null; then
-    SUCCESS=false
-fi
-
-# If there's a diff in existing files, fail
-if ! git diff --exit-code $DIR &>/dev/null; then
-    SUCCESS=false
-fi
-
-if ! $SUCCESS; then
-    echo "*********************************************************"
-    echo " *** SNAPSHOT DIFF:"
-    echo ""
-    echo "$ git status $DIR"
-    git status $DIR
-    echo ""
-    echo "$ git diff -a $DIR"
-    git diff -a $DIR
-    echo "*********************************************************"
-    exit 1
-else
-    echo "Snapshot seems clean"
-    exit 0
-fi

From e245ad57a585dd4e556988c5feb79062497034ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:49:34 -0800
Subject: [PATCH 04/14] winwrap.sh: a utility for silly mixed Cygwin/Windows
 builds

---
 mk/winwrap.sh | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100755 mk/winwrap.sh

diff --git a/mk/winwrap.sh b/mk/winwrap.sh
new file mode 100755
index 00000000000..2c493b61a42
--- /dev/null
+++ b/mk/winwrap.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+# Running ./winwrap.sh cmd args will make replace any cygwin paths in
+# the args before calling cmd. E.g. /cygdrive/c/foo/bar -> c:/foo/bar
+#
+# If none of the arguments are of that shape, this script should be
+# fully transparent, passing arguments to $cmd in exactly the same shape
+# even if they contain spaces, etc.
+
+cmd=$1
+shift
+
+args=()
+
+for arg; do
+	arg=$(echo "$arg" | sed 's,^/cygdrive/\(.\)/,\1:/,')
+	args+=("$arg")
+done
+
+exec $cmd "${args[@]}"

From d418726cb53384a7cbe19e2b14ff9586dd1b1173 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:50:17 -0800
Subject: [PATCH 05/14] F*: remove cygpath translation

It is not the job of F* to do this, nor rely on external processes for
it.
---
 src/basic/FStarC.Common.fst  | 23 -----------------------
 src/basic/FStarC.Common.fsti |  7 -------
 src/basic/FStarC.Options.fst |  4 ++--
 3 files changed, 2 insertions(+), 32 deletions(-)

diff --git a/src/basic/FStarC.Common.fst b/src/basic/FStarC.Common.fst
index db613214251..158c5e8c101 100644
--- a/src/basic/FStarC.Common.fst
+++ b/src/basic/FStarC.Common.fst
@@ -21,29 +21,6 @@ open FStarC.Compiler.Effect
 module List = FStarC.Compiler.List
 module BU = FStarC.Compiler.Util
 
-let has_cygpath =
-    try
-        let t_out = BU.run_process "has_cygpath" "which" ["cygpath"] None in
-        BU.trim_string t_out = "/usr/bin/cygpath"
-    with
-    | _ -> false
-
-let try_convert_file_name_to_mixed =
-  let cache = BU.smap_create 20 in
-  fun (s:string) ->
-    if has_cygpath
-    && BU.starts_with s "/" then
-      match BU.smap_try_find cache s with
-      | Some s ->
-          s
-      | None ->
-          let label = "try_convert_file_name_to_mixed" in
-          let out = BU.run_process label "cygpath" ["-m"; s] None |> BU.trim_string in
-          BU.smap_add cache s out;
-          out
-    else
-      s
-
 let snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b) = BU.atomically (fun () ->
   let len : int = List.length !stackref in
   let arg' = push arg in
diff --git a/src/basic/FStarC.Common.fsti b/src/basic/FStarC.Common.fsti
index eadb6f1711d..8cc4f3d907a 100644
--- a/src/basic/FStarC.Common.fsti
+++ b/src/basic/FStarC.Common.fsti
@@ -21,13 +21,6 @@ open FStarC.Compiler.Effect
 module List = FStarC.Compiler.List
 module BU = FStarC.Compiler.Util
 
-//try to convert filename passed from the editor to mixed path
-//that works on both cygwin and native windows
-//noop if not on cygwin
-//on cygwin emacs this is required
-// NOTE: Will likely be removed soon. F* should not do path translation.
-val try_convert_file_name_to_mixed (fn : string) : string
-
 val snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b)
 
 val rollback (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) : 'a
diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst
index 2dad42c3408..4588f7c6c21 100644
--- a/src/basic/FStarC.Options.fst
+++ b/src/basic/FStarC.Options.fst
@@ -52,7 +52,7 @@ let as_int = function
   | _ -> failwith "Impos: expected Int"
 let as_string = function
   | String b -> b
-  | Path b -> FStarC.Common.try_convert_file_name_to_mixed b
+  | Path b -> b
   | _ -> failwith "Impos: expected String"
 let as_list' = function
   | List ts -> ts
@@ -1847,7 +1847,7 @@ let parse_cmd_line () =
     then set_error_flags()
     else res
   in
-  res, List.map FC.try_convert_file_name_to_mixed !file_list_
+  res, !file_list_
 
 let file_list () =
   !file_list_

From 3ea0a51b943928bfa69aef51442b3c099ffb5002 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:50:55 -0800
Subject: [PATCH 06/14] Find: fix for '\r' in fstar.include

---
 src/basic/FStarC.Find.fst | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst
index aeaead7670a..91b7b1530c5 100644
--- a/src/basic/FStarC.Find.fst
+++ b/src/basic/FStarC.Find.fst
@@ -31,8 +31,11 @@ let read_fstar_include (fn : string) : option (list string) =
     let s = BU.file_get_contents fn in
     let subdirs =
       // Read each line
-      String.split ['\n'] s |>
-      // Trim whitespace (including Windows' \r ! Important!)
+      String.split ['\r'; '\n'] s |>
+      // Trim whitespace. NOTE: Carriage returns (\r) should be trimmed
+      // by BU.trim_string (which is BatString.trim) according to
+      // the docs, but do not seem to be. So instead we use it as a
+      // separator above and just get a few more empty lines.
       List.map BU.trim_string |>
       // And keep the non-empty lines that don't begin with '#'
       List.filter (fun s -> s <> "" && not (String.get s 0 = '#'))

From c7e0659439b0e45539d0691848336d289e9e07cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:53:10 -0800
Subject: [PATCH 07/14] package: ship libgmp-10.dll in Windows

This DLL is needed to run F*, ship it.
---
 .scripts/bin-install.sh | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh
index 2adfafb98ba..b8b3a4e4800 100755
--- a/.scripts/bin-install.sh
+++ b/.scripts/bin-install.sh
@@ -23,6 +23,14 @@ if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then
   .scripts/package_z3.sh "$PREFIX"
 fi
 
+if windows; then
+    # This dll is needed. It must be installed if we're packaging, as we
+    # must have run F* already, but it should probably be obtained from
+    # somewhere else..
+    LIBGMP=$(which libgmp-10.dll) || echo "error: libgmp-10.dll not found! Carrying on..." >&2
+    cp "$LIBGMP" "$PREFIX/bin"
+fi
+
 # License and extra files. Not there on normal installs, but present in
 # package.
 cp LICENSE* "$PREFIX"

From 8be8486728817e3c230df11a660db808315604e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 10 Jan 2025 19:51:38 -0800
Subject: [PATCH 08/14] build: support building source packages in Windows

This patch allows a source package (generated by package-src) to be
built into a native Windows executable. The full build does not yet
work, I think only due to intricacies of the many different kinds of
symlinks in Windows/Cygwin.
---
 .scripts/src-install.sh         |  6 +++
 mk/fstar-12.mk                  |  8 +++-
 mk/lib.mk                       |  8 +++-
 mk/plugins.mk                   |  8 +++-
 mk/src_package_mk.mk            | 81 ++++++++++++++++++++++++++-------
 ulib/ml/app/ints/dune           | 21 +++++----
 ulib/ml/app/ints/mk_int_file.sh |  4 +-
 7 files changed, 107 insertions(+), 29 deletions(-)

diff --git a/.scripts/src-install.sh b/.scripts/src-install.sh
index 544ac436e5b..49848f8a69d 100755
--- a/.scripts/src-install.sh
+++ b/.scripts/src-install.sh
@@ -49,7 +49,13 @@ cp mk/src_package_mk.mk "${PREFIX}/Makefile"
 mkdir "${PREFIX}/mk"
 cp mk/lib.mk "${PREFIX}/mk/lib.mk"
 cp mk/common.mk "${PREFIX}/mk/common.mk"
+cp mk/winwrap.sh "${PREFIX}/mk/winwrap.sh"
 cp -H mk/fstar-12.mk "${PREFIX}/mk/fstar-12.mk"
+mkdir "${PREFIX}/.scripts"
+cp .scripts/bin-install.sh  "${PREFIX}/.scripts"
+cp .scripts/mk-package.sh   "${PREFIX}/.scripts"
+cp .scripts/get_fstar_z3.sh "${PREFIX}/.scripts"
+cp .scripts/package_z3.sh   "${PREFIX}/.scripts"
 
 # Remove extra ML files, rsync has resolved the links
 # into the corresponding files already, and these would be
diff --git a/mk/fstar-12.mk b/mk/fstar-12.mk
index a4f20fb017d..011ac5e58ed 100644
--- a/mk/fstar-12.mk
+++ b/mk/fstar-12.mk
@@ -39,7 +39,13 @@ FSTAR_OPTIONS += --include "$(SRC)"
 
 FSTAR_OPTIONS += $(OTHERFLAGS)
 
-FSTAR = $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
+ifeq ($(OS),Windows_NT)
+WINWRAP=$(FSTAR_ROOT)/mk/winwrap.sh
+else
+WINWRAP=
+endif
+
+FSTAR := $(WINWRAP) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 
 # FIXME: Maintaining this list sucks. Could **the module** itself specify whether it is
 # noextract? Actually, the F* compiler should already know which of its modules are
diff --git a/mk/lib.mk b/mk/lib.mk
index 280e2affcbc..754089224f6 100644
--- a/mk/lib.mk
+++ b/mk/lib.mk
@@ -105,7 +105,13 @@ EXTRACT_NS += +FStar.Int.Cast.Full
 EXTRACT_NS += -FStar.Tactics
 EXTRACT_NS += -FStar.Reflection
 
-FSTAR := $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
+ifeq ($(OS),Windows_NT)
+WINWRAP=$(FSTAR_ROOT)/mk/winwrap.sh
+else
+WINWRAP=
+endif
+
+FSTAR := $(WINWRAP) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 
 EXTRACT := --extract '* $(EXTRACT_NS)'
 
diff --git a/mk/plugins.mk b/mk/plugins.mk
index 91f2cab9437..590a817d280 100644
--- a/mk/plugins.mk
+++ b/mk/plugins.mk
@@ -31,7 +31,13 @@ FSTAR_OPTIONS += --include $(SRC)
 
 FSTAR_OPTIONS += $(OTHERFLAGS)
 
-FSTAR = $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
+ifeq ($(OS),Windows_NT)
+WINWRAP=$(FSTAR_ROOT)/mk/winwrap.sh
+else
+WINWRAP=
+endif
+
+FSTAR = $(WINWRAP) $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 
 # FIXME: Maintaining this list sucks. Could **the module** itself specify whether it is
 # noextract? Or maybe if we find an aptly-named .ml file then we auto skip?
diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk
index bd35b606a94..873325aede4 100644
--- a/mk/src_package_mk.mk
+++ b/mk/src_package_mk.mk
@@ -1,74 +1,121 @@
-# This makefile is for OCaml source distributions and is
-# modeled after stage{1,2}/Makefile, but
-# 1- is standalone, does use common.mk or others
-# 2- does not install the library as it will not be there on
-#    OCaml source distributions
+# This makefile is for OCaml source distributions.
 #
 # FSTAR_DUNE_OPTIONS += --no-print-directory
 # FSTAR_DUNE_OPTIONS += --display=quiet
+#
+# Also note: this Makefile should run in Windows too. Some
+# of the $(call cygpath, ..) below are in support of this. Example
+# windows error:
+#
+# ...
+# dune install --root=dune --prefix=/cygdrive/d/a/FStar/FStar/fstar/out
+# env \
+#   SRC=ulib/ \
+#   FSTAR_EXE=out/bin/fstar.exe \
+#   CACHE_DIR=ulib.checked \
+#   TAG=lib \
+#   CODEGEN=none \
+#   OUTPUT_DIR=none \
+#   make -f mk/lib.mk verify
+# mk/lib.mk:3: *** FSTAR_EXE ("out/bin/fstar.exe") does not exist (cwd = /cygdrive/d/a/FStar/FStar/fstar).  Stop.
+# ...
+#
+# I think this is probably a dune bug.
 
-FSTAR_DUNE_BUILD_OPTIONS := $(FSTAR_DUNE_OPTIONS)
-
-.NOTPARALLEL:
-# Sorry, but dune seems to get confused when its OCAMLPATH is changing
+include mk/common.mk
 
+FSTAR_DUNE_BUILD_OPTIONS := $(FSTAR_DUNE_OPTIONS)
 .DEFAULT_GOAL:= all
 
 .PHONY: _force
 _force:
 
+ifeq ($(OS),Windows_NT)
+cygpath=$(shell cygpath -m "$(abspath $(1))")
+else
+cygpath=$(abspath "$(1)")
+endif
+
 build:
+	$(call msg, "DUNE BUILD")
 	dune build --root=dune $(FSTAR_DUNE_BUILD_OPTIONS)
 
 install_bin: build
-	dune install --root=dune --prefix=$(CURDIR)/out
+	$(call msg, "DUNE INSTALL")
+	dune install --root=dune --prefix=$(call cygpath,out)
 
 check_lib: install_bin
+	$(call msg, "CHECK LIB")
 	env \
 	  SRC=ulib/ \
-	  FSTAR_EXE=out/bin/fstar.exe \
+	  FSTAR_EXE=$(call cygpath,out/bin/fstar.exe) \
 	  CACHE_DIR=ulib.checked \
 	  TAG=lib \
 	  CODEGEN=none \
 	  OUTPUT_DIR=none \
+	  FSTAR_ROOT=$(CURDIR) \
 	  $(MAKE) -f mk/lib.mk verify
 
+ifeq ($(OS),Windows_NT)
+vv=-v
+else
+vv=
+endif
+
 install_lib: check_lib
+	$(call msg, "INSTALL LIB")
 	@# Install library and its checked files
-	cp -H -p -r ulib out/lib/fstar/ulib
-	cp -H -p -r ulib.checked out/lib/fstar/ulib.checked
+	cp $(vv) -T -H -p -r ulib out/lib/fstar/ulib
+	cp $(vv) -T -H -p -r ulib.checked out/lib/fstar/ulib.checked
 	echo 'ulib'          > out/lib/fstar/fstar.include
 	echo 'ulib.checked' >> out/lib/fstar/fstar.include
 
 check_fstarc: install_bin
+	$(call msg, "CHECK FSTARC")
 	env \
 	  SRC=src/ \
-	  FSTAR_EXE=out/bin/fstar.exe \
+	  FSTAR_EXE=$(call cygpath,out/bin/fstar.exe) \
 	  CACHE_DIR=fstarc.checked/ \
 	  CODEGEN=None \
 	  OUTPUT_DIR=None \
 	  TAG=fstarc \
-	  FSTAR_LIB=$(abspath ulib) \
+	  FSTAR_LIB=$(call cygpath,ulib) \
 	  FSTAR_ROOT=$(CURDIR) \
 	  $(MAKE) -f mk/fstar-12.mk all-checked
 
 install_fstarc: check_fstarc
+	$(call msg, "INSTALL FSTARC")
 	@# Install checked files for FStarC
 	mkdir -p out/lib/fstar/fstarc/
-	cp -H -p -r src               out/lib/fstar/fstarc/src
-	cp -H -p -r fstarc.checked    out/lib/fstar/fstarc/src.checked
+	cp $(vv) -T -H -p -r src               out/lib/fstar/fstarc/src
+	cp $(vv) -T -H -p -r fstarc.checked    out/lib/fstar/fstarc/src.checked
 	echo 'src'          > out/lib/fstar/fstarc/fstar.include
 	echo 'src.checked' >> out/lib/fstar/fstarc/fstar.include
 
 trim: _force
+	@echo DUNE CLEAN
 	dune clean $(FSTAR_DUNE_OPTIONS) --root=dune
 
 clean: trim
 	rm -rf $(CURDIR)/out
+	rm -r ulib.checked
+	rm -r fstarc.checked
 
 all: install_lib install_fstarc
 
+install_fstarc: install_lib
+# ^ The windows build in Github actions seems to sporadically
+# hang for over an hour, but sometimes works fine. I suspect
+# some kind of stupid race, so sequentialize these two install
+# phases.
+
 # Needed for 'opam install'
 PREFIX ?= /usr/local
 install: install_lib install_fstarc
+	mkdir -p $(PREFIX)
 	cp -r out/* $(PREFIX)
+
+package:
+	$(MAKE) install PREFIX=fstar
+	.scripts/bin-install.sh fstar
+	.scripts/mk-package.sh fstar fstar$(FSTAR_TAG)
diff --git a/ulib/ml/app/ints/dune b/ulib/ml/app/ints/dune
index cb984f42488..2f7e19e83a6 100644
--- a/ulib/ml/app/ints/dune
+++ b/ulib/ml/app/ints/dune
@@ -1,41 +1,46 @@
+; NOTE: We explcitly write 'bash ./mk_int_file.sh' instead of just
+; calling the script so this works in native Windows. This is needed to
+; even build a source package in Windows, since we ship exactly this
+; dune file and script. We should consider just shipping the generated
+; ML files, if there's a convenient way to do so.
 
 ; This one is special and hand-written... sigh
 ; (rule
 ;   (target FStar_UInt8.ml)
 ;   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-;   (action (with-stdout-to %{target} (run ./mk_int_file.sh U 8))))
+;   (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 8))))
 
 (rule
   (target FStar_UInt16.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh U 16))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 16))))
 
 (rule
   (target FStar_UInt32.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh U 32))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 32))))
 
 (rule
   (target FStar_UInt64.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh U 64))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 64))))
 
 (rule
   (target FStar_Int8.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh S 8))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 8))))
 
 (rule
   (target FStar_Int16.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh S 16))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 16))))
 
 (rule
   (target FStar_Int32.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh S 32))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 32))))
 
 (rule
   (target FStar_Int64.ml)
   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
-  (action (with-stdout-to %{target} (run ./mk_int_file.sh S 64))))
+  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 64))))
diff --git a/ulib/ml/app/ints/mk_int_file.sh b/ulib/ml/app/ints/mk_int_file.sh
index 0d257da79b1..6d4f6d64c32 100755
--- a/ulib/ml/app/ints/mk_int_file.sh
+++ b/ulib/ml/app/ints/mk_int_file.sh
@@ -1,4 +1,6 @@
-#!/bin/bash
+#!/usr/bin/env bash
+
+# This script must run on Windows/Cygwin too.
 
 set -eu
 

From 1cd013aff5718b33bcc202548a567fec66e8aa96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 11:11:03 -0800
Subject: [PATCH 09/14] scripts: avoid realpath -m (not there in macos)

---
 .scripts/bin-install.sh |  7 +++----
 .scripts/package_z3.sh  |  5 ++++-
 .scripts/src-install.sh | 10 +++-------
 3 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh
index b8b3a4e4800..6ee6a98dd37 100755
--- a/.scripts/bin-install.sh
+++ b/.scripts/bin-install.sh
@@ -14,10 +14,9 @@ if [ $# -ne 1 ]; then
 	exit 1
 fi
 
-# $1 will usually exist, but mkdir it if not
-PREFIX="$(realpath -m "$1")" # -m: leading dirs allowed to not exist
-
-mkdir -p "${PREFIX}"
+PREFIX="$1"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
 
 if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then
   .scripts/package_z3.sh "$PREFIX"
diff --git a/.scripts/package_z3.sh b/.scripts/package_z3.sh
index dd4a069c6f4..16ab78deb61 100755
--- a/.scripts/package_z3.sh
+++ b/.scripts/package_z3.sh
@@ -1,6 +1,9 @@
 #!/bin/bash
 
-PREFIX="$(realpath -m "$1")" # -m: leading dirs allowed to not exist
+PREFIX="$1"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
+
 D="$(dirname "$0")"
 
 mkdir -p "$PREFIX"/lib/fstar
diff --git a/.scripts/src-install.sh b/.scripts/src-install.sh
index 49848f8a69d..3239f60c267 100755
--- a/.scripts/src-install.sh
+++ b/.scripts/src-install.sh
@@ -8,14 +8,10 @@ if [ $# -ne 2 ]; then
 fi
 
 BROOT="$(realpath "$1")"
-PREFIX="$(realpath -m "$2")" # -m: leading dirs allowed to not exist
 
-if [ -e "${PREFIX}" ]; then
-  echo "Destination directory already exists: ${PREFIX}"
-  exit 1
-fi
-
-mkdir -p "${PREFIX}"
+PREFIX="$2"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
 
 # Note: we must exclude everything in the Dune build directories, since
 # if some files "vanish" during this copy, rsync will fail (even if

From 8da0f06597e265d76d813cc8f2f3ee6a5844b4fe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 11:24:03 -0800
Subject: [PATCH 10/14] scripts: silencing some output

---
 .scripts/get_fstar_z3.sh | 12 ++++++------
 .scripts/package_z3.sh   |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.scripts/get_fstar_z3.sh b/.scripts/get_fstar_z3.sh
index 8184cac8ca6..938d9be0253 100755
--- a/.scripts/get_fstar_z3.sh
+++ b/.scripts/get_fstar_z3.sh
@@ -60,11 +60,11 @@ download_z3() {
   z3_path="${base_name%.zip}/bin/z3"
   if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi
 
-  pushd "$tmp_dir"
-  curl -L "$url" -o "$base_name"
+  pushd "$tmp_dir" > /dev/null
+  curl -s -L "$url" -o "$base_name"
 
   unzip -q "$base_name" "$z3_path"
-  popd
+  popd > /dev/null
   install -m0755 "$tmp_dir/$z3_path" "$destination_file_name"
   echo ">>> Installed Z3 $version to $destination_file_name"
 }
@@ -77,17 +77,17 @@ full_install_z3() {
   dest_dir="$3"
 
   mkdir -p "$dest_dir/z3-$version"
-  pushd "$dest_dir/z3-$version"
+  pushd "$dest_dir/z3-$version" > /dev/null
 
   echo ">>> Downloading Z3 $version from $url ..."
   base_name="$(basename "$url")"
-  curl -L "$url" -o "$base_name"
+  curl -s -L "$url" -o "$base_name"
 
   unzip -q "$base_name"
   mv "${base_name%.zip}"/* .
   rmdir "${base_name%.zip}"
   rm "$base_name"
-  popd
+  popd > /dev/null
 }
 
 usage() {
diff --git a/.scripts/package_z3.sh b/.scripts/package_z3.sh
index 16ab78deb61..f08150d9138 100755
--- a/.scripts/package_z3.sh
+++ b/.scripts/package_z3.sh
@@ -11,7 +11,7 @@ mkdir -p "$PREFIX"/lib/fstar
 TMP=$(mktemp -d)
 $D/get_fstar_z3.sh --full "$TMP"
 
-pushd "$TMP"
+pushd "$TMP" > /dev/null
 
 inst1 () {
 	TGT="$PREFIX/lib/fstar/$1"
@@ -24,6 +24,6 @@ inst1 ./z3-4.8.5/LICENSE.txt
 inst1 ./z3-4.13.3/bin/z3
 inst1 ./z3-4.13.3/LICENSE.txt
 
-popd
+popd > /dev/null
 
 rm -r "$TMP"

From 41ceb79c7f6742c3590bb6a31b63738d98a51e8e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 11:24:38 -0800
Subject: [PATCH 11/14] mk-package.sh: windows fixes (7z, paths, etc)

---
 .scripts/mk-package.sh | 95 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 85 insertions(+), 10 deletions(-)

diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh
index 401c2cdef17..1f9b7ec472b 100755
--- a/.scripts/mk-package.sh
+++ b/.scripts/mk-package.sh
@@ -1,34 +1,109 @@
 #!/bin/bash
 
+set -eu
+
 # This will just create a tar.gz or zip out of a directory.
 # You may want to look at src-install.sh and bin-install.sh
 # that generate the layouts for a source and binary package,
 # and are then packaged up with this script.
 
 if [ $# -ne 2 ]; then
-	echo "usage: $0 <install_root> <package_basename>" >&2
-	echo "Default format is tar.gz. Optionally set FSTAR_PACKAGE_FORMAT=zip to generate a zip instead." >&2
-	echo "Output filename is <package_basename> + proper extension." >&2
-	exit 1
+  exec >&2
+  echo "usage: $0 <install_root> <package_basename>"
+  echo "The archive format and command used depends on the system and installed tools,"
+  echo "see script for details."
+  echo "Optionally set FSTAR_PACKAGE_FORMAT to: "
+  echo " - 'zip': create a .zip via 'zip' command"
+  echo " - '7z': create a .zip via '7z' command"
+  echo " - 'tar.gz': create a .tar.gz, via calling"
+  echo "Output filename is <package_basename> + proper extension"
+  echo "If FSTAR_RELEASE is non-empty, we use maximum compression."
+  exit 1
 fi
 
 PREFIX="$1"
 ARCHIVE="$2"
 
+windows () {
+  [ -v OS ] && [ "$OS" = "Windows_NT" ]
+}
+
+# Computes a (hopefully) sensible default for the current system
+detect_format () {
+  if windows; then
+    # Github actions runner do not have 'zip'
+    if which zip > /dev/null; then
+      FSTAR_PACKAGE_FORMAT=zip
+    elif which 7z > /dev/null; then
+      FSTAR_PACKAGE_FORMAT=7z
+    else
+      echo "error: no zip or 7z command found." >&2
+      exit 1
+    fi
+  else
+    FSTAR_PACKAGE_FORMAT=tar.gz
+  fi
+}
+
+# If unset, pick a default for the system.
+if ! [ -v FSTAR_PACKAGE_FORMAT ]; then
+  detect_format
+fi
+
+# Fix for stupid path confustion in windows
+if windows; then
+  WRAP=$(pwd)/mk/winwrap.sh
+else
+  WRAP=
+fi
+
 case $FSTAR_PACKAGE_FORMAT in
   zip)
     TGT="$ARCHIVE.zip"
-    TGT="$(realpath "$TGT")"
-    pushd "$PREFIX"
-    zip -q -r -9 "$TGT" .
-    popd
+    ATGT="$(realpath "$TGT")"
+    pushd "$PREFIX" >/dev/null
+    LEVEL=
+    if [ -v FSTAR_RELEASE ]; then
+      LEVEL=-9
+    fi
+    $WRAP zip -q -r $LEVEL "$ATGT" .
+    popd >/dev/null
     ;;
-  tar.gz|tgz|"")
+  7z)
+    TGT="$ARCHIVE.zip"
+    ATGT="$(realpath "$TGT")"
+    LEVEL=
+    if [ -v FSTAR_RELEASE ]; then
+      LEVEL=-mx9
+    fi
+    pushd "$PREFIX" >/dev/null
+    $WRAP 7z $LEVEL a "$ATGT" .
+    popd >/dev/null
+    ;;
+  tar.gz|tgz)
     # -h: resolve symlinks
-    tar czf "$ARCHIVE.tar.gz" -h -C "$PREFIX" .
+    TGT="$ARCHIVE.tar.gz"
+    $WRAP tar cf "$ARCHIVE.tar" -h -C "$PREFIX" .
+    LEVEL=
+    if [ -v FSTAR_RELEASE ]; then
+      LEVEL=-9
+    fi
+    $WRAP gzip -f $LEVEL "$ARCHIVE.tar"
     ;;
   *)
     echo "unrecognized FSTAR_PACKAGE_FORMAT: $FSTAR_PACKAGE_FORMAT" >&2
     exit 1
     ;;
 esac
+
+if ! [ -f "$TGT" ] ; then
+  echo "error: something seems wrong, archive '$TGT' not found?" >&2
+  exit 1
+fi
+
+# bytes=$(stat -c%s "$TGT")
+# echo "Wrote $TGT" ($bytes bytes)"
+# ^ Does not work in Mac (no -c option for stat)
+
+echo "Wrote $TGT"
+ls -l "$TGT" || true

From d57a0c6af6967878fae4648a177b0f324ada5b4f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 12:44:54 -0800
Subject: [PATCH 12/14] scripts: tweak windows detection logic

---
 .scripts/bin-install.sh        | 12 ++++++++----
 .scripts/make_fstar_version.sh |  7 +++++--
 .scripts/mk-package.sh         |  6 +++++-
 3 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh
index 6ee6a98dd37..cd8571e5140 100755
--- a/.scripts/bin-install.sh
+++ b/.scripts/bin-install.sh
@@ -1,17 +1,21 @@
 #!/bin/bash
 
 # This is called by the Makefile *after* an installation into the
-# prefix, so we add the rest of the files that go into a binary pacakge.
+# prefix, so we add the rest of the files that go into a binary package.
 
 set -eu
 
 windows () {
-  [ -v OS ] && [ "$OS" = "Windows_NT" ]
+  # This seems portable enough and does not trigger an
+  # undefined variable error (see set -u above) if $OS
+  # is unset (like in linux/mac). Note: OSX's bash is usually
+  # old and does not support '[ -v OS ]'.
+  [[ "${OS:-}" = "Windows_NT" ]]
 }
 
 if [ $# -ne 1 ]; then
-	echo "Usage: $0 <prefix>" >&2
-	exit 1
+  echo "Usage: $0 <prefix>" >&2
+  exit 1
 fi
 
 PREFIX="$1"
diff --git a/.scripts/make_fstar_version.sh b/.scripts/make_fstar_version.sh
index d4ebe49b567..e47448b6a36 100755
--- a/.scripts/make_fstar_version.sh
+++ b/.scripts/make_fstar_version.sh
@@ -1,11 +1,14 @@
 #!/usr/bin/env bash
 
+windows () {
+  [[ "${OS:-}" = "Windows_NT" ]]
+}
+
 if [[ -z "$FSTAR_VERSION" ]]; then
   FSTAR_VERSION=$(head -n 1 version.txt)~dev
 fi
 
-if [ "$OS" = "Windows_NT" ]
-then
+if windows; then
    if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" ]
    then
      PLATFORM="Windows_x64"
diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh
index 1f9b7ec472b..7d37bed1062 100755
--- a/.scripts/mk-package.sh
+++ b/.scripts/mk-package.sh
@@ -25,7 +25,11 @@ PREFIX="$1"
 ARCHIVE="$2"
 
 windows () {
-  [ -v OS ] && [ "$OS" = "Windows_NT" ]
+  # This seems portable enough and does not trigger an
+  # undefined variable error (see set -u above) if $OS
+  # is unset (like in linux/mac). Note: OSX's bash is usually
+  # old and does not support '[ -v OS ]'.
+  [[ "${OS:-}" = "Windows_NT" ]]
 }
 
 # Computes a (hopefully) sensible default for the current system

From cac389a84df792a8071caa66c3818192e6051078 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 11:58:59 -0800
Subject: [PATCH 13/14] release: use higher compression

---
 .github/workflows/build-linux.yml |  1 +
 .github/workflows/build-macos.yml |  1 +
 .scripts/mk-package.sh            | 10 +++++++---
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml
index 3da91037e01..879d07bec20 100644
--- a/.github/workflows/build-linux.yml
+++ b/.github/workflows/build-linux.yml
@@ -37,6 +37,7 @@ jobs:
             echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
           elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
             echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+            echo FSTAR_RELEASE=1 >> $GITHUB_ENV
           fi
 
       # NB: release workflow later adds version number to the name
diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
index 6c9863cc302..4a9d2748e00 100644
--- a/.github/workflows/build-macos.yml
+++ b/.github/workflows/build-macos.yml
@@ -29,6 +29,7 @@ jobs:
             echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
           elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
             echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+            echo FSTAR_RELEASE=1 >> $GITHUB_ENV
           fi
 
       # Note *g*make below!
diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh
index 7d37bed1062..7a02148b960 100755
--- a/.scripts/mk-package.sh
+++ b/.scripts/mk-package.sh
@@ -32,6 +32,10 @@ windows () {
   [[ "${OS:-}" = "Windows_NT" ]]
 }
 
+release () {
+  [[ -n "${FSTAR_RELEASE:-}" ]]
+}
+
 # Computes a (hopefully) sensible default for the current system
 detect_format () {
   if windows; then
@@ -67,7 +71,7 @@ case $FSTAR_PACKAGE_FORMAT in
     ATGT="$(realpath "$TGT")"
     pushd "$PREFIX" >/dev/null
     LEVEL=
-    if [ -v FSTAR_RELEASE ]; then
+    if release; then
       LEVEL=-9
     fi
     $WRAP zip -q -r $LEVEL "$ATGT" .
@@ -77,7 +81,7 @@ case $FSTAR_PACKAGE_FORMAT in
     TGT="$ARCHIVE.zip"
     ATGT="$(realpath "$TGT")"
     LEVEL=
-    if [ -v FSTAR_RELEASE ]; then
+    if release; then
       LEVEL=-mx9
     fi
     pushd "$PREFIX" >/dev/null
@@ -89,7 +93,7 @@ case $FSTAR_PACKAGE_FORMAT in
     TGT="$ARCHIVE.tar.gz"
     $WRAP tar cf "$ARCHIVE.tar" -h -C "$PREFIX" .
     LEVEL=
-    if [ -v FSTAR_RELEASE ]; then
+    if release; then
       LEVEL=-9
     fi
     $WRAP gzip -f $LEVEL "$ARCHIVE.tar"

From f980983e75b3cc8c8c25fe2ccf294fdf4792fa86 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sat, 11 Jan 2025 13:11:14 -0800
Subject: [PATCH 14/14] ci: nits

---
 .github/workflows/build-linux.yml | 6 ++++--
 .github/workflows/build-macos.yml | 5 +++--
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml
index 879d07bec20..da2fc110b31 100644
--- a/.github/workflows/build-linux.yml
+++ b/.github/workflows/build-linux.yml
@@ -12,7 +12,7 @@ defaults:
     shell: bash
 
 jobs:
-  build:
+  build-linux:
     runs-on: ubuntu-22.04
     # We prefer slightly older Ubuntu so we get binaries that work on
     # all more recent versions.
@@ -46,8 +46,10 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
-          make -skj$(nproc) package     FSTAR_TAG=-$KERNEL-$ARCH
+          export FSTAR_TAG=-$KERNEL-$ARCH
+          make -skj$(nproc) package
           make -skj$(nproc) package-src FSTAR_TAG=
+          # ^ no tag in source package
 
       - uses: actions/upload-artifact@v4
         with:
diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
index 4a9d2748e00..c943f9995f2 100644
--- a/.github/workflows/build-macos.yml
+++ b/.github/workflows/build-macos.yml
@@ -5,7 +5,7 @@ on:
   workflow_call:
 
 jobs:
-  build:
+  build-macos:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@master
@@ -39,7 +39,8 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
-          gmake -skj$(nproc) package FSTAR_TAG=-$KERNEL-$ARCH
+          export FSTAR_TAG=-$KERNEL-$ARCH
+          gmake -skj$(nproc) package
 
       - uses: actions/upload-artifact@v4
         with: