From f6dcfcf158cc41e15440de05a7b76f21bfa30bbc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 10:54:33 -0800
Subject: [PATCH 1/6] Makefile: remove use of undefine (GNU only)

---
 Makefile | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Makefile b/Makefile
index f7b7c61b0ec..e5c298cb14c 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,6 @@ export FSTAR_ROOT=$(CURDIR)
 # ^ This variable is only used by internal makefiles.
 # Do NOT rely on it in client code. It is not what FSTAR_HOME was.
 include mk/common.mk
-undefine FSTAR_EXE # just in case
 
 # NOTE: If you are changing any of install rules, run a macos build too.
 # The behavior of cp, find, etc, can differ in subtle ways from that of GNU tools.

From 0d74b5d8311a124efa86bfbce3d76d8b30a88e75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 14:57:27 -0800
Subject: [PATCH 2/6] ci: testing binary packages

---
 .github/workflows/build-linux.yml | 27 +++++++++++++++++++++++++++
 .github/workflows/build-macos.yml | 30 +++++++++++++++++++++++++++++-
 .github/workflows/tests.yml       | 19 +++----------------
 3 files changed, 59 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml
index e1bd9192ddd..131ffa59eeb 100644
--- a/.github/workflows/build-linux.yml
+++ b/.github/workflows/build-linux.yml
@@ -60,3 +60,30 @@ jobs:
       #   with:
       #     path: fstar-src.tar.gz
       #     name: package-src
+
+  smoke_test:
+    needs: build
+    strategy:
+      matrix:
+        os:
+          - ubuntu-22.04
+          - ubuntu-24.04
+          - ubuntu-latest
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: cda-tum/setup-z3@main
+        with:
+          version: 4.8.5
+
+      - name: Get fstar package
+        uses: actions/download-artifact@v4
+        with:
+          name: package-linux
+
+      - run: tar xzf fstar*.tar.gz
+
+      - name: Smoke test
+        run: |
+          ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
+          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          ./fstar/bin/fstar.exe A.fst
diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
index 9049c4ac502..ef32d78b511 100644
--- a/.github/workflows/build-macos.yml
+++ b/.github/workflows/build-macos.yml
@@ -6,7 +6,7 @@ on:
 
 jobs:
   build:
-    runs-on: macos-latest
+    runs-on: macos-14
     steps:
       - uses: actions/checkout@master
 
@@ -46,3 +46,31 @@ jobs:
         with:
           path: fstar-*
           name: package-mac
+
+  smoke_test:
+    needs: build
+    strategy:
+      matrix:
+        os:
+          - macos-14
+          - macos-15
+          - macos-latest
+    runs-on: ${{ matrix.os }}
+    steps:
+      # no 4.8.5 on mac, could call script but just admit.
+      # - uses: cda-tum/setup-z3@main
+      #   with:
+      #     version: 4.8.5
+
+      - name: Get fstar package
+        uses: actions/download-artifact@v4
+        with:
+          name: package-mac
+
+      - run: tar xzf fstar*.tar.gz
+
+      - name: Smoke test
+        run: |
+          ./fstar/bin/fstar.exe --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
+          echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
+          ./fstar/bin/fstar.exe --admit_smt_queries true A.fst
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
index 19c6b404ee4..5c766d4cf99 100644
--- a/.github/workflows/tests.yml
+++ b/.github/workflows/tests.yml
@@ -77,20 +77,7 @@ jobs:
         run: make -skj$(nproc) _test
 
   binary-smoke:
-    strategy:
-      matrix:
-        pak:
-          - fstar.tar.gz
-          # - fstar-stage1.tar.gz
-          # ^ See note in test-local.
-        os:
-          # - ubuntu-20.04
-          # - ubuntu-22.04
-          - ubuntu-24.04
-          # - ubuntu-latest
-          # FIXME: the container builds with a recent glibc, use an older
-          # base system to get a more portable executable.
-    runs-on: ${{ matrix.os }}
+    runs-on: ubuntu-24.04
     steps:
       - uses: cda-tum/setup-z3@main
         with:
@@ -99,9 +86,9 @@ jobs:
       - name: Get fstar package
         uses: actions/download-artifact@v4
         with:
-          name: ${{ matrix.pak }}
+          name: fstar.tar.gz
 
-      - run: tar xzf ${{ matrix.pak }}
+      - run: tar xzf fstar.tar.gz
 
       - name: Smoke test
         run: |

