Makefile/package fixes

.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

.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

.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: |

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.

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

src/basic/FStarC.Platform.Base.fsti

@@ -0,0 +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

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 ":"

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

src/basic/FStarC.Plugins.fst

@@ -88,18 +88,14 @@ 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
        | None -> ""
      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

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

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;
@@ -266,8 +265,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";
         ()

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 =

src/ml/FStarC_Platform_Base.ml

@@ -0,0 +1,17 @@
+type sys =
+  | Unix
+  | Win32
+  | Cygwin
+
+let system =
+  match Sys.os_type with
+  | "Unix" -> Unix
+  | "Win32" -> Win32
+  | "Cygwin" -> Cygwin
+  | s -> failwith ("Unrecognized system: " ^ s)
+
+let kernel () : string =
+  try
+    List.hd (Process.read_stdout "uname" [| |])
+  with
+  | _ -> Sys.os_type

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

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

stage1/dune/fstar-guts/dune

@@ -11,6 +11,7 @@
     dynlink
     menhirLib
     pprint
+    process
     sedlex
     mtime.clock.os
  )

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

stage2/dune/fstar-guts/dune

@@ -11,6 +11,7 @@
     dynlink
     menhirLib
     pprint
+    process
     sedlex
     mtime.clock.os
  )

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