Merge branch 'master' into unfold_once

FStarLang · Jan 13, 2025 · 1f2e2d9 · 1f2e2d9
2 parents 5fcd56d + 7ff2d93
commit 1f2e2d9
Showing 1 changed file with 14 additions and 4 deletions.
diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst
@@ -204,7 +204,7 @@ let defaults =
       ("eager_subtyping"              , Bool false);
       ("error_contexts"               , Bool false);
       ("expose_interfaces"            , Bool false);
-      ("message_format"               , String "human");
+      ("message_format"               , String "auto");
       ("ext"                          , Unset);
       ("extract"                      , Unset);
       ("extract_all"                  , Bool false);
@@ -991,8 +991,10 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
 
   ( noshort,
     "message_format",
-    EnumStr ["human"; "json"; "github"],
-    text "Format of the messages emitted by F* (default `human`)");
+    EnumStr ["human"; "json"; "github"; "auto"],
+    text "Format of the messages emitted by F*. Using 'auto' will use human messages \
+          unless the variable GITHUB_ACTIONS is non-empty, in which case 'github' is \
+          used (default `auto`).");
 
   ( noshort,
     "hide_uvar_nums",
@@ -1993,8 +1995,17 @@ let dump_module                  s  = get_dump_module() |> List.existsb (module_
 let eager_subtyping              () = get_eager_subtyping()
 let error_contexts               () = get_error_contexts              ()
 let expose_interfaces            () = get_expose_interfaces          ()
+let interactive                  () = get_in () || get_ide () || get_lsp ()
 let message_format               () =
   match get_message_format () with
+  | "auto" -> (
+    if interactive () then Human
+    else
+    match Util.expand_environment_variable "GITHUB_ACTIONS" with
+    | None
+    | Some "" -> Human
+    | Some _ -> Github
+  )
   | "human" -> Human
   | "json" -> Json
   | "github" -> Github
@@ -2033,7 +2044,6 @@ let print                        () = get_print                       ()
 let print_in_place               () = get_print_in_place              ()
 let initial_fuel                 () = min (get_initial_fuel ()) (get_max_fuel ())
 let initial_ifuel                () = min (get_initial_ifuel ()) (get_max_ifuel ())
-let interactive                  () = get_in () || get_ide () || get_lsp ()
 let lax                          () = get_lax                         ()
 let load                         () = get_load                        ()
 let load_cmxs                    () = get_load_cmxs                   ()