From 0cc39d885a2afd644655abd3bf8cc530ed1456ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 15:07:51 -0800
Subject: [PATCH 3/6] stage.mk: cleaning lib before intasll

If lib/fstar/ulib already exists, we will ulib into it, instead
of overwriting it. Just remove it beforehand. We should own
$(PREFIX)/lib/fstar.
---
 mk/stage.mk | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/mk/stage.mk b/mk/stage.mk
index 69bda327317..eca3a265fe0 100644
--- a/mk/stage.mk
+++ b/mk/stage.mk
@@ -47,7 +47,7 @@ clean: _force
 # In a local build, we prefer to symlink the library and checked file
 # directories to get better IDE integration, but of course we cannot do
 # that on actual install, and must copy all files. Note: this flag is
-# also only set by the parent Makefile on Lonux, since Mac's ln does not
+# also only set by the parent Makefile on Linux, since Mac's ln does not
 # support the same options.
 ifeq ($(FSTAR_LINK_LIBDIRS),1)
 INSTALL_DIR := ln -Tsrf
@@ -69,7 +69,9 @@ install: # NOTE: no deps, dune figures it out and rebuilds if needed
 	cd dune && $(DUNE) build $(FSTAR_DUNE_BUILD_OPTIONS)
 	cd dune && $(DUNE) install $(FSTAR_DUNE_OPTIONS) --prefix=$(PREFIX)
 	@# Install library and its checked files
+	rm -rf $(PREFIX)/lib/fstar/ulib
 	$(INSTALL_DIR) ulib $(PREFIX)/lib/fstar/ulib
+	rm -rf $(PREFIX)/lib/fstar/ulib.checked
 	$(INSTALL_DIR) ulib.checked $(PREFIX)/lib/fstar/ulib.checked
 	echo 'ulib'          > $(PREFIX)/lib/fstar/fstar.include
 	echo 'ulib.checked' >> $(PREFIX)/lib/fstar/fstar.include

From 93127451d38847fe073992bea49a357a51853eff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 10:27:20 -0800
Subject: [PATCH 4/6] FStarC.Platform: some refactoring

---
 src/basic/FStarC.Platform.Base.fsti |  8 ++++++++
 src/basic/FStarC.Platform.fst       | 26 ++++++++++++++++++++++++++
 src/basic/FStarC.Platform.fsti      | 23 +++++++++++++++++------
 src/basic/FStarC.Plugins.fst        |  6 +-----
 src/class/FStarC.Class.Show.fst     | 14 ++++++++++++--
 src/fstar/FStarC.OCaml.fst          |  6 +-----
 src/ml/FStarC_Platform.ml           | 17 -----------------
 src/ml/FStarC_Platform_Base.ml      | 11 +++++++++++
 src/ml/FStarC_Util.ml               |  4 ++--
 src/parser/FStarC.Parser.Dep.fst    |  2 +-
 stage1/dune/main.ml                 |  2 +-
 stage2/dune/main.ml                 |  2 +-
 12 files changed, 81 insertions(+), 40 deletions(-)
 create mode 100644 src/basic/FStarC.Platform.Base.fsti
 create mode 100644 src/basic/FStarC.Platform.fst
 delete mode 100644 src/ml/FStarC_Platform.ml
 create mode 100644 src/ml/FStarC_Platform_Base.ml

diff --git a/src/basic/FStarC.Platform.Base.fsti b/src/basic/FStarC.Platform.Base.fsti
new file mode 100644
index 00000000000..79dd81543a7
--- /dev/null
+++ b/src/basic/FStarC.Platform.Base.fsti
@@ -0,0 +1,8 @@
+module FStarC.Platform.Base
+
+type sys =
+  | Unix
+  | Win32
+  | Cygwin
+
+val system : sys
diff --git a/src/basic/FStarC.Platform.fst b/src/basic/FStarC.Platform.fst
new file mode 100644
index 00000000000..7ffb1c2e1af
--- /dev/null
+++ b/src/basic/FStarC.Platform.fst
@@ -0,0 +1,26 @@
+module FStarC.Platform
+
+open FStarC.Effect
+open FStarC.Platform.Base
+
+instance showable_sys : showable sys = {
+  show = (function
+          | Unix -> "Unix"
+          | Win32 -> "Win32"
+          | Cygwin -> "Cygwin");
+}
+
+let windows =
+  system = Win32
+
+let cygwin =
+  system = Cygwin
+
+let unix =
+  system = Unix || system = Cygwin
+
+let exe s =
+  if windows then s ^ ".exe" else s
+
+let ocamlpath_sep =
+  if windows then ";" else ":"
diff --git a/src/basic/FStarC.Platform.fsti b/src/basic/FStarC.Platform.fsti
index 1e8b79b5be5..af1105e8dc8 100644
--- a/src/basic/FStarC.Platform.fsti
+++ b/src/basic/FStarC.Platform.fsti
@@ -1,12 +1,23 @@
 module FStarC.Platform
