Merge pull request #3701 from mtzguido/misc

Misc patches for error reporting

src/basic/FStarC.Options.fst

@@ -33,6 +33,8 @@ module FC = FStarC.Common
 module Util = FStarC.Util
 module List = FStarC.List
 
+exception NotSettable of string
+
 module Ext = FStarC.Options.Ext
 
 let debug_embedding = mk_ref false
@@ -1785,7 +1787,19 @@ let all_specs = specs true
 let all_specs_getopt = List.map fst all_specs
 
 let all_specs_with_types = specs_with_types true
-let settable_specs = all_specs |> List.filter (fun ((_, x, _), _) -> settable x)
+let settable_specs =
+  all_specs |>
+  List.map (fun spec ->
+    let ((c, x, h), doc) = spec in
+    if settable x
+    then spec
+    else
+      let h' = match h with
+               | ZeroArgs _ -> ZeroArgs (fun () -> raise (NotSettable x))
+               | OneArg (_, k) -> OneArg ((fun s -> raise (NotSettable x)), k)
+      in
+      ((c, x, h'), doc)
+  )
 
 let help_for_option (s:string) : option Pprint.document =
   match all_specs |> List.filter (fun ((_, x, _), _) -> x = s) with

src/basic/FStarC.Options.fsti

@@ -21,6 +21,10 @@ open FStarC.BaseTypes
 open FStarC.VConfig
 open FStarC
 
+(* Raised when a processing a pragma an a non-settable option
+appears there. *)
+exception NotSettable of string
+
 type codegen_t =
   | OCaml
   | FSharp

src/fstar/FStarC.Main.fst

@@ -44,10 +44,6 @@ open FStarC.Reflection.V2.Interpreter {}
 let process_args () : parse_cmdline_res & list string =
   Options.parse_cmd_line ()
 
-(* cleanup: kills background Z3 processes; relevant when --n_cores > 1 *)
-(* GM: unclear if it's useful now? *)
-let cleanup () = Util.kill_all ()
-
 (* printing a finished message *)
 let finished_message fmods errs =
   let print_to = if errs > 0 then Util.print_error else Util.print_string in
@@ -350,14 +346,17 @@ let go () =
     OCaml.exec_ocamlopt_plugin rest
 
   | _ -> go_normal ()
+
 let handle_error e =
     if FStarC.Errors.handleable e then
-      FStarC.Errors.err_exn e;
-    if Options.trace_error() then
-      Util.print2_error "Unexpected error\n%s\n%s\n" (Util.message_of_exn e) (Util.trace_of_exn e)
-    else if not (FStarC.Errors.handleable e) then
-      Util.print1_error "Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.\n%s\n" (Util.message_of_exn e);
-    cleanup();
+      FStarC.Errors.err_exn e
+    else begin
+      Util.print1_error "Unexpected error: %s\n" (Util.message_of_exn e);
+      if Options.trace_error() then
+        Util.print1_error "Trace:\n%s\n" (Util.trace_of_exn e)
+      else
+        Util.print_error "Please file a bug report, ideally with a minimized version of the source program that triggered the error.\n"
+    end;
     report_errors []
 
 let main () =
@@ -368,8 +367,8 @@ let main () =
     then Util.print2_error "TOTAL TIME %s ms: %s\n"
               (FStarC.Util.string_of_int time)
               (String.concat " " (FStarC.Getopt.cmdline()));
-    cleanup ();
     exit 0
   with
-  | e -> handle_error e;
-        exit 1
+  | e ->
+    handle_error e;
+    exit 1

src/parser/FStarC.Parser.Dep.fst

@@ -540,11 +540,7 @@ exception Exit
 
 (* In public interface *)
 
-let core_modules () =
-  [Basefiles.prims_basename () ;
-   Basefiles.pervasives_basename () ;
-   Basefiles.pervasives_native_basename ()]
-  |> List.map module_name_of_file
+let core_modules () = [ "Prims"; "FStar.Pervasives"; "FStar.Pervasives.Native" ]
 
 let implicit_ns_deps =
   [ Const.fstar_ns_lid ]

src/syntax/FStarC.Syntax.Util.fst

@@ -1581,6 +1581,7 @@ let remove_attr (attr : lident) (attrs:list attribute) : list attribute =
 let process_pragma p r =
     FStarC.Errors.set_option_warning_callback_range (Some r);
     let set_options s =
+      try
       match Options.set_options s with
       | Getopt.Success -> ()
       | Getopt.Help  ->
@@ -1590,6 +1591,11 @@ let process_pragma p r =
         Errors.raise_error r Errors.Fatal_FailToProcessPragma [
           Errors.Msg.text <| "Failed to process pragma: " ^ s;
         ]
+      with
+      | Options.NotSettable x ->
+        Errors.raise_error r Errors.Fatal_FailToProcessPragma [
+          Errors.Msg.text <| U.format1 "Option '%s' is not settable via a pragma." x;
+        ]
     in
     match p with
     | ShowOptions ->