Print version/kernel on fstar.exe -d output

mtzguido · Feb 7, 2025 · ddeccf5 · ddeccf5
1 parent 9312745
commit ddeccf5
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -11,6 +11,7 @@
     dynlink
     menhirLib
     pprint
+    process
     sedlex
     mtime.clock.os
  )
-Original file line number
+Diff line change
@@ Expand Up / @@ -11,6 +11,7 @@ @@
         dynlink
         menhirLib
         pprint
+        process
         sedlex
         mtime.clock.os
      )
@@ Expand Down @@