+
 open FStarC.Effect
+include FStarC.Platform.Base
+
+open FStarC.Class.Show
+instance val showable_sys : showable sys
+
+(* Running on Windows (not cygwin) *)
+val windows : bool
+
+(* Running on Cygwin. *)
+val cygwin : bool
 
-type sys =
-| Windows
-| Posix
+(* Running on a unix-like system *)
+val unix : bool
 
-val system : sys
+(* Executable name for this platform, currently
+just appends '.exe' on Windows. *)
 val exe : string -> string
 
-(* true when we are running in Cygwin. Note: system will return 'Windows' in this case *)
-val is_cygwin : bool
+(* String used to separate paths in the OCAMLPATH environment variable. *)
+val ocamlpath_sep : string
diff --git a/src/basic/FStarC.Plugins.fst b/src/basic/FStarC.Plugins.fst
index d21c88f5bc8..6a994b927ee 100644
--- a/src/basic/FStarC.Plugins.fst
+++ b/src/basic/FStarC.Plugins.fst
@@ -88,10 +88,6 @@ let compile_modules dir ms =
                 @ (List.map pkg packages)
                 @ ["-o"; m ^ ".cmxs"; m ^ ".ml"] in
      (* Note: not useful when in an OPAM setting *)
-     let ocamlpath_sep = match Platform.system with
-       | Platform.Windows -> ";"
-       | Platform.Posix -> ":"
-     in
      let old_ocamlpath =
        match BU.expand_environment_variable "OCAMLPATH" with
        | Some s -> s
@@ -99,7 +95,7 @@ let compile_modules dir ms =
      in
      let env_setter = BU.format3 "env OCAMLPATH=\"%s%s%s\""
        (Find.locate_ocaml ())
-       ocamlpath_sep
+       Platform.ocamlpath_sep
       //  Options.fstar_bin_directory // needed?
       //  ocamlpath_sep
        old_ocamlpath
diff --git a/src/class/FStarC.Class.Show.fst b/src/class/FStarC.Class.Show.fst
index a36b1703648..22859ee55e3 100644
--- a/src/class/FStarC.Class.Show.fst
+++ b/src/class/FStarC.Class.Show.fst
@@ -28,11 +28,21 @@ instance showable_string : showable string =
 }
 
 instance show_list (a:Type) (_ : showable a) : Tot (showable (list a)) = {
-  show = FStarC.Common.string_of_list show;
+  show =
+    (fun l ->
+      let rec show_list_aux = (fun l ->
+        match l with
+        | [] -> ""
+        | [x] -> show x
+        | x::xs -> show x ^ ", " ^ show_list_aux xs
+      ) in
+      "[" ^ show_list_aux l ^ "]"
+    );
 }
 
 instance show_option (a:Type) (_ : showable a) : Tot (showable (option a)) = {
-  show = FStarC.Common.string_of_option show;
+  show = (function None -> "None"
+                 | Some x -> "Some " ^ show x);
 }
 
 instance show_either
diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst
index d455fbcc70c..f3d48c2923a 100644
--- a/src/fstar/FStarC.OCaml.fst
+++ b/src/fstar/FStarC.OCaml.fst
@@ -30,12 +30,8 @@ let shellescape (s:string) : string =
 
 let new_ocamlpath () : string =
   let ocamldir = Find.locate_ocaml () in
-  let sep = match Platform.system with
-    | Platform.Windows -> ";"
-    | Platform.Posix -> ":"
-  in
   let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in
-  let new_ocamlpath = ocamldir ^ sep ^ old_ocamlpath in
+  let new_ocamlpath = ocamldir ^ Platform.ocamlpath_sep ^ old_ocamlpath in
   new_ocamlpath
 
 let exec_in_ocamlenv #a (cmd : string) (args : list string) : a =
