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] 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
  )