Driver: special-case -cc msvc to call script

Starting from cl.exe seems hopeless
FStarLang · Feb 12, 2025 · eb642ae · eb642ae
1 parent 8aa1ab7
commit eb642ae
Showing 1 changed file with 39 additions and 34 deletions.
diff --git a/lib/Driver.ml b/lib/Driver.ml
@@ -391,27 +391,11 @@ let fill_cc_args () =
     @ List.rev !Options.ccopts
     @ !cc_args
 
-let detect_cc () =
-  detect_base_tools_if ();
-
-  if not !Options.silent then
-    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
-
-  (* Use Options.cc if passed, otherwise CC from env, otherwise "cc" *)
-  let cc_name =
-    if !Options.cc <> ""
-    then !Options.cc
-    else
-      match Sys.getenv "CC" with
-      | s -> s
-      | exception _ -> "cc"
-  in
-
-  (* cc_name can be relative or absolute, `which` handles both. *)
-  if not (success "which" [| cc_name |]) then
-    Warn.fatal_error "C compiler '%s' not found!" cc_name;
-
-  cc := cc_name;
+(* Sets cc, cc_flavor *)
+let auto_detect_cc () =
+  (* !cc can be relative or absolute, `which` handles both. *)
+  if not (success "which" [| !cc |]) then
+    Warn.fatal_error "C compiler '%s' not found!" !cc;
 
   if not !Options.silent then begin
     (* If not absolute print realpath too *)
@@ -427,24 +411,45 @@ let detect_cc () =
     in
     KPrint.bprintf "%scc is:%s %s%s\n" Ansi.underline Ansi.reset !cc real
   end;
+  match !Options.cc_flavor with
+  | Some f -> cc_flavor := f
+  | None ->   cc_flavor := detect_compiler_flavor !cc
 
-  begin
-    match !Options.cc_flavor with
-    | Some f -> cc_flavor := f
-    | None ->   cc_flavor := detect_compiler_flavor !cc
-  end;
+let detect_cc () =
+  detect_base_tools_if ();
+
+  if not !Options.silent then
+    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
+
+  (* Use Options.cc if passed, otherwise CC from env, otherwise "cc" *)
+  let cc_name =
+    if !Options.cc <> ""
+    then !Options.cc
+    else
+      match Sys.getenv "CC" with
+      | s -> s
+      | exception _ -> "cc"
+  in
+
+  if cc_name = "msvc" then (
+    (* We special-case "msvc" and use this wrapper script to find it
+       and set its environment up, it's not really feasible to
+       just find the cl.exe *)
+    KPrint.bprintf "%scc is:%s MSVC (will use cl-wrapper script)\n" Ansi.underline Ansi.reset;
+    cc := !misc_dir ^^ "cl-wrapper.bat";
+    cc_flavor := MSVC
+  ) else (
+    (* Otherwise cc_name is a normal command or path like gcc/clang,
+       auto-detect its flavor. *)
+    cc := cc_name;
+    auto_detect_cc ()
+  );
 
   if not !Options.silent then
     KPrint.bprintf "%scc flavor is:%s %s\n" Ansi.underline Ansi.reset
       (Options.string_of_compiler_flavor !cc_flavor);
 
-  (* For MSVC, we need to use the wrapper. *)
-  if !cc_flavor = MSVC then begin
-    (* FIXME: Can we make the script use the cc we've set up? *)
-    cc := !misc_dir ^^ "cl-wrapper.bat"
-  end;
-
-  (* Now that we detected the flavor , call this callback to
+  (* Now that we detected the flavor, call this callback to
      right default arguments for the compiler filled in. *)
   !cc_flavor_callback !cc_flavor;
 
@@ -454,7 +459,7 @@ let detect_cc () =
     cc_args := "-m32" :: !cc_args;
 
   if not !Options.silent then
-    KPrint.bprintf "%s%s options are:%s %s\n" Ansi.underline !cc Ansi.reset
+    KPrint.bprintf "%scc options are:%s %s\n" Ansi.underline Ansi.reset
       (String.concat " " !cc_args)
 
 let detect_cc_if () =