diff --git a/src/ml/FStarC_Platform.ml b/src/ml/FStarC_Platform.ml
deleted file mode 100644
index c337ad1405e..00000000000
--- a/src/ml/FStarC_Platform.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-type sys =
-| Windows
-| Posix
-
-let system =
- if Sys.win32 || Sys.cygwin then
-     Windows
- else
-     Posix
-
-let exe name =
-  if Sys.unix then
-    name
-  else
-    name^".exe"
-
-let is_cygwin = Sys.cygwin
diff --git a/src/ml/FStarC_Platform_Base.ml b/src/ml/FStarC_Platform_Base.ml
new file mode 100644
index 00000000000..15e6f21de67
--- /dev/null
+++ b/src/ml/FStarC_Platform_Base.ml
@@ -0,0 +1,11 @@
+type sys =
+  | Unix
+  | Win32
+  | Cygwin
+
+let system =
+  match Sys.os_type with
+  | "Unix" -> Unix
+  | "Win32" -> Win32
+  | "Cygwin" -> Cygwin
+  | s -> failwith ("Unrecognized system: " ^ s)
diff --git a/src/ml/FStarC_Util.ml b/src/ml/FStarC_Util.ml
index 468add9dd96..e19e022192b 100644
--- a/src/ml/FStarC_Util.ml
+++ b/src/ml/FStarC_Util.ml
@@ -192,7 +192,7 @@ let kill_process (p: proc) =
          get ESRCH. On Windows, we apparently get EACCES (permission denied). *)
       (try Unix.kill p.pid Sys.sigkill
        with Unix.Unix_error (Unix.ESRCH, _, _) -> ()
-          | Unix.Unix_error (Unix.EACCES, _, _) when FStarC_Platform.system = FStarC_Platform.Windows -> ()
+          | Unix.Unix_error (Unix.EACCES, _, _) when FStarC_Platform.windows -> ()
           ); 
 
       (* Avoid zombie processes (Unix.close_process does the same thing. *)
@@ -349,7 +349,7 @@ let get_file_extension (fn:string) : string = snd (BatString.rsplit fn ".")
 
 (* NOTE: Working around https://github.com/ocaml-batteries-team/batteries-included/issues/1136 *)
 let is_absolute_windows (path_str : string) : bool =
-  if FStarC_Platform.system = FStarC_Platform.Windows then
+  if FStarC_Platform.windows then
     match BatString.to_list path_str with
     | '\\' :: _ -> true
     | letter :: ':' :: '\\' :: _ -> BatChar.is_letter letter
diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst
index a76fb45cb8b..b52a3d56be9 100644
--- a/src/parser/FStarC.Parser.Dep.fst
+++ b/src/parser/FStarC.Parser.Dep.fst
@@ -127,7 +127,7 @@ let module_name_of_file f =
     | None ->
       raise_error0 Errors.Fatal_NotValidFStarFile (
         [ text <| Util.format1 "Not a valid FStar file: '%s'" f; ] @
-        (if Platform.system = Platform.Windows && f = ".." then [
+        (if Platform.windows && f = ".." then [
           text <| "Note: In Windows-compiled versions of F*, a literal
           asterisk as argument will be expanded to a list of files,
           **even if quoted**. It is possible you provided such an
diff --git a/stage1/dune/main.ml b/stage1/dune/main.ml
index 43d25ac5234..7dd2f108948 100644
--- a/stage1/dune/main.ml
+++ b/stage1/dune/main.ml
@@ -4,7 +4,7 @@ let x =
          by default will terminate F*, and we won't get an exception
          or anything. So, block them, and instead rely on OCaml exceptions
          to detect this. *)
-      if Fstarcompiler.FStarC_Platform.system = Posix then
+      if Fstarcompiler.FStarC_Platform.unix then
         ignore (Unix.sigprocmask Unix.SIG_BLOCK [Sys.sigpipe]);
 
       (* Enable memtrace, only if the environment variable MEMTRACE is set. *)
diff --git a/stage2/dune/main.ml b/stage2/dune/main.ml
index 43d25ac5234..7dd2f108948 100644
--- a/stage2/dune/main.ml
+++ b/stage2/dune/main.ml
@@ -4,7 +4,7 @@ let x =
          by default will terminate F*, and we won't get an exception
          or anything. So, block them, and instead rely on OCaml exceptions
          to detect this. *)
-      if Fstarcompiler.FStarC_Platform.system = Posix then
+      if Fstarcompiler.FStarC_Platform.unix then
         ignore (Unix.sigprocmask Unix.SIG_BLOCK [Sys.sigpipe]);
 
       (* Enable memtrace, only if the environment variable MEMTRACE is set. *)

From ddeccf50649b6555bbd92639ccb80b874bb8ca8e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 14:49:26 -0800
Subject: [PATCH 5/6] Print version/kernel on fstar.exe -d output

---
 src/basic/FStarC.Platform.Base.fsti | 5 +++++
 src/fstar/FStarC.Main.fst           | 5 +++--
 src/ml/FStarC_Platform_Base.ml      | 6 ++++++
 stage1/dune/fstar-guts/dune         | 1 +
 stage2/dune/fstar-guts/dune         | 1 +
 5 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/basic/FStarC.Platform.Base.fsti b/src/basic/FStarC.Platform.Base.fsti
index 79dd81543a7..27219da1ffb 100644
--- a/src/basic/FStarC.Platform.Base.fsti
+++ b/src/basic/FStarC.Platform.Base.fsti
@@ -1,8 +1,13 @@
 module FStarC.Platform.Base
 
+open FStarC.Effect
+
 type sys =
   | Unix
   | Win32
   | Cygwin
 
 val system : sys
+
+(* Tries to read the output of the `uname` command. *)
+val kernel () : string
diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst
index ba78883d7da..29bf51e8924 100644
--- a/src/fstar/FStarC.Main.fst
+++ b/src/fstar/FStarC.Main.fst
@@ -266,8 +266,9 @@ let go_normal () =
       fstar_files := Some filenames;
 
       if Debug.any () then (
-        Util.print1 "- F* executable: %s\n" (Util.exec_name);
-        Util.print1 "- Library root: %s\n" ((Util.dflt "<none>" (Find.lib_root ())));
+        Util.print3 "- F* version %s -- %s (on %s)\n"  !Options._version !Options._commit (Platform.kernel ());
+        Util.print1 "- Executable: %s\n" (Util.exec_name);
+        Util.print1 "- Library root: %s\n" (Util.dflt "<none>" (Find.lib_root ()));
         Util.print1 "- Full include path: %s\n" (show (Find.include_path ()));
         Util.print_string "\n";
         ()
diff --git a/src/ml/FStarC_Platform_Base.ml b/src/ml/FStarC_Platform_Base.ml
index 15e6f21de67..712a61f7882 100644
--- a/src/ml/FStarC_Platform_Base.ml
+++ b/src/ml/FStarC_Platform_Base.ml
@@ -9,3 +9,9 @@ let system =
   | "Win32" -> Win32
   | "Cygwin" -> Cygwin
   | s -> failwith ("Unrecognized system: " ^ s)
+
+let kernel () : string =
+  try
+    List.hd (Process.read_stdout "uname" [| |])
+  with
+  | _ -> Sys.os_type
diff --git a/stage1/dune/fstar-guts/dune b/stage1/dune/fstar-guts/dune
index 5162865f29e..a2c4f8f81cf 100644
--- a/stage1/dune/fstar-guts/dune
+++ b/stage1/dune/fstar-guts/dune
@@ -11,6 +11,7 @@
     dynlink
     menhirLib
     pprint
+    process
     sedlex
     mtime.clock.os
  )
diff --git a/stage2/dune/fstar-guts/dune b/stage2/dune/fstar-guts/dune
index 5162865f29e..a2c4f8f81cf 100644
--- a/stage2/dune/fstar-guts/dune
+++ b/stage2/dune/fstar-guts/dune
@@ -11,6 +11,7 @@
     dynlink
     menhirLib
     pprint
+    process
     sedlex
     mtime.clock.os
  )

From 9dd08acd614cdbbb3e25995c4f9ff86608e43725 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Thu, 6 Feb 2025 17:07:42 -0800
Subject: [PATCH 6/6] Reduce verbosity

---
 src/fstar/FStarC.Main.fst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst
index 29bf51e8924..ea3d9ed48b2 100644
--- a/src/fstar/FStarC.Main.fst
+++ b/src/fstar/FStarC.Main.fst
@@ -95,9 +95,8 @@ let load_native_tactics () =
                 | Some f -> f
               end
     in
+
     let cmxs_files = (modules_to_load@cmxs_to_load) |> List.map cmxs_file in
-    if Debug.any () then
-      Util.print1 "Will try to load cmxs files: [%s]\n" (String.concat ", " cmxs_files);
     Plugins.load_plugins cmxs_files;
     iter_opt (Options.use_native_tactics ())
       Plugins.load_plugins_dir;